| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-10-02 | Univs: fixed 3685 by side-effect :) | Matthieu Sozeau | |
| 2015-10-02 | Univs: minor fixes to test-suite files | Matthieu Sozeau | |
| 108 used an implicit lowering to Prop. | |||
| 2015-10-02 | Univs: fix handling of evd's universes and side effects in build_by_tactic | Matthieu Sozeau | |
| 2015-10-02 | Univs: fix semantics of Type in proof mode in universe-polymorphic mode | Matthieu Sozeau | |
| Allowing universes to be instantiated if the body of the proof requires it (the levels stay flexible). Not allowed for non-polymorphic cases, to be compatible with the stm's invariant that the type should not change. | |||
| 2015-10-02 | Univs: fix minimization to allow lowering a universe to Set, not Prop. | Matthieu Sozeau | |
| 2015-10-02 | Univs: fix inference of the lowest sort for records. | Matthieu Sozeau | |
| 2015-10-02 | Univs: fix subtyping of polymorphic parameters. | Matthieu Sozeau | |
| 2015-10-02 | Univs: fix evar_map handling in Hint processing. | Matthieu Sozeau | |
| 2015-10-02 | Univs: fix test-suite file for HoTT/coq bug #120 | Matthieu Sozeau | |
| 2015-10-02 | Univs: test-suite file for bug #2016 | Matthieu Sozeau | |
| 2015-10-02 | Univs: test-suite file for #4301, subtyping of poly parameters | Matthieu Sozeau | |
| 2015-10-02 | Univs: uncovered bug in strengthening of opaque polymorphic definitions. | Matthieu Sozeau | |
| 2015-10-02 | Fix test-suite file for bug #3777 | Matthieu Sozeau | |
| 2015-10-02 | Fix test-suite file: failing earlier as expected. | Matthieu Sozeau | |
| 2015-10-02 | Fix test-suite file | Matthieu Sozeau | |
| 2015-10-02 | Univs: correcly compute the levels of records when they fall in Prop. | Matthieu Sozeau | |
| 2015-10-02 | Univs/program: handle side effects in obligations. | Matthieu Sozeau | |
| 2015-10-02 | Univs: fix Show Universes. | Matthieu Sozeau | |
| 2015-10-02 | Univs: fix handling of side effects/delayed proofs | Matthieu Sozeau | |
| - When there are side effects which might enrich the initial universes of a proof, keep the initial and refined universe contexts apart like for delayed proofs, ensuring universes are declared before they are used in the right order. - Fix undefined levels in proof statements so that they can't be lowered to Set by a subsequent, delayed proof. | |||
| 2015-10-02 | Univs: handle side-effects of futures correctly in kernel. | Matthieu Sozeau | |
| 2015-10-02 | Univs: fix environment handling in scheme building. | Matthieu Sozeau | |
| 2015-10-02 | discriminate: Do fresh_global in the right env in presence of side-effects. | Matthieu Sozeau | |
| 2015-10-02 | Univs: fixed bug 2584, correct universe found for mutual inductive. | Matthieu Sozeau | |
| 2015-10-02 | Univs: fix Universe vernacular, fix bug #4287. | Matthieu Sozeau | |
| No universe can be set lower than Prop anymore (or Set). | |||
| 2015-10-02 | Univs: fix after rebase (from_ctx/from_env) | Matthieu Sozeau | |
| 2015-10-02 | Univs: fixed bug #4328. | Matthieu Sozeau | |
| 2015-10-02 | Univs: fix many evar_map initializations and leaks. | Matthieu Sozeau | |
| 2015-10-02 | Univs (pretyping): allow parsing and decl of Top.n | Matthieu Sozeau | |
| This allows pretyping and detyping to be inverses regarding universes, and makes Function's detyping/pretyping manipulations bearable in presence of global universes that must be declared (otherwise an evd would need to be threaded there in many places as well). | |||
| 2015-10-02 | Univs (evd): deal with global universes and sideff | Matthieu Sozeau | |
| - Fix union of universe contexts to keep declarations - Fix side-effect handling to register new global universes in the graph. | |||
| 2015-10-02 | Univs: fix evar_map initialization in newring. | Matthieu Sozeau | |
| 2015-10-02 | Univs: fix evar_map leaks bugs in Function | Matthieu Sozeau | |
| The evar_map's that are used to typecheck terms must now always be initialized with the global universe graphs using Evd.from_env, so any failure to initialize and thread evar_map's correctly results in errors. | |||
| 2015-10-02 | Univs: fix an evar leak in congruence | Matthieu Sozeau | |
| 2015-10-02 | Univs: minimization, adapt to graph invariants. | Matthieu Sozeau | |
| We are forced to declare universes that are global and appear in the local constraints as we start from an empty universe graph. | |||
| 2015-10-02 | Univs (kernel) adapt to new invariants | Matthieu Sozeau | |
| Remove predicative flag and adapt to new invariant where every universe must be declared, ensuring it is >= Set, safe_repr is not necessary anymore. | |||
| 2015-10-02 | Univs: module constraints move to universe contexts as they might | Matthieu Sozeau | |
| declare new universes (e.g. with). | |||
| 2015-10-02 | Remove Print Universe directive. | Matthieu Sozeau | |
| 2015-10-02 | Univs: More info for developers. | Matthieu Sozeau | |
| 2015-10-02 | Forcing i > Set for global universes (incomplete) | Matthieu Sozeau | |
| 2015-10-02 | Univs: force all universes to be >= Set. | Matthieu Sozeau | |
| 2015-10-02 | Univs: Fix part of bug #4161 | Matthieu Sozeau | |
| Rechecking applications built by evarconv's imitation. | |||
| 2015-10-02 | Universes: enforce Set <= i for all Type occurrences. | Matthieu Sozeau | |
| 2015-10-02 | Changed status of Info messages from notice to info. | Pierre Courtieu | |
| This fixes a bug in proofgeneral. PG will now diplay this message eagerly. Otherwise since they appear before the goal, they are considered outdated and not displayed. | |||
| 2015-10-02 | emacs output mode: Added <infomsg> tag to debug messages. | Pierre Courtieu | |
| So that they display in response buffer. | |||
| 2015-09-30 | Fixing documentation wrt the ctrl-shift-u Unicode input method (see #2013). | Hugo Herbelin | |
| Incidentally made writing style in CoqIDE chapter more homogeneous. | |||
| 2015-09-30 | Build the compatibility files. | Guillaume Melquiond | |
| 2015-09-30 | Add compatibility files (feature 4319) | Jason Gross | |
| 2015-09-30 | Unexport Loadpath.get_paths. | Guillaume Melquiond | |
| 2015-09-29 | Fix dumb typo. | Guillaume Melquiond | |
| 2015-09-29 | Make the interface of System.raw_extern_intern much saner. | Guillaume Melquiond | |
| There is no reason (any longer?) to create simultaneous closures for interning and externing files. This patch makes the code more readable by separating both functions and their signatures. | |||
| 2015-09-29 | Prevent States.intern_state and System.extern_intern from looking up files ↵ | Guillaume Melquiond | |
| in the loadpath. This patch causes a bit of code duplication (because of the .coq suffix added to state files) but it makes it clear which part of the code is looking up files in the loadpath and for what purpose. Also it makes the interface of System.extern_intern and System.raw_extern_intern much saner. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |