aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Univs: fixed bug 2584, correct universe found for mutual inductive.Gravatar Matthieu Sozeau2015-10-02
* Univs: fix Universe vernacular, fix bug #4287.Gravatar Matthieu Sozeau2015-10-02
* Univs: fix after rebase (from_ctx/from_env)Gravatar Matthieu Sozeau2015-10-02
* Univs: fixed bug #4328.Gravatar Matthieu Sozeau2015-10-02
* Univs: fix many evar_map initializations and leaks.Gravatar Matthieu Sozeau2015-10-02
* Univs (pretyping): allow parsing and decl of Top.nGravatar Matthieu Sozeau2015-10-02
* Univs (evd): deal with global universes and sideffGravatar Matthieu Sozeau2015-10-02
* Univs: fix evar_map initialization in newring.Gravatar Matthieu Sozeau2015-10-02
* Univs: fix evar_map leaks bugs in FunctionGravatar Matthieu Sozeau2015-10-02
* Univs: fix an evar leak in congruenceGravatar Matthieu Sozeau2015-10-02
* Univs: minimization, adapt to graph invariants.Gravatar Matthieu Sozeau2015-10-02
* Univs (kernel) adapt to new invariantsGravatar Matthieu Sozeau2015-10-02
* Univs: module constraints move to universe contexts as they mightGravatar Matthieu Sozeau2015-10-02
* Remove Print Universe directive.Gravatar Matthieu Sozeau2015-10-02
* Univs: More info for developers.Gravatar Matthieu Sozeau2015-10-02
* Forcing i > Set for global universes (incomplete)Gravatar Matthieu Sozeau2015-10-02
* Univs: force all universes to be >= Set.Gravatar Matthieu Sozeau2015-10-02
* Univs: Fix part of bug #4161Gravatar Matthieu Sozeau2015-10-02
* Universes: enforce Set <= i for all Type occurrences.Gravatar Matthieu Sozeau2015-10-02
* Changed status of Info messages from notice to info.Gravatar Pierre Courtieu2015-10-02
* emacs output mode: Added <infomsg> tag to debug messages.Gravatar Pierre Courtieu2015-10-02
* Fixing documentation wrt the ctrl-shift-u Unicode input method (see #2013).Gravatar Hugo Herbelin2015-09-30
* Build the compatibility files.Gravatar Guillaume Melquiond2015-09-30
* Add compatibility files (feature 4319)Gravatar Jason Gross2015-09-30
* Unexport Loadpath.get_paths.Gravatar Guillaume Melquiond2015-09-30
* Fix dumb typo.Gravatar Guillaume Melquiond2015-09-29
* Make the interface of System.raw_extern_intern much saner.Gravatar Guillaume Melquiond2015-09-29
* 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
* Fixing loss of extra data in Evd.Gravatar Pierre-Marie Pédrot2015-09-27
* Documenting how to support some special unicode characters in coqdocGravatar Hugo Herbelin2015-09-26
* Clarifying the doc of coqdoc --utf8 as discussed on coq-club on August 19, 2015.Gravatar Hugo Herbelin2015-09-26
* Test for bug #4347.Gravatar Pierre-Marie Pédrot2015-09-26
* Fixing bug #4347: Not_found Exception with some Records.Gravatar Pierre-Marie Pédrot2015-09-26
* 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
* The -compile option now accepts ".v" files and outputs a warning otherwise.Gravatar Pierre-Marie Pédrot2015-09-25
* Hopefully better names to constructors of internal_flag, as discussedGravatar Hugo Herbelin2015-09-23
* Give a way to control if the decidable-equality schemes are built likeGravatar Hugo Herbelin2015-09-23
* Removing the generalization of the body of inductive schemes fromGravatar Hugo Herbelin2015-09-23
* Fixing bug #4207: setoid_rewrite creates self-referring hypotheses.Gravatar Pierre-Marie Pédrot2015-09-22
* Fixing tutorial.Gravatar Pierre-Marie Pédrot2015-09-21
* Change the default modifiers for navigation. (Fix bug #4295)Gravatar Guillaume Melquiond2015-09-21
* Proof: suggest Admitted->Qed only if the proof is really complete (#4349)Gravatar Enrico Tassi2015-09-20
* Print Assumptions shows engagement.Gravatar Maxime Dénès2015-09-20
* Nametab: print debug notice only in debug mode.Gravatar Maxime Dénès2015-09-20
* Remove unused type_in_type field in safe_env.Gravatar Maxime Dénès2015-09-20
* Test file for #3948 - Anomaly: unknown constant in Print Assumptions.Gravatar Maxime Dénès2015-09-20
* Revert "On MacOS X, ensuring that files found in the file system have the"Gravatar Maxime Dénès2015-09-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 21:59:55 +0000