aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-10-02Univs: fix test-suite file for HoTT/coq bug #120Matthieu Sozeau
2015-10-02Univs: test-suite file for bug #2016Matthieu Sozeau
2015-10-02Univs: test-suite file for #4301, subtyping of poly parametersMatthieu Sozeau
2015-10-02Univs: uncovered bug in strengthening of opaque polymorphic definitions.Matthieu Sozeau
2015-10-02Fix test-suite file for bug #3777Matthieu Sozeau
2015-10-02Fix test-suite file: failing earlier as expected.Matthieu Sozeau
2015-10-02Fix test-suite fileMatthieu Sozeau
2015-10-02Univs: correcly compute the levels of records when they fall in Prop.Matthieu Sozeau
2015-10-02Univs/program: handle side effects in obligations.Matthieu Sozeau
2015-10-02Univs: fix Show Universes.Matthieu Sozeau
2015-10-02Univs: fix handling of side effects/delayed proofsMatthieu Sozeau
2015-10-02Univs: handle side-effects of futures correctly in kernel.Matthieu Sozeau
2015-10-02Univs: fix environment handling in scheme building.Matthieu Sozeau
2015-10-02discriminate: Do fresh_global in the right env in presence of side-effects.Matthieu Sozeau
2015-10-02Univs: fixed bug 2584, correct universe found for mutual inductive.Matthieu Sozeau
2015-10-02Univs: fix Universe vernacular, fix bug #4287.Matthieu Sozeau
2015-10-02Univs: fix after rebase (from_ctx/from_env)Matthieu Sozeau
2015-10-02Univs: fixed bug #4328.Matthieu Sozeau
2015-10-02Univs: fix many evar_map initializations and leaks.Matthieu Sozeau
2015-10-02Univs (pretyping): allow parsing and decl of Top.nMatthieu Sozeau
2015-10-02Univs (evd): deal with global universes and sideffMatthieu Sozeau
2015-10-02Univs: fix evar_map initialization in newring.Matthieu Sozeau
2015-10-02Univs: fix evar_map leaks bugs in FunctionMatthieu Sozeau
2015-10-02Univs: fix an evar leak in congruenceMatthieu Sozeau
2015-10-02Univs: minimization, adapt to graph invariants.Matthieu Sozeau
2015-10-02Univs (kernel) adapt to new invariantsMatthieu Sozeau
2015-10-02Univs: module constraints move to universe contexts as they mightMatthieu Sozeau
2015-10-02Remove Print Universe directive.Matthieu Sozeau
2015-10-02Univs: More info for developers.Matthieu Sozeau
2015-10-02Forcing i > Set for global universes (incomplete)Matthieu Sozeau
2015-10-02Univs: force all universes to be >= Set.Matthieu Sozeau
2015-10-02Univs: Fix part of bug #4161Matthieu Sozeau
2015-10-02Universes: enforce Set <= i for all Type occurrences.Matthieu Sozeau
2015-10-02Changed status of Info messages from notice to info.Pierre Courtieu
2015-10-02emacs output mode: Added <infomsg> tag to debug messages.Pierre Courtieu
2015-09-30Fixing documentation wrt the ctrl-shift-u Unicode input method (see #2013).Hugo Herbelin
2015-09-30Build the compatibility files.Guillaume Melquiond
2015-09-30Add compatibility files (feature 4319)Jason Gross
2015-09-30Unexport Loadpath.get_paths.Guillaume Melquiond
2015-09-29Fix dumb typo.Guillaume Melquiond
2015-09-29Make the interface of System.raw_extern_intern much saner.Guillaume Melquiond
2015-09-29Prevent States.intern_state and System.extern_intern from looking up files in...Guillaume Melquiond
2015-09-29Remove some uses of Loadpath.get_paths.Guillaume Melquiond
2015-09-28Make -load-vernac-object respect the loadpath.Guillaume Melquiond
2015-09-27Fixing loss of extra data in Evd.Pierre-Marie Pédrot
2015-09-26Documenting how to support some special unicode characters in coqdocHugo Herbelin
2015-09-26Clarifying the doc of coqdoc --utf8 as discussed on coq-club on August 19, 2015.Hugo Herbelin
2015-09-26Test for bug #4347.Pierre-Marie Pédrot
2015-09-26Fixing bug #4347: Not_found Exception with some Records.Pierre-Marie Pédrot
2015-09-25The -require option now accepts a logical path instead of a physical one.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-17 21:37:32 +0000