| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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. | |||
| 2014-06-10 | Imperatively check touched universes in compare_neq functions. This ensures | Pierre-Marie Pédrot | |
| a O(1) check, contrasting with the previous O(n) behaviour that rendered universe constraint checking prohibitive on big files. I expect a 20% speedup on such files. | |||
| 2014-06-10 | Providing the checker with its own version of the Univ file. | Pierre-Marie Pédrot | |
| I also took the opportunity to remove a lot of code not used by the checker. | |||
| 2014-06-10 | - Fix substitution of universes which needlessly hashconsed existing universes. | Matthieu Sozeau | |
| - More cleanup. remove unneeded functions in universes | |||
| 2014-06-10 | Oops, one refactoring was not compiled. | Matthieu Sozeau | |
| 2014-06-10 | More cleanup/reorganizing of univ.ml to separate constraint/universe ↵ | Matthieu Sozeau | |
| handling from the instance/contexts and substitution code. | |||
| 2014-06-10 | Fix module order in printers.mllib | Matthieu Sozeau | |
| 2014-06-10 | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in ↵ | Matthieu Sozeau | |
| Universes. Needed to exponse compare_head_gen(_leq) so that it could be reused in Universes. Remove unused functions from univ as well and refactor a little bit. Changed the syntax to Type@{} for explicit universe level specs, following the WG decision. | |||
| 2014-06-10 | Remove unused function in univ | Matthieu Sozeau | |
| 2014-06-10 | Merge branch 'hott-test-suite-progress' of https://github.com/JasonGross/coq ↵ | Matthieu Sozeau | |
| into trunk | |||
| 2014-06-09 | Flattening Level module structure in Univ. | Pierre-Marie Pédrot | |
| 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 | Adding a toplevel option allowing to deactivate the term sharing in kernel | Pierre-Marie Pédrot | |
| reduction. | |||
| 2014-06-08 | Moving hook code from Future to Lemmas. This seemed to disrupt compilation of | Pierre-Marie Pédrot | |
| the checker, and it was not used before that anyway. | |||
| 2014-06-08 | Fix canonical structure resolution in unification (bug found in Ssreflect). | Matthieu Sozeau | |
| 2014-06-08 | Timeout implementation for Windows based on threads. | Pierre-Marie Pédrot | |
| 2014-06-08 | Enforce a correct exception handling in declaration_hooks | Enrico Tassi | |
| This should finally get rid of the following class of bugs: Qed fails, STM undoes to the beginning of the proof because the exception is not annotated with the correct state, PG gets out of sync because errors always refer to the last command in PGIP. | |||
| 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-08 | STM: handle "Time Abort" correctly (Closes: 3332) | Enrico Tassi | |
| 2014-06-08 | Function in Univ uselessly exported. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |