aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* 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
* Lemmas accept the Local flag.Gravatar Pierre-Marie Pédrot2015-10-17
* Remove -vm flag of coqtop.Gravatar Maxime Dénès2015-10-14
* Fixing bug #4367: Wrong error message in unification.Gravatar Pierre-Marie Pédrot2015-10-14
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* Fix Definition id := Eval <redexpr> in by passing the right universeGravatar Matthieu Sozeau2015-10-12
* Code cleaning in VM (with Benjamin).Gravatar Maxime Dénès2015-10-09
* Fix Next Obligation to not raise an anomaly in case of mutualGravatar Matthieu Sozeau2015-10-09
* Axioms now support the universe binding syntax.Gravatar Pierre-Marie Pédrot2015-10-08
* aux_file: export API to ease writing of a Proof Using annotator.Gravatar Enrico Tassi2015-10-08
* Proof using: let-in policy, optional auto-clear, forward closure*Gravatar Enrico Tassi2015-10-08
* Spawn: use each socket exclusively for writing or readingGravatar Enrico Tassi2015-10-08
* Goptions: new value type: optional stringGravatar Enrico Tassi2015-10-08
* Univs: fix FingerTree contrib.Gravatar Matthieu Sozeau2015-10-07
* Univs: add Strict Universe Declaration option (on by default)Gravatar Matthieu Sozeau2015-10-07
* Univs: fix handling of evar_map in identity coercion construction.Gravatar Matthieu Sozeau2015-10-05
* Fix after rebase...Gravatar Matthieu Sozeau2015-10-02
* Univs: fix inference of the lowest sort for records.Gravatar Matthieu Sozeau2015-10-02
* Univs: correcly compute the levels of records when they fall in Prop.Gravatar Matthieu Sozeau2015-10-02
* Univs/program: handle side effects in obligations.Gravatar Matthieu Sozeau2015-10-02
* Univs: fix Show Universes.Gravatar Matthieu Sozeau2015-10-02
* Univs: fix environment handling in scheme building.Gravatar Matthieu Sozeau2015-10-02
* Univs: fix after rebase (from_ctx/from_env)Gravatar Matthieu Sozeau2015-10-02
* Univs: fix many evar_map initializations and leaks.Gravatar Matthieu Sozeau2015-10-02
* Universes: enforce Set <= i for all Type occurrences.Gravatar Matthieu Sozeau2015-10-02
* Prevent States.intern_state and System.extern_intern from looking up files in...Gravatar Guillaume Melquiond2015-09-29
* Remove some uses of Loadpath.get_paths.Gravatar Guillaume Melquiond2015-09-29
* Make -load-vernac-object respect the loadpath.Gravatar Guillaume Melquiond2015-09-28
* The -require option now accepts a logical path instead of a physical one.Gravatar Pierre-Marie Pédrot2015-09-25
* Updating the documentation and the toolchain w.r.t. the change in -compile.Gravatar Pierre-Marie Pédrot2015-09-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 17:16:04 +0000