aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Collapse)Author
2016-05-13More informative error message when interpreting ltac variables in terms.Pierre-Marie Pédrot
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-05-04Moving the Val module to Geninterp.Pierre-Marie Pédrot
2016-05-04Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-03Use the canonical name when looking for an eliminator (bug #4670).Guillaume Melquiond
Disclaimer: I have no idea what I am doing.
2016-05-02Avoid infinite loop/stack overflow when using "simpl nomatch" (bug #4576).Guillaume Melquiond
When encountering a "simpl nomatch" constant, the reduction machinery tries to unfold it. If the subsequent partial reduction does not produce any match construct, it keeps going from the reduced term. Unfortunately, the reduced term has been refolded in the meantime, which means that some of the previous reduction steps have been canceled, thus causing an infinite loop. This patch delays the refolding till the very end, so that reduction always progresses. Disclaimer: I have no idea what I am doing here. The patch compiles the standard library and the test suite properly, so hopefully they contain enough tests to exercise the reduction machinery.
2016-05-02Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-29Fix incorrect cbv reduction of primitive projections. (Bug #4634)Guillaume Melquiond
As noticed by Cyprien Mangin, projected terms cannot directly be used as head values. Indeed, they might be applications (e.g. constructors as in the bug report) whose arguments would thus be missing from the evaluation stack when doing any iota-reduction step. The only case where it would make sense is when the evaluation stack is empty, as an optimization. Indeed, in that case, the arguments are put on the stack, and then immediately put back inside the term.
2016-04-27Revert "When interpreting "match goal with ... end" in ltac, expand evars by"Hugo Herbelin
This reverts commit 7e613daf7c71a4180725bddb40151c2b5a6348f4.
2016-04-27Revert "More abstraction in cases.mli."Hugo Herbelin
This reverts commit 975e2a05050c704161aca3fbac96376eeda6fb4a.
2016-04-27Revert "Add support for generalization also on named variables in ↵Hugo Herbelin
pattern-matching" This reverts commit be80899499094fc8a15362931e3cec650f2fb14e.
2016-04-27Revert "Add support for deep dependencies in variables within the recursive ↵Hugo Herbelin
structure." This reverts commit eaca8dadf7dd8152a86f4fc75631754344268dbf.
2016-04-27Revert "Fixing a De Bruijn bug in computing return predicate by inversion."Hugo Herbelin
This reverts commit 94e9e28ebaa33e11164ca07f225d998ca7f8e52c.
2016-04-27Revert "Using existing names as a basis for the inner names of the ↵Hugo Herbelin
pattern-matching produced by an implicit "in" clause" This reverts commit ba9f53314ff6132d0013e53879395e0dc9d8038c.
2016-04-27Revert "Vers un filtrage profond ..."Hugo Herbelin
This reverts commit d9f0daefb437955df8102de2b3c4c31749b6946e.
2016-04-27Vers un filtrage profond ...Hugo Herbelin
2016-04-27Using existing names as a basis for the inner names of the pattern-matching ↵Hugo Herbelin
produced by an implicit "in" clause
2016-04-27Fixing a De Bruijn bug in computing return predicate by inversion.Hugo Herbelin
2016-04-27Add support for deep dependencies in variables within the recursive structure.Hugo Herbelin
2016-04-27Add support for generalization also on named variables in pattern-matchingHugo Herbelin
algorithm.
2016-04-27More abstraction in cases.mli.Hugo Herbelin
2016-04-27When interpreting "match goal with ... end" in ltac, expand evars byHugo Herbelin
need at matching time rather than eagerly at the beginning of the call to "match". To be done for other constructs too, e.g. "match term with ... endp".
2016-04-27Fixing a "This clause is redundant" error when interpreting the "in"Hugo Herbelin
clause of a "match" over an irrefutable pattern.
2016-04-27Optimization in building a return clause by pattern-matching: do notHugo Herbelin
build a default case if the pattern is irrefutable. It did not matter in practice because we did not check for unused clauses in this case.
2016-04-25Merging the ML tactic notation and plain Tactic Notation mechanisms.Pierre-Marie Pédrot
2016-04-24Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-19Fixing #4677 (collision of a global variable and of a local variableHugo Herbelin
while eta-expanding a notation) + a more serious variant of it (alpha-conversion incorrect wrt eta-expansion).
2016-04-04Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq ↵Matthieu Sozeau
into JasonGross-trunk-function_scope
2016-03-30Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-25Moving type_uconstr to Pretyping.Pierre-Marie Pédrot
2016-03-25Fix a bug in Program coercion codeMatthieu Sozeau
It was not accounting for the universe constraints generated by applications of the coercion.
2016-03-20Moving Evarutil and Proofview to engine/Pierre-Marie Pédrot
2016-03-20Making Evarutil independent from Reductionops.Pierre-Marie Pédrot
2016-03-20Splitting Evarutil in two distinct files.Pierre-Marie Pédrot
Some parts of Evarutils were related to the management of evars under constraints. We put them in the Evardefine file.
2016-03-20Pushing Proofview further down the dependency alley.Pierre-Marie Pédrot
2016-03-20Moving Proofview to pretyping/.Pierre-Marie Pédrot
2016-03-20Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-18Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-17Fix #4623: set tactic too weak with universes (regression)Maxime Dénès
The regression was introduced by efa1c32a4d178, which replaced unification by conversion when looking for more occurrences of a subterm. The conversion function called was not the right one, as it was not inferring constraints.
2016-03-16Fix incorrect behavior of CS resolutionMatthieu Sozeau
Due to a change in pretyping, using cast annotations as typing constraints, the canonical structure problems given to the unification could contain non-evar-normalized terms, hence we force evar normalization where necessary to ensure the same CS solutions can be found. Here the dependency test is fooled by an erasable dependency, and the following resolution needs a independent codomain for pop b to be well-scoped.
2016-03-15Try eta-expansion of records only on non-recursive onesMatthieu Sozeau
2016-03-14Try eta-expansion of records only on non-recursive onesMatthieu Sozeau
2016-03-10Primitive projections: protect kernel from erroneous definitions.Matthieu Sozeau
E.g., Inductive foo := mkFoo { bla : foo } allowed to define recursive records with eta for which conversion is incomplete. - Eta-conversion only applies to BiFinite inductives - Finiteness information is now checked by the kernel (the constructor types must be strictly non recursive for BiFinite declarations).
2016-03-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-09Fix strategy of Keyed UnificationMatthieu Sozeau
Try first to find a keyed subterm without conversion/betaiota on open terms (that is the usual strategy of rewrite), if this fails, try with full conversion, incuding betaiota. This makes the test-suite pass again, retaining efficiency in the most common cases.
2016-03-05Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-28Slightly contracting code of evarconv.ml.Hugo Herbelin
2016-02-23Fix part of bug #4533: respect declared global transparency ofMatthieu Sozeau
projections in unification.ml
2016-02-19Adding location to universes generated by the pretyper.Pierre-Marie Pédrot
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 07:34:43 +0000