aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* Univs: fix evar_map handling in Hint processing.Gravatar Matthieu Sozeau2015-10-02
* Univs: fix test-suite file for HoTT/coq bug #120Gravatar Matthieu Sozeau2015-10-02
* Univs: test-suite file for bug #2016Gravatar Matthieu Sozeau2015-10-02
* Univs: test-suite file for #4301, subtyping of poly parametersGravatar Matthieu Sozeau2015-10-02
* Univs: uncovered bug in strengthening of opaque polymorphic definitions.Gravatar Matthieu Sozeau2015-10-02
* Fix test-suite file for bug #3777Gravatar Matthieu Sozeau2015-10-02
* Fix test-suite file: failing earlier as expected.Gravatar Matthieu Sozeau2015-10-02
* Fix test-suite fileGravatar 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 handling of side effects/delayed proofsGravatar Matthieu Sozeau2015-10-02
* Univs: handle side-effects of futures correctly in kernel.Gravatar Matthieu Sozeau2015-10-02
* Univs: fix environment handling in scheme building.Gravatar Matthieu Sozeau2015-10-02
* discriminate: Do fresh_global in the right env in presence of side-effects.Gravatar Matthieu Sozeau2015-10-02
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 19:53:54 +0000