aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-03-28Patterns: Accepting patterns in PFix and PCofix and not only constr.Hugo Herbelin
2018-03-28Adding Array.fold_left4.Hugo Herbelin
2018-03-28Detyping: Adding a variant of share_names for patterns.Hugo Herbelin
2018-03-28Detyping: Making detype_fix/detype_cofix polymorphic combinator (step 1).Hugo Herbelin
2018-03-28Patternops: renaming an internal function to more closely match its effect.Hugo Herbelin
2018-03-28Glob_ops: cosmetic renaming to reflect the type of objects.Hugo Herbelin
2018-03-28Getting rid of some false "collision between bound variable names" warnings.Hugo Herbelin
- In a situation like "match x with ... end" with no "return" clause we don't warn for the implicit "as x" coming from repeating "x" - In a multiple fixpoint, we don't warn for the recursive context being distributed several times over the different mutual components.
2018-03-28Fix #7101: STM delegation policy brokenMaxime Dénès
I make here a minimal fix, but a lot of cleaning should be done around Aux_file handling, including removing some code from the kernel.
2018-03-28[api] Deprecate a couple of aliases that we missed.Emilio Jesus Gallego Arias
2018-03-28Merge PR #7090: stm: don't propagate side effects when editing a proofEmilio Jesus Gallego Arias
2018-03-28coqide: avoid marking sentences that are not in the document anymoreEnrico Tassi
2018-03-28Merge PR #6961: [test-suite] Add backtracking test for `Load`.Enrico Tassi
2018-03-27stm: don't propagate side effects when editing a proofEnrico Tassi
2018-03-27Adding tacticals tclBINDFIRST/tclBINDLAST.Hugo Herbelin
Design choice: Failing with an anomaly or with a catchable Ltac error "Fail": we fail with a Fail as it was the case with the related constrained version of tclTHENFIRST/tclTHENLAST.
2018-03-27Export Proofview.undefined as "unsafe" primitive.Hugo Herbelin
2018-03-27Adding informative variant of shelve_unifiable returning set of shelved evars.Hugo Herbelin
2018-03-27Congruence: Fixing a bug with native projections.Hugo Herbelin
There is a code to turn constants denoting projections into proper primitive projections, but it did not drop parameters. The code seems anyway redundant with an "expand_projections" which is already present in Cctac.decompose_term. After removal of this code, the two calls to congruence added to cc.v work.
2018-03-27Congruence: typography in a comment.Hugo Herbelin
2018-03-27Congruence: getting rid of a detour by the compatibility layer of proof engine.Hugo Herbelin
The V82 compatibility layer of the proof engine was used by cc (congruence closure) for the sole purpose of maintaining an environment and a sigma. We inline the corresponding env and sigma in the state of cc algorithm to get rid of the compatibility layer.
2018-03-27[default.nix] Unpin nixpkgsMaxime Dénès
Sphinx dependencies are now available in unstable channel
2018-03-27Merge PR #6835: Deprecate undocumented "intros until 0" in favor of "intros *"Pierre-Marie Pédrot
2018-03-27Merge PR #7062: Slightly refining some error messages about unresolvable evars.Pierre-Marie Pédrot
2018-03-27Expliciting and taking advantage of a representation invariant in Esubst.Pierre-Marie Pédrot
2018-03-27Adding a fiat-parser overlayHugo Herbelin
2018-03-27Fixing #5547 (typability of return predicate in nested pattern-matching).Hugo Herbelin
Answering to commit about #5500: we don't know in general if the return predicate T(y1,..,yn,x) in the intermediate step of a nested pattern-matching is a sort, but we don't even know if it is well-typed: retyping is not enough, we need full typing.
2018-03-27Fixing #5500 (missing test in return clause of match leading to anomaly).Hugo Herbelin
This is a quick fix to check in nested pattern-matching that the return clause is typed by an arity (there was already a check when the return clause was given explicitly - in the 3rd section of prepare_predicate -; it was automatically typed by a sort when the return clause was coming by pattern-matching with the type constraint, since the type constraint is a type; but it was not done when the predicate was derived from a former predicate in nested pattern-matching). Indeed, in nested pattern-matching, we know that the return predicate has the form λy1..yn.λx:I(y1,..,yn).T(y1,..,yn,x) and we know that T(v1,...,vn,u) : Type for the effective u:I(v1,..,vn) we are matching on, but we don't know if T(y1,..,yn,x) is itself a sort (e.g. it can be a "match" which reduces to a sort when instantiated with v1..vn, but whose evaluation remains blocked when the y1..yn are variables). Note that in the bug report, the incorrect typing is produced by small inversion. In practice, we can raise the anomaly also without small inversion, so we fix it in the general case. See file 5500.v for details.
2018-03-27Fix printing of toplevel record values.Pierre-Marie Pédrot
2018-03-27Fixup strict mode for patternsPierre-Marie Pédrot
2018-03-26Fixes #7011 (Fix/CoFix were not considered in tactic unification).Hugo Herbelin
2018-03-26[doc] Port Chapter 20 Type Classes to SphinxMatthieu Sozeau
2018-03-26Merge PR #6739: Tentative fix for #6520: camlcity.org unresponsive makes ↵Maxime Dénès
AppVeyor fail.
2018-03-26Move Classes.tex to type-classes.rstMatthieu Sozeau
2018-03-26Merge PR #6970: [vernac] Move `Quit` and `Drop` to the toplevel layer.Enrico Tassi
2018-03-26Add Michael Soegtrop as a code owner for Windows build scripts.Théo Zimmermann
2018-03-26Use Pierre Corbineau GitHub nickname in CODEOWNERS.Théo Zimmermann
2018-03-26More efficient reallocation of VM global tables.Pierre-Marie Pédrot
The previous code was mimicking what the C implementation was doing, which was a quadratic algorithm. We simply use the good old exponential reallocation strategy that is amortized O(1).
2018-03-26Moving the VM global atom table to a ML reference.Pierre-Marie Pédrot
2018-03-26Moving the VM global data to a ML reference.Pierre-Marie Pédrot
2018-03-25Clarify wording in tactics documentation.Théo Zimmermann
Closes #6980.
2018-03-24Slightly refining some error messages about unresolvable evars.Hugo Herbelin
For instance, error in "Goal forall a f, f a = 0" is now located.
2018-03-23Deprecate undocumented "intros until 0" in favor of "intros *".Hugo Herbelin
- The case 0 makes the code of intros until (and in particular of Detyping.lookup_quantified_hypothesis_as_displayed more complicated). - The introduction pattern "*" is compositional while "until 0" is not.
2018-03-23Merge PR #7046: Switch maintainers for documentationThéo Zimmermann
2018-03-23Merge PR #7018: Fix typo in CHANGES.Maxime Dénès
2018-03-23Merge PR #7029: improve merge-pr scriptMaxime Dénès
2018-03-23improve merge-pr scriptEnrico Tassi
The script now performs many more checks and reports errors in a more intelligible way.
2018-03-23Merge PR #7052: More precise wording about the merge process.Théo Zimmermann
2018-03-23More precise wording about the merge process.Maxime Dénès
In particular, don't use the GitHub interface. Also, not all reviews are mandatory in some corner cases.
2018-03-23Merge PR #7028: Fix #7026: ssr: applying an overloaded lemma as a view takes ↵Enrico Tassi
too long.
2018-03-23Merge PR #6968: [stm] Never consider `Backtrack` as part of the script.Enrico Tassi
2018-03-23Merge PR #7025: Coq makefile: provide variables to extend the flags passed ↵Enrico Tassi
to coq, coqchk, coqdoc
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-30 00:34:27 +0000