| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-06-20 | Bug 27 closed now that universe contexts can be refined during the proof, | Matthieu Sozeau | |
| here instantiating a flexible level with Set. | |||
| 2014-06-19 | HoTT coq bug #62 fixed. | Matthieu Sozeau | |
| 2014-06-18 | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau | |
| and avoiding explicit substitutions and merging of contexts, e.g. in obligations.ml. The context produced by typechecking a statement is passed in the proof, allowing the universe name context to be correctly folded as well. Mainly an API cleanup. | |||
| 2014-06-17 | Fix a destArity that does not exactly match isArity in presence of let-ins. | Matthieu Sozeau | |
| 2014-06-17 | Reinstate eta for records in evarconv, fixing two HoTT coq bugs. | Matthieu Sozeau | |
| 2014-06-17 | Not a bug, keep for backwards compatibility | Matthieu Sozeau | |
| 2014-06-17 | Bug closed, now in polymorphic mode, Variables A B : Type give different ↵ | Matthieu Sozeau | |
| levels to A and B. | |||
| 2014-06-17 | Explicit universes allow to write liftings explicitely. Implicit lifting ↵ | Matthieu Sozeau | |
| would change the theory non-trivially. | |||
| 2014-06-17 | Not considering test-suite file #89 as a bug anymore. | Matthieu Sozeau | |
| 2014-06-17 | Continue fix on argument scopes of primitive projections. | Matthieu Sozeau | |
| 2014-06-17 | Fix HoTT bug #84, binding scopes to projections. | Matthieu Sozeau | |
| 2014-06-17 | HoTT coq bug #82 already fixed. | Matthieu Sozeau | |
| 2014-06-17 | Adapt coercion code to work with projections as target classes. | Matthieu Sozeau | |
| 2014-06-17 | Fixing #3282 (two bugs in the presence of let-in's in "fix"). | Hugo Herbelin | |
| 2014-06-17 | - Fix the de Bruijn problem in check_projection for good :) | Matthieu Sozeau | |
| - Fix HoTT coq bug #80, implicit arguments with primitive projections were wrongly automatically infered. | |||
| 2014-06-17 | Fix a de Bruijn bug in checking code of projections. | Matthieu Sozeau | |
| 2014-06-17 | Existing Class now works with universe polymorphism. Fixes HoTT bug #063 | Matthieu Sozeau | |
| 2014-06-16 | Unification in HoTT_coq_061.v was looping with previous commit (while | Hugo Herbelin | |
| it was failing with Not_found before previous commit). This "fixes" the loop by expanding local defs in "imitate" rather than keeping them explicit. The example is otherwise too large for me to be able to understand where does the loop come from. | |||
| 2014-06-16 | - Add "Show Universes" to print information about universes during a proof. | Matthieu Sozeau | |
| - Remove dead code in evarconv. | |||
| 2014-06-16 | HoTT bug #29 is fixed, using the correct notion of polymorphic product types. | Matthieu Sozeau | |
| 2014-06-15 | Fix test-suite file | Matthieu Sozeau | |
| 2014-06-15 | Change Ltac constr matching semantics to consider universes when merging two | Matthieu Sozeau | |
| bindings of the same variable (fixing HoTT bug #52). Document the unification of universes in Ltac/tactics. | |||
| 2014-06-15 | The semantics of Variable x y : T is to have the exact same type T for x and y, | Matthieu Sozeau | |
| while Context gives different type to each variable, this test-suite file shows this. | |||
| 2014-06-15 | Remove HoTT bug #33, as the stdlib won't become polymorphic in the next version. | Matthieu Sozeau | |
| 2014-06-15 | - Fix xml plugin treatment of inductives. | Matthieu Sozeau | |
| - Move HoTT bug #30 to closed | |||
| 2014-06-13 | Fix HoTT/coq bug # 14. Now coercion code correctly raises an error instead ↵ | Matthieu Sozeau | |
| of an anomaly in case a universe inconsistency occurs when applying a coercion. The statement of the test-suite file cannot check as is, but does check when the correct FunctorCategory is given, instantiating the TypeCat to Set. | |||
| 2014-06-13 | HoTT/coq bug #7 is closed, and the definitions can be made to go through ↵ | Matthieu Sozeau | |
| using explicit universes. The behavior of Hint Rewrite still differs from Hint Resolve though. | |||
| 2014-06-13 | Fixing "clear" in internal_cut_replace: forbid dependencies in the | Hugo Herbelin | |
| name of replaced hypothesis. | |||
| 2014-06-13 | Fixing wrong environment for Meta's in pose_all_metas_as_evars (bug #3284). | Hugo Herbelin | |
| 2014-06-11 | Fix bug #3291, stack overflow in rewrite. | Matthieu Sozeau | |
| 2014-06-11 | Fix bug #3289 | Matthieu Sozeau | |
| 2014-06-11 | Move bug # 3368 to closed bugs | Matthieu Sozeau | |
| 2014-06-10 | Add many more cases to the test-suite | Jason Gross | |
| I'd add more, but I'm tired and it's late and I should sleep. Maybe I'll pick up at 3279 (working down) another day. Bug 3344 is broken; [Fail Defined.] says that [Defined] has not failed, even though it raises an anomaly. So there's no way I can think of to test it. I've left it in the [opened] directory anyway. | |||
| 2014-06-10 | Move closed bug 3314 | Jason Gross | |
| 2014-06-10 | Add a test-case for bug #3314 proving False | Jason Gross | |
| 2014-06-08 | Mark some progress in the HoTT/coq test-suite | Jason Gross | |
| I've marked new failing commands that I'm confused about with "???"; I'm not sure whether or not they should fail there, but we should keep the test-suite compiling, probably. | |||
| 2014-06-08 | Fix canonical structure resolution in unification (bug found in Ssreflect). | Matthieu Sozeau | |
| 2014-06-08 | ind_tables: always declare side effects (Closes: HOTT#110) | Enrico Tassi | |
| declare takes care of ignoring side effects that are available in the global environment. This is yet another instance of what the "abominion" (aka abstract) can do: the code was checking for the existence in the environment of the elimination principle, and not regenerating it (nor declaring the corresponding side effect) if the elimination principle is used twice. Of course to functionalize the imperative actions on the environment when two proofs generated by abstract use the same elim principle, such elim principle has to be inlined twice, once in each abstracted proof. In other words, a side effect generated by a tactic inside an abstract is *global* but will be made local, si it must always be declared, no matter what. Now the system works like this: - side effects are always declared, even if a caching mechanism thinks the constant is already there (it can be there, no need to regenerate it but the intent to generate it *must* be declared anyhow) - at Qed time, we filter the list of side effects and decide which ones are really needed to be inlined. bottom line: STOP using abstract. | |||
| 2014-06-04 | - Better parsing and printing of named universes: Type{ident} and ↵ | Matthieu Sozeau | |
| foo@{(ident|Prop|Set|Type|' ')*} (user given names are still write only). - Add test-suite file for named universes. | |||
| 2014-06-04 | - Force every universe level to be >= Prop, so one cannot "go under" it anymore. | Matthieu Sozeau | |
| - Finish the change to level-to-level substitutions, in the checker. | |||
| 2014-06-04 | - Fix hashing of levels to get the "right" order in universe contexts etc... | Matthieu Sozeau | |
| - Add a tentative syntax for specifying universes: Type{"i"} and foo@{Type{"i"},Type{"j"}}. These are always rigid. - Use level-to-level substitutions where the more general level-to-universe substitutions were previously used. | |||
| 2014-06-04 | cbn understand ! Arguments directive | Pierre Boutillier | |
| Of course, this is an under approximation of the expected behavior : unfolding a constant iff a leaf of its underlying split-tree is reached. | |||
| 2014-06-03 | A bug has been closed (HoTT/coq #105) | Jason Gross | |
| 2014-05-31 | More on injection over a projectable "existT". - Fixing syntax "injection ↵ | Hugo Herbelin | |
| ... as ..." which was not working. - Now applying the simplification on any "existT" generated by "injection" (possible source of incompatibilities). | |||
| 2014-05-31 | Fixing introduction patterns * and ** when used in a branch so that they do ↵ | Hugo Herbelin | |
| not introduce beyond what is under control of the branch. See test-suite intros.v for an example. | |||
| 2014-05-30 | Adding test-suite for bug #3355. | Pierre-Marie Pédrot | |
| 2014-05-26 | - Fix in kernel conversion not folding the universe constraints | Matthieu Sozeau | |
| correctly when comparing stacks. - Disallow Type i <= Prop/Set constraints, that would otherwise allow constraints that make a universe lower than Prop. - Fix stm/lemmas that was pushing constraints to the global context, it is done depending on the constant/variable polymorphic status now. - Adapt generalized rewriting in Type code to these fixes. | |||
| 2014-05-16 | Fix unification of non-unfoldable primitive projections in evarconv. | Matthieu Sozeau | |
| 2014-05-13 | Test-suite for bug #3259. | Pierre-Marie Pédrot | |
| 2014-05-12 | Update various polyproj bugs w.r.t. latest trunk | Jason Gross | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |
path: root/test-suite