aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2016-01-06Remove deprecated command-line options such as "-as".Guillaume Melquiond
2016-01-02Reduce dependencies of interface files.Guillaume Melquiond
2016-01-02Remove useless rec flags.Guillaume Melquiond
2016-01-02Simplification of grammar_prod_item type.Pierre-Marie Pédrot
2016-01-02Separation of concern in TacAlias API.Pierre-Marie Pédrot
2015-12-31Merge branch 'v8.5' into trunkGuillaume Melquiond
2015-12-30External tactics and notations now accept any tactic argument.Pierre-Marie Pédrot
2015-12-22Do not compose "str" and "to_string" whenever possible.Guillaume Melquiond
2015-12-22Inclusion of functors with restricted signature is now forbidden (fix #3746)Pierre Letouzey
2015-12-18CLEANUP: Vernacexpr.VernacDeclareTacticDefinitionMatej Kosik
2015-12-18CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular comma...Matej Kosik
2015-12-18CLEANUP: simplifying "Coqtop.init_gc" implementationMatej Kosik
2015-12-18CLEANUP: removing unnecessary wrapper functionMatej Kosik
2015-12-18CLEANUP: Vernacexpr.vernac_exprMatej Kosik
2015-12-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-14Flag -compat 8.4 now loads Coq.Compat.Coq84.Maxime Dénès
2015-12-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-09Print Assumptions: improve detection of case on an axiom of FalseEnrico Tassi
2015-12-05Moving extended_rel_vect/extended_rel_list to the kernel.Hugo Herbelin
2015-12-05Moving three related small half-general half-ad-hoc utility functionsHugo Herbelin
2015-12-03Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-02Univs/Program: update the universe context with global universeMatthieu Sozeau
2015-12-02Fix bug #4444: Next Obligation performed after a Section opening wasMatthieu Sozeau
2015-12-02Removing dead code in Obligations.Pierre-Marie Pédrot
2015-11-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-28Univs: correctly register universe binders for lemmas.Matthieu Sozeau
2015-11-27Fix [Polymorphic Hint Rewrite].Matthieu Sozeau
2015-11-26Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-24Univs: carry on universe substitution when defining obligations ofMatthieu Sozeau
2015-11-23Fix output of universe arcs. (Fix bug #4422)Guillaume Melquiond
2015-11-20Univs: generation of induction schemes should not generated uselessMatthieu Sozeau
2015-11-20Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-19Allow program hooks to see the refined universe_context at the end of aMatthieu Sozeau
2015-11-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-02Adding syntax "Show id" to show goal named id (shelved or not).Hugo Herbelin
2015-10-30Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-30Command.declare_definition: grab the fix_exn early (follows 77cf18e)Enrico Tassi
2015-10-30Add a way to get the right fix_exn in external vernacular commandsMatthieu Sozeau
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-29Accept option -compat 8.5. (Fix bug #4393)Guillaume Melquiond
2015-10-28Univs: local names handling.Matthieu Sozeau
2015-10-28Avoid type checking private_constants (side_eff) again during Qed (#4357).Enrico Tassi
2015-10-28Univs: fix bug #4375, accept universe binders on (co)-fixpointsMatthieu Sozeau
2015-10-27Fix bugs 4389, 4390 and 4391 due to wrong handling of universe namesMatthieu Sozeau
2015-10-27Type-safe Egramml.grammar_prod_item.Pierre-Marie Pédrot
2015-10-27Finer type for Pcoq.interp_entry_name.Pierre-Marie Pédrot
2015-10-27Indexing existentially quantified entries returned by interp_entry_name.Pierre-Marie Pédrot
2015-10-26Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-25Minor module cleanup : error HigherOrderInclude was never happeningPierre Letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-20 20:38:52 +0000