| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
| |
This was broken by the attempt to use the same algorithm for rewriting
closed subterms than for rewriting subterms with evars: the algorithm
to find subterms (w_unify_to_subterm) did not go through evars. But
what to do when looking say, for a pattern "S ?n" in a goal "S ?x[a:=S ?y]"?
Should we unify ?x[a:=S ?y] with ?n or consider ?x as rigid and look
in the instance? If we adopt the first approach, then, what to do when
looking for "S ?n" in a goal "?x[a:=S ?y]"? Failing? Looking in the
instance? Is it normal that an evar behaves as a rigid constant when
it cannot be unified with the pattern?
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
while before these were supposed to consider only syntactically.
Made the experiment to unify with all delta flags unset. Keeping the
same flags as for non evar/meta free subterms would lead to too much
successes, as e.g. "true && b" matching "b" when the
modulo_conv_on_closed_terms flag is set, which is the case for
rewrite. But maybe should we instead investigate to have the same
flags but with the restrict_conv_on_strict_subterms flag set. This
rules out examples like "true && b" unifying with "b" and this is
another option which is ok for compiling the stdlib without any
changes.
|
| |
|
|
| |
was rightly failing.
|
| |
|
|
|
| |
works in the presence of local definitions referring to x and
dependent in other hyps or concl.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
in r14199 (June 2011). Meta's implicitly depend on the context they are
defined in and this has to be taken into account for checking if
occurrences are distinct (in particular, no Var's are allowed as
arguments of a pattern-unifiable Meta). The example expected to be
accepted thanks to r14199 is not a pattern-unification problem (it has
more than one solution) and was anyway already accepted (strange).
Compared to before r14199, aliases expansion and restriction of
pattern unification check to variables occurring in the right-hand
side are however now taken into account.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14642 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
| |
evars when rewriting. Use it for autorewrite and subst. Accept evars
instantiation in multi_rewrite so that rewrite alone remains
compatible (it is used in contribs, e.g. Godel, in places where it
does not seem absurd to allow it), but there are no good reason for
it. Comments welcome.
+ addition of some tests for rewriting (one being related to commit 14217)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14222 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
| |
proof of Chung-Kil's Hur Heq package): conversion in "trivial_unify"
accepted evars as ordinary variables. I hope I did not invalidate some
features that would have needed restricting conversion on evar-free
terms, but since failure of conversion in presence of evars is redirected
to the main unification algorithm, I guess it is OK.
For better readibility, I also inlined and cleaned a bit trivial_unify.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13193 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
(expected goal was not correct for rewriting in hypotheses)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12580 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Cleaning and uniformisation in command.ml:
- For better modularity and better visibility, two files got isolated
out of command.ml:
- lemmas.ml is about starting and saving a proof
- indschemes.ml is about declaring inductive schemes
- Decomposition of the functions of command.ml into a functional part
and the imperative part
- Inductive schemes:
- New architecture in ind_tables.ml for registering scheme builders,
and for sharing and generating on demand inductive schemes
- Adding new automatically generated equality schemes (file eqschemes.ml)
- "_congr" for equality types (completing here commit 12273)
- "_rew_forward" (similar to vernac-level eq_rect_r), "_rew_forward_dep",
"_rew_backward" (similar to eq_rect), "_rew_backward_dep" for
rewriting schemes (warning, rew_forward_dep cannot be stated following
the standard Coq pattern for inductive types: "t=u" cannot be the
last argument of the scheme)
- "_case", "_case_nodep", "_case_dep" for case analysis schemes
- Preliminary step towards discriminate and injection working on any
equality-like type (e.g. eq_true)
- Restating JMeq_congr under the canonical form of congruence schemes
- Renamed "Set Equality Scheme" into "Set Equality Schemes"
- Added "Set Rewriting Schemes", "Set Case Analysis Schemes"
- Activation of the automatic generation of boolean equality lemmas
- Partial debug and error messages improvements for the generation of
boolean equality and decidable equality
- Added schemes for making dependent rewrite working (unfortunately with
not a fully satisfactory design - see file eqschemes.ml)
- Some names of ML function made more regular (see dev/doc/changes.txt)
- Incidentally, added a flush to obsolete Local/Global syntax warning
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12481 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
Correction bugs commentaires pour coqdoc (ChoiceFacts.v)
Test-suite
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10756 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9666 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6260 85f007b7-540e-0410-9357-904b9bb8a0f7
|
Hugo Herbelin
Matthieu Sozeau
herbelin