From cbe17d1d7b5116edfaf3fedd74fe4636f08f0c70 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 4 Apr 2008 09:57:41 +0000
Subject: Protection de rewrite in contre le dépliage des constantes dans
 w_unify, ce qui n'était pas encore fait

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10750 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 28e35cf97b..08eddef96c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -931,7 +931,8 @@ 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 ~allow_K:false hypmv elimclause' hypclause in
+  let elimclause'' =
+    clenv_fchain ~allow_K:false ~flags:elim_flags 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" 
@@ -1959,7 +1960,7 @@ let compute_elim_sig ?elimc elimt =
   let nparams = Intset.cardinal (free_rels concl_with_args) in
   let preds,params = cut_list (List.length params_preds - nparams) params_preds in
   
-  (* A first approximation, further anlysis will tweak it *)
+  (* A first approximation, further analysis will tweak it *)
   let res = ref { empty_scheme with
     (* This fields are ok: *)
     elimc = elimc; elimt = elimt; concl = conclusion;
-- 
cgit v1.2.3