| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-10-02 | Fixing error messages about Hint. | Hugo Herbelin | |
| 2015-10-02 | Improving reference manual in that auto uses simple apply rather than apply. | Hugo Herbelin | |
| Still, there are small differences, e.g. on "use_metas_eagerly_in_conv_on_closed_terms", but also maybe in some amount of use of delta that Matthieu would know better than me if it matters or not in practice. | |||
| 2015-10-02 | Update the history of versions with recent versions. | Hugo Herbelin | |
| 2015-10-02 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-02 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-02 | Univs: Change intf of push_named_def to return the computed universe | Matthieu Sozeau | |
| context Let-bound definitions can be opaque but the whole universe context was not gathered to be discharged at section closing time. | |||
| 2015-10-02 | Univs: refined handling of assumptions | Matthieu Sozeau | |
| According to their polymorphic/non-polymorphic status, which imply that universe variables introduced with it are assumed to be >= or > Set respectively in the following definitions. | |||
| 2015-10-02 | Univs: fix checker generating undeclared universes. | Matthieu Sozeau | |
| 2015-10-02 | Univs: fix test-suite file for #4287, now properly rejected. | Matthieu Sozeau | |
| 2015-10-02 | Univs: Remove test-suite file #3309 | Matthieu Sozeau | |
| This relied on universes lower than Prop. A proper test for the sharing option should be found, -type-in-type is not enough either. | |||
| 2015-10-02 | Univs: fix test-suite file (4301 is invalid, but a good regression test) | Matthieu Sozeau | |
| 2015-10-02 | Fix after rebase... | Matthieu Sozeau | |
| 2015-10-02 | Univs: forgot a substitution in mod_typing. | Matthieu Sozeau | |
| 2015-10-02 | Univs: correct handling of with in modules | Matthieu Sozeau | |
| For polymorphic and non-polymorphic parameters and definitions, fixes bugs #4298, #4294 | |||
| 2015-10-02 | Univs: the stdlib now needs 5 universes | Matthieu Sozeau | |
| Prop < Set < i for every global univ i | |||
| 2015-10-02 | Univs: fix bug #4251, handling of template polymorphic constants. | Matthieu Sozeau | |
| 2015-10-02 | Univs: update checker | Matthieu Sozeau | |
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |