diff options
| author | herbelin | 2008-04-04 16:25:05 +0000 |
|---|---|---|
| committer | herbelin | 2008-04-04 16:25:05 +0000 |
| commit | bc8728f0762f7e39f779c677679a8bc351a4290a (patch) | |
| tree | b8a131508fcd4bc0ca131d4032788316b08b6997 /pretyping/unification.ml | |
| parent | 2814afbbd4803216ad4cb6af9ec5d86fce71e8eb (diff) | |
- Relâchement de la contrainte de bonne longueur des intropatterns
lorsqu'en position terminale (en fait, l'idéal serait de pouvoir
mettre des tactiques dans les branches, style "intros [H ; tac | ]")
(cf un exemple QvMake.v)
- Pas de delta du tout quand on fait de la recherche de sous-terme
(même lorsqu'on vient de apply avec une conclusion ?P t) (cf un
exemple dans Rocq/DEMOS/Sorting.v)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10755 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 3ef17778a9..b1a4c3b8c7 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -633,6 +633,8 @@ let w_unify_to_subterm_list env flags allow_K oplist t evd = (evd,[]) let secondOrderAbstraction env flags allow_K typ (p, oplist) evd = + (* Remove delta when looking for a subterm *) + let flags = { flags with modulo_delta = Cpred.empty } in let (evd',cllist) = w_unify_to_subterm_list env flags allow_K oplist typ evd in let typp = Typing.meta_type evd' p in |