aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* A hack to fix another regression with Ltac trace report in 8.5. E.g.Gravatar Hugo Herbelin2016-06-18
* Merge branch 'bug4725' into v8.5Gravatar Matthieu Sozeau2016-06-14
|\
* | Tentatively fixing misguiding error message with "binder" type inGravatar Hugo Herbelin2016-06-13
* | Reserve exception "ConversionFailed" in unification for failure ofGravatar Hugo Herbelin2016-06-12
* | Fixing bug in printing CannotSolveConstraint (collision of context names).Gravatar Hugo Herbelin2016-06-12
* | Fixing problems introduced in 8.5 with Ltac trace report. E.g.Gravatar Hugo Herbelin2016-06-06
* | Revert "Rename Lexer -> CLexer."Gravatar Pierre-Marie Pédrot2016-05-31
| * Univs/Program/Function: Fix bug #4725Gravatar Matthieu Sozeau2016-05-26
| * Program: remove debug tracingGravatar Matthieu Sozeau2016-05-26
|/
* Fix bug #3887: Better error message for "More than one program with unsolved ...Gravatar Pierre-Marie Pédrot2016-05-09
* Rename Lexer -> CLexer.Gravatar Pierre-Marie Pédrot2016-05-09
* Fix bug #4705: coqtop accepts both -emacs and -ideslave.Gravatar Pierre-Marie Pédrot2016-05-03
* Call hooks when terminating a definition proof (bug #4663).Gravatar Guillaume Melquiond2016-05-03
* Properly handle notations containing spaces (bug #4538).Gravatar Guillaume Melquiond2016-05-02
* Building lazily a few debugging messages involving expressions of commandsGravatar Hugo Herbelin2016-04-17
* Allow to unset the refinement mode of Instance in MLGravatar Matthieu Sozeau2016-04-07
* Fix handling of arity of definitional classes.Gravatar Matthieu Sozeau2016-03-24
* Fix bug #4627: records with no declared arity can be template polymorphic.Gravatar Matthieu Sozeau2016-03-17
* Fix bug when a sort is ascribed to a RecordGravatar Matthieu Sozeau2016-03-15
* Adding backtraces to scheme error messages.Gravatar Pierre-Marie Pédrot2016-03-07
* Rename Ephemeron -> CEphemeron.Gravatar Maxime Dénès2016-03-04
* Fixing bug #4580: [Set Refine Instance Mode] also used for Program Instance.Gravatar Pierre-Marie Pédrot2016-02-19
* Improving error message with missing patterns in the presence ofGravatar Hugo Herbelin2016-02-08
* Fixing bug #3826: "Incompatible module types" is uninformative.Gravatar Pierre-Marie Pédrot2016-01-24
* Fixing bug #4495: Failed assertion in metasyntax.ml.Gravatar Pierre-Marie Pédrot2016-01-24
* Implement support for universe binder lists in Instance and Program Fixpoint/...Gravatar Matthieu Sozeau2016-01-23
* Restore warnings produced by the interpretation of the command lineGravatar Hugo Herbelin2016-01-22
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Gravatar Maxime Dénès2016-01-15
* Inclusion of functors with restricted signature is now forbidden (fix #3746)Gravatar Pierre Letouzey2015-12-22
* Flag -compat 8.4 now loads Coq.Compat.Coq84.Gravatar Maxime Dénès2015-12-14
* Print Assumptions: improve detection of case on an axiom of FalseGravatar Enrico Tassi2015-12-09
* Univs/Program: update the universe context with global universeGravatar Matthieu Sozeau2015-12-02
* Fix bug #4444: Next Obligation performed after a Section opening wasGravatar Matthieu Sozeau2015-12-02
* Univs: correctly register universe binders for lemmas.Gravatar Matthieu Sozeau2015-11-28
* Fix [Polymorphic Hint Rewrite].Gravatar Matthieu Sozeau2015-11-27
* Univs: carry on universe substitution when defining obligations ofGravatar Matthieu Sozeau2015-11-24
* Fix output of universe arcs. (Fix bug #4422)Gravatar Guillaume Melquiond2015-11-23
* Univs: generation of induction schemes should not generated uselessGravatar Matthieu Sozeau2015-11-20
* Allow program hooks to see the refined universe_context at the end of aGravatar Matthieu Sozeau2015-11-19
* Adding syntax "Show id" to show goal named id (shelved or not).Gravatar Hugo Herbelin2015-11-02
* Command.declare_definition: grab the fix_exn early (follows 77cf18e)Gravatar Enrico Tassi2015-10-30
* Add a way to get the right fix_exn in external vernacular commandsGravatar Matthieu Sozeau2015-10-30
* Accept option -compat 8.5. (Fix bug #4393)Gravatar Guillaume Melquiond2015-10-29
* Univs: local names handling.Gravatar Matthieu Sozeau2015-10-28
* Avoid type checking private_constants (side_eff) again during Qed (#4357).Gravatar Enrico Tassi2015-10-28
* Univs: fix bug #4375, accept universe binders on (co)-fixpointsGravatar Matthieu Sozeau2015-10-28
* Fix bugs 4389, 4390 and 4391 due to wrong handling of universe namesGravatar Matthieu Sozeau2015-10-27
* Minor module cleanup : error HigherOrderInclude was never happeningGravatar Pierre Letouzey2015-10-25
* Miscellaneous typos, spacing, US spelling in comments or variable names.Gravatar Hugo Herbelin2015-10-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 08:58:45 +0000