diff options
| author | herbelin | 2007-10-12 13:36:02 +0000 |
|---|---|---|
| committer | herbelin | 2007-10-12 13:36:02 +0000 |
| commit | f9d7ccaf40f7f21ce0630c9b668581249a635de9 (patch) | |
| tree | 659d29f45c32211ef8bd012353d9100514932c1e | |
| parent | 5c0beed3886749f7beb1227e8b321828eeae57a1 (diff) | |
Uniformisation du comportement de rewrite et rewrite in : quand le
filtrage d'ordre 2 échoue à trouver un prédicat de réécriture qui
n'est pas une K-abstraction, les deux rewrite essaie alors le filtrage
d'ordre 1. Ce n'est pas le plus élégant mais c'est la solution
uniforme permettant d'être conservatif.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10221 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/clenv.ml | 4 | ||||
| -rw-r--r-- | pretyping/clenv.mli | 3 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
3 files changed, 5 insertions, 4 deletions
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index 793ac2c32b..2d26e5bb14 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -302,7 +302,7 @@ let connect_clenv gls clenv = In particular, it assumes that [env'] and [sigma'] extend [env] and [sigma]. *) -let clenv_fchain mv clenv nextclenv = +let clenv_fchain ?(allow_K=true) mv clenv nextclenv = (* Add the metavars of [nextclenv] to [clenv], with their name-environment *) let clenv' = { templval = clenv.templval; @@ -312,7 +312,7 @@ let clenv_fchain mv clenv nextclenv = env = nextclenv.env } in (* unify the type of the template of [nextclenv] with the type of [mv] *) let clenv'' = - clenv_unify true CUMUL + clenv_unify allow_K CUMUL (clenv_nf_meta clenv' nextclenv.templtyp.rebus) (clenv_meta_type clenv' mv) clenv' in diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index 73a171b8d3..8546a44ef3 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -61,7 +61,8 @@ val mk_clenv_type_of : evar_info sigma -> constr -> clausenv (* linking of clenvs *) val connect_clenv : evar_info sigma -> clausenv -> clausenv -val clenv_fchain : metavariable -> clausenv -> clausenv -> clausenv +val clenv_fchain : + ?allow_K:bool -> metavariable -> clausenv -> clausenv -> clausenv (***************************************************************) (* Unification with clenvs *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index cffe550afc..c2dea3dadf 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -903,7 +903,7 @@ let elimination_in_clause_scheme with_evars id elimclause indclause gl = let hyp = mkVar id in let hyp_typ = pf_type_of gl hyp in let hypclause = mk_clenv_from_n gl (Some 0) (hyp, hyp_typ) in - let elimclause'' = clenv_fchain hypmv elimclause' hypclause in + let elimclause'' = clenv_fchain ~allow_K:false hypmv elimclause' hypclause in let new_hyp_typ = clenv_type elimclause'' in if eq_constr hyp_typ new_hyp_typ then errorlabstrm "general_rewrite_in" |