From f9d7ccaf40f7f21ce0630c9b668581249a635de9 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 12 Oct 2007 13:36:02 +0000
Subject: 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
---
 pretyping/clenv.ml  | 4 ++--
 pretyping/clenv.mli | 3 ++-
 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" 
-- 
cgit v1.2.3