| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot | |
| 2014-06-17 | Fix type inference of the record argument of a projection to catch ill-typed | Matthieu Sozeau | |
| applications earlier. | |||
| 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 | Safer entry point of primitive projections in the kernel, now it does recognize | Matthieu Sozeau | |
| a projection constant only of the form λ params (r : I params), match r with BuildR args => args_i end, without any other user input and relies on it being typable (no more primitive projections escaping this). | |||
| 2014-06-17 | Existing Class now works with universe polymorphism. Fixes HoTT bug #063 | Matthieu Sozeau | |
| 2014-06-17 | Improve hotspot in Auto. | Pierre-Marie Pédrot | |
| 2014-06-16 | Checking that a library name is valid before compilation. | Pierre-Marie Pédrot | |
| Fixes bug #3333. | |||
| 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 | Fixing part of HoTT bug #61 (in declare_evar_from_virtual_equation, | Hugo Herbelin | |
| fix the type of the term which has to be in the signature of the evar to declare); some problems remain though (see next commit). | |||
| 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-16 | Fix spacing in error message. | Guillaume Melquiond | |
| 2014-06-16 | Preemptively remove files from native compilation. | Guillaume Melquiond | |
| Ocaml does not remove the .cmi file if compilation fails, thus causing subsequent native compilations to fail due to mismatching interfaces. For the sake of homogeneity, also remove the .cmo/.cmxs file along the way. | |||
| 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 | Deprecate useless option -quality. | Guillaume Melquiond | |
| 2014-06-13 | Remove documentation for the unsupported options -byte and -opt. | Guillaume Melquiond | |
| 2014-06-13 | Deprecate useless option -unsafe. | Guillaume Melquiond | |
| 2014-06-13 | Deprecate options -dont, -lazy, -force-load-proofs. | Guillaume Melquiond | |
| These options no longer have any impact on the way proofs are loaded. In other words, loading is always lazy, whatever the options. Keeping them just so that coqc dies when the user prints some opaque symbol does not seem worth it. | |||
| 2014-06-13 | Less ocaml warnings. | Hugo Herbelin | |
| 2014-06-13 | Improving tclWITHHOLES which did not see undefined evars up to | Hugo Herbelin | |
| restriction, after last fix commit which precisely possibly restricts evars of a term "t" in "apply t in H" without resolving them. | |||
| 2014-06-13 | Fixing "clear" in internal_cut_replace: forbid dependencies in the | Hugo Herbelin | |
| name of replaced hypothesis. | |||
| 2014-06-13 | Improved error message when a meta posed as an evar remains unsolved | Hugo Herbelin | |
| in case prefix 'e' of "apply" and co is not given. | |||
| 2014-06-13 | Check resolution of Metas turned into Evars by pose_all_metas_as_evars | Hugo Herbelin | |
| in unification.ml in case prefix 'e' of "apply" and co is not given. | |||
| 2014-06-13 | Fixing wrong environment for Meta's in pose_all_metas_as_evars (bug #3284). | Hugo Herbelin | |
| 2014-06-13 | Adapt simpl/cbn unfolding and refolding machinery to projections, so that | Matthieu Sozeau | |
| primitive projections obey the Arguments command. | |||
| 2014-06-12 | Code cleaning in Univ. | Pierre-Marie Pédrot | |
| 2014-06-12 | Passing some tactics to the new monad type. | Pierre-Marie Pédrot | |
| 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-11 | Merge branch 'more-test-suite' of https://github.com/JasonGross/coq into trunk | Matthieu Sozeau | |
| 2014-06-11 | - Fix bug #3368, due to wrong use of the Cst_stack for projections. | Matthieu Sozeau | |
| - Monomorphize Cst_stack to 'a = constr. - Add corresponding debug printer. | |||
| 2014-06-11 | In generalized rewrite, avoid retyping completely and constantly the ↵ | Matthieu Sozeau | |
| conclusion, and results of unifying the lemma with subterms. Using Retyping.get_type_of instead results in 3x speedup in Ncring_polynom. | |||
| 2014-06-11 | fix handling of side effects in abstract (fixes QArithSternBrocot) | Enrico Tassi | |
| The right fix should probably be to remove the build_constant_by_tactic function and only use the build_by_tactic one | |||
| 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-10 | Fixing Sorting Universes in a world where le and lt constraints may be | Pierre-Marie Pédrot | |
| redundant in canonical arcs. | |||
| 2014-06-10 | Compute the trace of a universe inconsistency only when explicitly required | Pierre-Marie Pédrot | |
| by the printing options (i.e. when "Print Universes" is set). | |||
| 2014-06-10 | Made explanations for universe inconsistencies optional. They are only used | Pierre-Marie Pédrot | |
| by the printer anyway. | |||
| 2014-06-10 | Specialize the type of [Univ.compare_neq] so that it is clear it is only used | Pierre-Marie Pédrot | |
| to recover the trace of a universe inconsistency. Changed its name too btw. | |||
| 2014-06-10 | Removing dead code in checker/univ.ml. | Pierre-Marie Pédrot | |
| 2014-06-10 | Removing explanations of universe inconsistencies from the checker. They | Pierre-Marie Pédrot | |
| were never used and were responsible for code duplication. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |