diff options
| author | herbelin | 2008-02-07 21:49:05 +0000 |
|---|---|---|
| committer | herbelin | 2008-02-07 21:49:05 +0000 |
| commit | 62091e13412cce60ca32aba542b146f0fe8403e1 (patch) | |
| tree | 13f5e42841568f01548f0d08332d4823456cb66e /pretyping/clenv.ml | |
| parent | 3c9fe09ad4cdba24b906658cb14df0b44ed634a2 (diff) | |
Mise en place d'une toute petite amélioration de l'unification de
apply : si on a trouvé une méta, alors, on l'utilise pour instancier
les trous lors de la tentative de conversion modulo delta. Cela permet
ainsi de résoudre de petits cas d'unification, tel que celui annoncé
échouant dans le "beginner question" du 6 fevrier 2008 de coq-club.
Solde au passage de modifs cosmétiques de setoid_replace.ml avant
abandon probable du code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10523 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/clenv.ml')
| -rw-r--r-- | pretyping/clenv.ml | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index b9881aaf04..18a22e5c71 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -241,18 +241,19 @@ let clenv_missing ce = clenv_dependent true ce (******************************************************************) -let clenv_unify allow_K cv_pb t1 t2 clenv = - { clenv with evd = w_unify allow_K clenv.env cv_pb t1 t2 clenv.evd } +let clenv_unify allow_K ?(flags=default_unify_flags) cv_pb t1 t2 clenv = + { clenv with + evd = w_unify allow_K ~flags:flags clenv.env cv_pb t1 t2 clenv.evd } -let clenv_unify_meta_types clenv = - { clenv with evd = w_unify_meta_types clenv.env clenv.evd } +let clenv_unify_meta_types ?(flags=default_unify_flags) clenv = + { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd } -let clenv_unique_resolver allow_K clenv gl = +let clenv_unique_resolver allow_K ?(flags=default_unify_flags) clenv gl = if isMeta (fst (whd_stack clenv.templtyp.rebus)) then - clenv_unify allow_K CUMUL (clenv_type clenv) (pf_concl gl) - (clenv_unify_meta_types clenv) + clenv_unify allow_K CUMUL ~flags:flags (clenv_type clenv) (pf_concl gl) + (clenv_unify_meta_types ~flags:flags clenv) else - clenv_unify allow_K CUMUL + clenv_unify allow_K CUMUL ~flags:flags (meta_reducible_instance clenv.evd clenv.templtyp) (pf_concl gl) clenv (* [clenv_pose_dependent_evars clenv] |