aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2016-04-17Building lazily a few debugging messages involving expressions of commandsHugo Herbelin
2016-04-07Allow to unset the refinement mode of Instance in MLMatthieu Sozeau
2016-03-24Fix handling of arity of definitional classes.Matthieu Sozeau
2016-03-17Fix bug #4627: records with no declared arity can be template polymorphic.Matthieu Sozeau
2016-03-15Fix bug when a sort is ascribed to a RecordMatthieu Sozeau
2016-03-07Adding backtraces to scheme error messages.Pierre-Marie Pédrot
2016-03-04Rename Ephemeron -> CEphemeron.Maxime Dénès
2016-02-19Fixing bug #4580: [Set Refine Instance Mode] also used for Program Instance.Pierre-Marie Pédrot
2016-02-08Improving error message with missing patterns in the presence ofHugo Herbelin
2016-01-24Fixing bug #3826: "Incompatible module types" is uninformative.Pierre-Marie Pédrot
2016-01-24Fixing bug #4495: Failed assertion in metasyntax.ml.Pierre-Marie Pédrot
2016-01-23Implement support for universe binder lists in Instance and Program Fixpoint/...Matthieu Sozeau
2016-01-22Restore warnings produced by the interpretation of the command lineHugo Herbelin
2016-01-20Update copyright headers.Maxime Dénès
2016-01-15Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Maxime Dénès
2015-12-22Inclusion of functors with restricted signature is now forbidden (fix #3746)Pierre Letouzey
2015-12-14Flag -compat 8.4 now loads Coq.Compat.Coq84.Maxime Dénès
2015-12-09Print Assumptions: improve detection of case on an axiom of FalseEnrico Tassi
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-11-28Univs: correctly register universe binders for lemmas.Matthieu Sozeau
2015-11-27Fix [Polymorphic Hint Rewrite].Matthieu Sozeau
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-19Allow program hooks to see the refined universe_context at the end of aMatthieu Sozeau
2015-11-02Adding syntax "Show id" to show goal named id (shelved or not).Hugo Herbelin
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-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-25Minor module cleanup : error HigherOrderInclude was never happeningPierre Letouzey
2015-10-18Miscellaneous typos, spacing, US spelling in comments or variable names.Hugo Herbelin
2015-10-17Lemmas accept the Local flag.Pierre-Marie Pédrot
2015-10-14Remove -vm flag of coqtop.Maxime Dénès
2015-10-14Fixing bug #4367: Wrong error message in unification.Pierre-Marie Pédrot
2015-10-13Fix some typos.Guillaume Melquiond
2015-10-12Fix Definition id := Eval <redexpr> in by passing the right universeMatthieu Sozeau
2015-10-09Code cleaning in VM (with Benjamin).Maxime Dénès
2015-10-09Fix Next Obligation to not raise an anomaly in case of mutualMatthieu Sozeau
2015-10-08Axioms now support the universe binding syntax.Pierre-Marie Pédrot
2015-10-08aux_file: export API to ease writing of a Proof Using annotator.Enrico Tassi
2015-10-08Proof using: let-in policy, optional auto-clear, forward closure*Enrico Tassi
2015-10-08Spawn: use each socket exclusively for writing or readingEnrico Tassi
2015-10-08Goptions: new value type: optional stringEnrico Tassi
2015-10-07Univs: fix FingerTree contrib.Matthieu Sozeau
2015-10-07Univs: add Strict Universe Declaration option (on by default)Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 10:37:01 +0000