diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-03-20 16:30:41 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-03-20 16:30:41 +0000 |
| commit | 93e1bfa7327acadc6177aa8c3d5ad9e4af412efa (patch) | |
| tree | 4af265b60c05edb596667704a93e7317eec6a82d /tactics | |
| parent | 9c88406557b19ed348199c57b1f32b77c6fa3d8b (diff) | |
Fixes to make Ynot compile with the trunk:
- Choose one of the possible instances of an evar when considering
remaining unification constraints: otherwise we just do nothing and
some evars remain uninstantiated.
- Normalise the goal w.r.t. evars before subst, to avoid a double vision
problem: the substituted variable appears only in an instance of an evar
and when we try the rewrite it has been substituted making the dependency
disappear.
- Hack to correcly handle let-in annotations which are internalized as
casts: they're really typing constraints. Shouldn't we just change the
AST to have the type at rawconstr let-in nodes?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11998 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 3af4fa171..99767afc0 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1216,7 +1216,7 @@ let subst_one x gl = tclMAP introtac depdecls]) @ [tclTRY (clear [x;hyp])]) gl -let subst = tclMAP subst_one +let subst ids = tclTHEN tclNORMEVAR (tclMAP subst_one ids) let subst_all gl = let test (_,c) = |