aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2014-06-16Checking that a library name is valid before compilation.Pierre-Marie Pédrot
Fixes bug #3333.
2014-06-16Unification in HoTT_coq_061.v was looping with previous commit (whileHugo 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-16Fixing 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-16HoTT bug #29 is fixed, using the correct notion of polymorphic product types.Matthieu Sozeau
2014-06-16Fix spacing in error message.Guillaume Melquiond
2014-06-16Preemptively 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-15Fix test-suite fileMatthieu Sozeau
2014-06-15Change Ltac constr matching semantics to consider universes when merging twoMatthieu Sozeau
bindings of the same variable (fixing HoTT bug #52). Document the unification of universes in Ltac/tactics.
2014-06-15The 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-15Remove 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-13Fix 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-13HoTT/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-13Deprecate useless option -quality.Guillaume Melquiond
2014-06-13Remove documentation for the unsupported options -byte and -opt.Guillaume Melquiond
2014-06-13Deprecate useless option -unsafe.Guillaume Melquiond
2014-06-13Deprecate 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-13Less ocaml warnings.Hugo Herbelin
2014-06-13Improving tclWITHHOLES which did not see undefined evars up toHugo 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-13Fixing "clear" in internal_cut_replace: forbid dependencies in theHugo Herbelin
name of replaced hypothesis.
2014-06-13Improved error message when a meta posed as an evar remains unsolvedHugo Herbelin
in case prefix 'e' of "apply" and co is not given.
2014-06-13Check resolution of Metas turned into Evars by pose_all_metas_as_evarsHugo Herbelin
in unification.ml in case prefix 'e' of "apply" and co is not given.
2014-06-13Fixing wrong environment for Meta's in pose_all_metas_as_evars (bug #3284).Hugo Herbelin
2014-06-13Adapt simpl/cbn unfolding and refolding machinery to projections, so thatMatthieu Sozeau
primitive projections obey the Arguments command.
2014-06-12Code cleaning in Univ.Pierre-Marie Pédrot
2014-06-12Passing some tactics to the new monad type.Pierre-Marie Pédrot
2014-06-11Fix bug #3291, stack overflow in rewrite.Matthieu Sozeau
2014-06-11Fix bug #3289Matthieu Sozeau
2014-06-11Move bug # 3368 to closed bugsMatthieu Sozeau
2014-06-11Merge branch 'more-test-suite' of https://github.com/JasonGross/coq into trunkMatthieu 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-11In 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-11fix 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-10Add many more cases to the test-suiteJason 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-10Move closed bug 3314Jason Gross
2014-06-10Add a test-case for bug #3314 proving FalseJason Gross
2014-06-10Fixing Sorting Universes in a world where le and lt constraints may bePierre-Marie Pédrot
redundant in canonical arcs.
2014-06-10Compute the trace of a universe inconsistency only when explicitly requiredPierre-Marie Pédrot
by the printing options (i.e. when "Print Universes" is set).
2014-06-10Made explanations for universe inconsistencies optional. They are only usedPierre-Marie Pédrot
by the printer anyway.
2014-06-10Specialize the type of [Univ.compare_neq] so that it is clear it is only usedPierre-Marie Pédrot
to recover the trace of a universe inconsistency. Changed its name too btw.
2014-06-10Removing dead code in checker/univ.ml.Pierre-Marie Pédrot
2014-06-10Removing explanations of universe inconsistencies from the checker. TheyPierre-Marie Pédrot
were never used and were responsible for code duplication.
2014-06-10Imperatively check touched universes in compare_neq functions. This ensuresPierre-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-10Providing 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-10Oops, one refactoring was not compiled.Matthieu Sozeau
2014-06-10More cleanup/reorganizing of univ.ml to separate constraint/universe ↵Matthieu Sozeau
handling from the instance/contexts and substitution code.
2014-06-10Fix module order in printers.mllibMatthieu Sozeau
2014-06-10Cleanup 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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 06:59:50 +0000