From 18ffccadd1901e666ea3600263454446f52849d8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 9 Dec 2002 08:40:00 +0000
Subject: Ajout Simpl et Change sur des sous-termes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3392 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/setoid_replace.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/setoid_replace.ml')

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index fa62c8dd46..fd57bce87f 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -636,7 +636,7 @@ and zapply is_r gl gl_m c1 c2 hyp glll = (match ((kind_of_term gl), gl_m) with
 	then
 	  let m = morphism_table_find fleche_constr in
 	  let args = Array.of_list (create_args al a m.profil c1 c2) in  
-	    tclTHEN (change_in_concl new_concl)
+	    tclTHEN (change_in_concl None new_concl)
 	      (tclTHENS (apply (mkApp (m.lem, args)))
 		 ((create_tac_list 0 a al c1 c2 hyp m.arg_types m.profil)@[unfold_constr (ConstRef fleche_cp)]))
 (*		 ((create_tac_list 0 a al c1 c2 hyp m.arg_types m.profil)@[tclIDTAC])) *)
-- 
cgit v1.2.3