aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-06-14-async-proofs-delegation-threshold default value set to 0.03Enrico Tassi
Documentation also updated.
2016-06-14Merge remote-tracking branch 'origin/pr/182' into trunkEnrico Tassi
2016-06-14Merge branch 'bug4725' into v8.5Matthieu Sozeau
2016-06-14Admitted: fix #4818 return initial stmt and univsMatthieu Sozeau
2016-06-14test-suiet: run fake_id as before pr/173 was mergedEnrico Tassi
2016-06-14configure: use ln on linux and cp on windowsEnrico Tassi
2016-06-14Merge remote-tracking branch 'origin/pr/173' into trunkEnrico Tassi
This is the "error resiliency" mode for STM
2016-06-14Ident selectors cannot be used inside an Ltac expression.Cyprien Mangin
They can still be used at the toplevel.
2016-06-14Goal selectors are now tacticals and can be used as such.Cyprien Mangin
This allows to write things like this: split; 2: intro _; exact I or like this: eexists ?[x]; ?[x]: exact 0; trivial This has the side-effect on making the '?' before '[x]' mandatory.
2016-06-14Remove the need for brackets in goal selectors.Cyprien Mangin
2016-06-14Fix a typo in proofs/proofview.mli.Cyprien Mangin
2016-06-14Fix usage of Pervasives in goal selectors.Cyprien Mangin
2016-06-14Add a comment about the use of a zipper, for clarity.Cyprien Mangin
2016-06-14Fix the pretty-printing of goal range selectors.Cyprien Mangin
2016-06-14Add a [CList.partitioni] function.Cyprien Mangin
2016-06-14Add test-suite file for goal selectors.Cyprien Mangin
2016-06-14Add goal range selectors.Cyprien Mangin
You can now write [[1, 3-5]:tac.] to apply [tac] on the subgoals numbered 1 and 3 to 5.
2016-06-14Merge branch "LtacProf for trunk" (PR #165).Pierre-Marie Pédrot
2016-06-14Commenting out debugging code.Pierre-Marie Pédrot
2016-06-14Correct use of printing primitives.Pierre-Marie Pédrot
2016-06-14Better coding style (semantics).Pierre-Marie Pédrot
2016-06-14Better coding style (syntax).Pierre-Marie Pédrot
2016-06-14Adding Coq headers.Pierre-Marie Pédrot
2016-06-14Moving back Ltac profiling to the Ltac folder.Pierre-Marie Pédrot
2016-06-14Merge remote-tracking branch 'github/evarunsafe' into trunkMatthieu Sozeau
2016-06-14Moving UTF-8 related functions to Unicode module.Pierre-Marie Pédrot
2016-06-13Revert "Strip some trailing spaces"Pierre-Marie Pédrot
This reverts commit 45748e4efae8630cc13b0199dfcc9803341e8cd8.
2016-06-13Univs: more robust Universe/Constraint decls #4816Matthieu Sozeau
This fixes the declarations of constraints, universes and assumptions: - global constraints can refer to global universes only, - polymorphic universes, constraints and assumptions can only be declared inside sections, when all the section's variables/universes are polymorphic as well. - monomorphic assumptions may only be declared in section contexts which are not parameterized by polymorphic universes/assumptions. Add fix for part 1 of bug #4816
2016-06-13Fix test-suite file, only part 2 is fixed in 8.5Matthieu Sozeau
2016-06-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-06-13Univs: fix for part #2 of bug #4816.Matthieu Sozeau
Check that the polymorphic status of everything that is parameterized in nested sections is coherent.
2016-06-13STM classification: VernacTimeout may contain an "internal command".Maxime Dénès
2016-06-13Print Assumptions and co. can "pierce opacity".Maxime Dénès
2016-06-13evar_conv: Refine occur_rigidlyMatthieu Sozeau
This avoids postponing constraints which will surely produce an occur-check and allow to backtrack on first-order unifications producing those constraints directly (e.g. to apply eta). (fixes HoTT/HoTT with 8.5).
2016-06-13Tentatively fixing misguiding error message with "binder" type inHugo Herbelin
non-recursive notations (#4815).
2016-06-12For the record, an example one would like to see working.Hugo Herbelin
2016-06-12Minor simplification in evarconv.Hugo Herbelin
Function default_fail was always part of an ise_try. Its associated error message was anyway thrown away. It is then irrelevant and could be made simpler.
2016-06-12Another fix to #4782 (a typing error not captured when dealing with bindings).Hugo Herbelin
The tentative fix in f9695eb4b (which I was afraid it might be too strong, since it was implying failing more often) indeed broke other things (see #4813).
2016-06-12Reserve exception "ConversionFailed" in unification for failure ofHugo Herbelin
conversion on closed terms. This will be useful to discriminate problems involving the "with" clause and which fails by lack of information or for deeper reasons.
2016-06-12Protecting eta-expansion in evarconv.ml against ill-typed problems.Hugo Herbelin
This can happen with the "with" clause (see e.g. #4782), but also with recursive calls in first-order unification (e.g. "?n a a b = f a" when a matching between "b" and "a" is tried before expanding f).
2016-06-12Fixing bug in printing CannotSolveConstraint (collision of context names).Hugo Herbelin
2016-06-11Fixing #4782 (a typing error not captured when dealing with bindings).Hugo Herbelin
Trying to now catch all unification errors, but without a clear view at whether some errors could be tolerated at the point of checking the type of the binding.
2016-06-11Fixing a try with in apply that has become too weak in 8.5.Hugo Herbelin
Don't know however what should be the right guard to this try. Now using catchable_exception, but even in 8.4, Failure was caught, which is strange.
2016-06-10Merge branch 'pack-plugins'Pierre Letouzey
2016-06-10coq_makefile: oups, a missing ; in my previous commitPierre Letouzey
2016-06-10coq_makefile: fix a crucial typo in e9c57a3Pierre Letouzey
2016-06-10coq_makefile: short display of COQC and COQDEP (follow-up of e9c57a3)Pierre Letouzey
2016-06-10A mini-optimization for free in unification.ml: test in O(1)Hugo Herbelin
complexity comes before tests in O(n) complexity.
2016-06-09Reporting about a few bug fixes (to be continued).Hugo Herbelin
2016-06-09newring: fix for hack using evars as integers.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-01 05:07:20 +0000