Imported Upstream version 8.1~gammaupstream/8.1.gamma

1 files changed, 257 insertions, 246 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index f05c3882..2526c84e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: equality.ml 9010 2006-07-05 07:17:41Z jforest $ *)
+(* $Id: equality.ml 9211 2006-10-05 12:38:33Z letouzey $ *)
 
 open Pp
 open Util
@@ -82,34 +82,34 @@ let elimination_sort_of_clause = function
 *)
 
 let general_rewrite_bindings_clause cls lft2rgt (c,l) gl =
-  let ctype = pf_type_of gl c in 
+  let ctype = pf_apply get_type_of gl c in 
   (* A delta-reduction would be here too strong, since it would 
      break search for a defined setoid relation in head position. *)
   let t = snd (decompose_prod (whd_betaiotazeta ctype)) in 
   let head = if isApp t then fst (destApp t) else t in 
-  if relation_table_mem head && l = NoBindings then 
-    general_s_rewrite_clause cls lft2rgt c [] gl
-  else 
-    (* Original code. In particular, [splay_prod] performs delta-reduction. *)
-    let env = pf_env gl in
-    let sigma = project gl in 
-    let _,t = splay_prod env sigma t in
-    match match_with_equation t with
-      | None -> 
-	  if l = NoBindings
-	  then general_s_rewrite_clause cls lft2rgt c [] gl
-	  else error "The term provided does not end with an equation" 
-      | Some (hdcncl,_) -> 
-          let hdcncls = string_of_inductive hdcncl in 
-	  let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in
-          let dir = if cls=None then lft2rgt else not lft2rgt in
-          let rwr_thm = if dir then hdcncls^suffix^"_r" else hdcncls^suffix in
-          let elim =
-	    try pf_global gl (id_of_string rwr_thm)
-            with Not_found ->
-              error ("Cannot find rewrite principle "^rwr_thm)
-          in 
-	  general_elim_clause cls (c,l) (elim,NoBindings) gl
+    if relation_table_mem head && l = NoBindings then 
+      general_s_rewrite_clause cls lft2rgt c [] gl
+    else 
+      (* Original code. In particular, [splay_prod] performs delta-reduction. *)
+      let env = pf_env gl in
+      let sigma = project gl in 
+      let _,t = splay_prod env sigma t in
+	match match_with_equation t with
+	  | None -> 
+	      if l = NoBindings
+	      then general_s_rewrite_clause cls lft2rgt c [] gl
+	      else error "The term provided does not end with an equation" 
+	  | Some (hdcncl,_) -> 
+              let hdcncls = string_of_inductive hdcncl in 
+	      let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in
+              let dir = if cls=None then lft2rgt else not lft2rgt in
+              let rwr_thm = if dir then hdcncls^suffix^"_r" else hdcncls^suffix in
+              let elim =
+		try pf_global gl (id_of_string rwr_thm)
+		with Not_found ->
+		  error ("Cannot find rewrite principle "^rwr_thm)
+              in 
+		general_elim_clause cls (c,l) (elim,NoBindings) gl
 
 let general_rewrite_bindings = general_rewrite_bindings_clause None
 let general_rewrite l2r c = general_rewrite_bindings l2r (c,NoBindings)
@@ -119,36 +119,39 @@ let general_rewrite_bindings_in l2r id =
 let general_rewrite_in l2r id c = 
   general_rewrite_bindings_clause (Some id) l2r (c,NoBindings)
 
-
 let general_multi_rewrite l2r c cl = 
-  let rec do_hyps = function 
-    | [] -> tclIDTAC
-    | ((_,id),_) :: l -> 
-	tclTHENFIRST (general_rewrite_bindings_in l2r id c) (do_hyps l)
-  in 
-  let rec try_do_hyps = function 
-    | [] -> tclIDTAC 
-    | id :: l -> 
-	tclTHENFIRST 
-	  (tclTRY (general_rewrite_bindings_in l2r id c)) 
-	  (try_do_hyps l)
-  in 
   if cl.concl_occs <> [] then 
-    error "The \"at\" syntax isn't available yet for the rewrite tactic"
-  else 
-    tclTHENFIRST 
-      (if cl.onconcl then general_rewrite_bindings l2r c else tclIDTAC)
-      (match cl.onhyps with 
-	 | Some l -> do_hyps l
-	 | None -> 
-	     fun gl -> 
-	       (* try to rewrite in all hypothesis 
-		  (except maybe the rewritten one) *)
-	       let ids = match kind_of_term (fst c) with 
-		 | Var id -> list_remove id (pf_ids_of_hyps gl)
-		 | _ -> pf_ids_of_hyps gl
-	       in try_do_hyps ids gl)
-
+    error "The \"at\" syntax isn't available yet for the rewrite/replace tactic"
+  else match cl.onhyps with 
+    | Some l -> 
+	(* If a precise list of locations is given, success is mandatory for
+	   each of these locations. *)
+	let rec do_hyps = function 
+	  | [] -> tclIDTAC
+	  | ((_,id),_) :: l -> 
+	      tclTHENFIRST (general_rewrite_bindings_in l2r id c) (do_hyps l)
+	in 
+	if not cl.onconcl then do_hyps l 
+	else tclTHENFIRST (general_rewrite_bindings l2r c) (do_hyps l)
+    | None -> 
+	(* Otherwise, if we are told to rewrite in all hypothesis via the 
+           syntax "* |-", we fail iff all the different rewrites fail *) 
+	let rec do_hyps_atleastonce = function 
+	  | [] -> (fun gl -> error "Nothing to rewrite.")
+	  | id :: l -> 
+	      tclIFTHENTRYELSEMUST 
+		(general_rewrite_bindings_in l2r id c) 
+		(do_hyps_atleastonce l)
+	in 
+	let do_hyps gl = 
+	  (* If the term to rewrite is an hypothesis, don't rewrite in itself *)
+	  let ids = match kind_of_term (fst c) with 
+	    | Var id -> list_remove id (pf_ids_of_hyps gl)
+	    | _ -> pf_ids_of_hyps gl
+	  in do_hyps_atleastonce ids gl
+	in 
+	if not cl.onconcl then do_hyps 
+	else tclIFTHENTRYELSEMUST (general_rewrite_bindings l2r c) do_hyps
 
 (* Conditional rewriting, the success of a rewriting is related 
    to the resolution of the conditions by a given tactic *)
@@ -182,9 +185,14 @@ let rewriteRL_clause = function
    tac : Used to prove the equality c1 = c2 
    gl : goal *)
 
-let abstract_replace clause c2 c1 unsafe tac gl =
-  let t1 = pf_type_of gl c1 
-  and t2 = pf_type_of gl c2 in
+let multi_replace clause c2 c1 unsafe try_prove_eq_opt gl = 
+  let try_prove_eq = 
+    match try_prove_eq_opt with 
+      | None -> tclIDTAC
+      | Some tac ->  tclTRY (tclCOMPLETE tac)
+  in
+  let t1 = pf_apply get_type_of gl c1 
+  and t2 = pf_apply get_type_of gl c2 in
   if unsafe or (pf_conv_x gl t1 t2) then
     let e = build_coq_eq () in
     let sym = build_coq_sym_eq () in
@@ -192,34 +200,28 @@ let abstract_replace clause c2 c1 unsafe tac gl =
     tclTHENS (assert_tac false Anonymous eq)
       [onLastHyp (fun id -> 
 	tclTHEN 
-	  (tclTRY (rewriteRL_clause clause (mkVar id,NoBindings)))
+	  (tclTRY (general_multi_rewrite false (mkVar id,NoBindings) clause))
 	  (clear [id]));
        tclFIRST
 	 [assumption;
 	  tclTHEN (apply sym) assumption;
-	  tclTRY (tclCOMPLETE tac)
+	  try_prove_eq
 	 ]
       ] gl
   else
     error "terms do not have convertible types"
+  
 
+let replace c2 c1 gl = multi_replace onConcl c2 c1 false None gl
 
-let replace c2 c1 gl = abstract_replace None c2 c1 false tclIDTAC gl
-
-let replace_in id c2 c1 gl = abstract_replace (Some id) c2 c1 false tclIDTAC gl
+let replace_in id c2 c1 gl = multi_replace (onHyp id) c2 c1 false None gl
 
-let replace_by c2 c1 tac gl = abstract_replace None c2 c1 false tac gl
+let replace_by c2 c1 tac gl = multi_replace onConcl c2 c1 false (Some tac) gl
 
-let replace_in_by id c2 c1 tac gl = abstract_replace (Some id) c2 c1 false tac gl
+let replace_in_by id c2 c1 tac gl = multi_replace (onHyp id) c2 c1 false (Some tac) gl
 
-
-let new_replace c2 c1 id tac_opt gl = 
-  let tac = 
-    match tac_opt with 
-      | Some tac -> tac 
-      | _ -> tclIDTAC
-  in
-  abstract_replace id c2 c1 false tac gl
+let replace_in_clause_maybe_by c2 c1 cl tac_opt gl = 
+  multi_replace cl c2 c1 false tac_opt gl
 
 (* End of Eduardo's code. The rest of this file could be improved
    using the functions match_with_equation, etc that I defined
@@ -269,24 +271,27 @@ exception DiscrFound of
   (constructor * int) list * constructor * constructor
 
 let find_positions env sigma t1 t2 =
-  let rec findrec posn t1 t2 =
+  let rec findrec sorts posn t1 t2 =
     let hd1,args1 = whd_betadeltaiota_stack env sigma t1 in
     let hd2,args2 = whd_betadeltaiota_stack env sigma t2 in
     match (kind_of_term hd1, kind_of_term hd2) with
   	
       | Construct sp1, Construct sp2 
           when List.length args1 = mis_constructor_nargs_env env sp1
-          ->
-        (* both sides are fully applied constructors, so either we descend,
-           or we can discriminate here. *)
+            ->
+	  let sorts = list_intersect sorts (allowed_sorts env (fst sp1)) in
+          (* both sides are fully applied constructors, so either we descend,
+             or we can discriminate here. *)
 	  if sp1 = sp2 then
+	    let nrealargs = constructor_nrealargs env sp1 in
+	    let rargs1 = list_lastn nrealargs args1 in
+	    let rargs2 = list_lastn nrealargs args2 in
             List.flatten
-	      (list_map2_i
-		 (fun i arg1 arg2 ->
-		    findrec ((sp1,i)::posn) arg1 arg2)
-		 0 args1 args2)
-	  else
-	    raise (DiscrFound(List.rev posn,sp1,sp2))
+	      (list_map2_i (fun i -> findrec sorts ((sp1,i)::posn))
+		0 rargs1 rargs2)
+	  else if List.mem InType sorts then (* see build_discriminator *)
+	    raise (DiscrFound (List.rev posn,sp1,sp2))
+	  else []
 
       | _ ->
 	  let t1_0 = applist (hd1,args1) 
@@ -295,14 +300,13 @@ let find_positions env sigma t1 t2 =
 	    []
           else
 	    let ty1_0 = get_type_of env sigma t1_0 in
-	    match get_sort_family_of env sigma ty1_0 with
-	      | InSet | InType -> [(List.rev posn,t1_0,t2_0)]
-	      | InProp -> []
-	  in 
-	  (try 
-	     Inr(findrec [] t1 t2)
-	   with DiscrFound (path,c1,c2) -> 
-	     Inl (path,c1,c2))
+	    let s = get_sort_family_of env sigma ty1_0 in
+	    if List.mem s sorts then [(List.rev posn,t1_0,t2_0)] else [] in 
+  try
+    (* Rem: to allow injection on proofs objects, just add InProp *)
+    Inr (findrec [InSet;InType] [] t1 t2)
+  with DiscrFound (path,c1,c2) ->
+    Inl (path,c1,c2)
 
 let discriminable env sigma t1 t2 =
   match find_positions env sigma t1 t2 with
@@ -371,6 +375,7 @@ let discriminable env sigma t1 t2 =
 
    the continuation then constructs the case-split.
  *)
+
 let descend_then sigma env head dirn =
   let IndType (indf,_) =
     try find_rectype env sigma (get_type_of env sigma head)
@@ -383,9 +388,7 @@ let descend_then sigma env head dirn =
   (dirn_nlams,
    dirn_env,
    (fun dirnval (dfltval,resty) ->
-      let arsign,_ = get_arity env indf in
-      let depind = build_dependent_inductive env indf in
-      let deparsign = (Anonymous,None,depind)::arsign in
+      let deparsign = make_arity_signature env true indf in
       let p =
 	it_mkLambda_or_LetIn (lift (mip.mind_nrealargs+1) resty) deparsign in
       let build_branch i =
@@ -416,7 +419,7 @@ let descend_then sigma env head dirn =
 
 let construct_discriminator sigma env dirn c sort =
   let IndType(indf,_) =
-    try find_rectype env sigma (type_of env sigma c)
+    try find_rectype env sigma (get_type_of env sigma c)
     with Not_found ->
        (* one can find Rel(k) in case of dependent constructors 
           like T := c : (A:Set)A->T and a discrimination 
@@ -428,10 +431,8 @@ let construct_discriminator sigma env dirn c sort =
 		 dependent types") in
   let (ind,_) = dest_ind_family indf in
   let (mib,mip) = lookup_mind_specif env ind in
-  let arsign,arsort = get_arity env indf in
   let (true_0,false_0,sort_0) = build_coq_True(),build_coq_False(),Prop Null in
-  let depind = build_dependent_inductive env indf in
-  let deparsign = (Anonymous,None,depind)::arsign in
+  let deparsign = make_arity_signature env true indf in
   let p = it_mkLambda_or_LetIn (mkSort sort_0) deparsign in
   let cstrs = get_constructors env indf in
   let build_branch i =
@@ -445,17 +446,22 @@ let construct_discriminator sigma env dirn c sort =
 let rec build_discriminator sigma env dirn c sort = function
   | [] -> construct_discriminator sigma env dirn c sort
   | ((sp,cnum),argnum)::l ->
-      let cty = type_of env sigma c in
-      let IndType (indf,_) =
-	try find_rectype env sigma cty with Not_found -> assert false in
-      let (ind,_) = dest_ind_family indf in
-      let (mib,mip) = lookup_mind_specif env ind in
-      let nparams = mib.mind_nparams  in
       let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in
-      let newc = mkRel(cnum_nlams-(argnum-nparams)) in
+      let newc = mkRel(cnum_nlams-argnum) in
       let subval = build_discriminator sigma cnum_env dirn newc sort l  in
       kont subval (build_coq_False (),mkSort (Prop Null))
 
+(* Note: discrimination could be more clever: if some elimination is
+   not allowed because of a large impredicative constructor in the
+   path (see allowed_sorts in find_positions), the positions could
+   still be discrimated by projecting first instead of putting the
+   discrimination combinator inside the projecting combinator. Example
+   of relevant situation:
+
+   Inductive t:Set := c : forall A:Set, A -> nat -> t.
+   Goal ~ c _ 0 0 = c _ 0 1. intro. discriminate H.
+*)
+
 let gen_absurdity id gl =
   if is_empty_type (clause_type (onHyp id) gl)
   then
@@ -466,12 +472,12 @@ let gen_absurdity id gl =
 
 (* Precondition: eq is leibniz equality
  
-  returns ((eq_elim t t1 P i t2), absurd_term)
-  where  P=[e:t]discriminator 
-         absurd_term=False
+   returns ((eq_elim t t1 P i t2), absurd_term)
+   where  P=[e:t]discriminator 
+          absurd_term=False
 *)
 
-let discrimination_pf e (t,t1,t2) discriminator lbeq gls =
+let discrimination_pf e (t,t1,t2) discriminator lbeq =
   let i           = build_coq_I () in
   let absurd_term = build_coq_False () in
   let eq_elim     = lbeq.ind in
@@ -479,28 +485,28 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq gls =
 
 exception NotDiscriminable
 
-let discrEq (lbeq,(t,t1,t2)) id gls =
-  let sort = pf_type_of gls (pf_concl gls) in 
+let eq_baseid = id_of_string "e"
+
+let discr_positions env sigma (lbeq,(t,t1,t2)) id cpath dirn sort =
+  let e = next_ident_away eq_baseid (ids_of_context env) in
+  let e_env = push_named (e,None,t) env in
+  let discriminator =
+    build_discriminator sigma e_env dirn (mkVar e) sort cpath in
+  let (pf, absurd_term) = discrimination_pf e (t,t1,t2) discriminator lbeq in
+  tclCOMPLETE 
+    ((tclTHENS (cut_intro absurd_term)
+      [onLastHyp gen_absurdity; 
+       refine (mkApp (pf,[|mkVar id|]))]))
+
+let discrEq (lbeq,(t,t1,t2) as u) id gls =
   let sigma = project gls in
   let env = pf_env gls in
-  (match find_positions env sigma t1 t2 with
-     | Inr _ ->
-	 errorlabstrm "discr" (str" Not a discriminable equality")
-     | Inl (cpath, (_,dirn), _) ->
-	 let e = pf_get_new_id (id_of_string "ee") gls in
-	 let e_env = push_named (e,None,t) env in
-	 let discriminator =
-	   build_discriminator sigma e_env dirn (mkVar e) sort cpath in
-	 let (pf, absurd_term) =
-	   discrimination_pf e (t,t1,t2) discriminator lbeq gls 
-	 in
-	 tclCOMPLETE((tclTHENS (cut_intro absurd_term)
-			([onLastHyp gen_absurdity;
-			  refine (mkApp (pf, [| mkVar id |]))]))) gls)
-
-let not_found_message id =
-  (str "The variable" ++ spc () ++ str (string_of_id id) ++ spc () ++
-    str" was not found in the current environment")
+  match find_positions env sigma t1 t2 with
+    | Inr _ ->
+	errorlabstrm "discr" (str" Not a discriminable equality")
+    | Inl (cpath, (_,dirn), _) ->
+	let sort = pf_apply get_type_of gls (pf_concl gls) in 
+	discr_positions env sigma u id cpath dirn sort gls
 
 let onEquality tac id gls =
   let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in
@@ -533,7 +539,7 @@ let discrEverywhere =
   tclORELSE
     (Tacticals.tryAllClauses discrSimpleClause)
     (fun gls -> 
-       errorlabstrm "DiscrEverywhere" (str" No discriminable equalities"))
+       errorlabstrm "DiscrEverywhere" (str"No discriminable equalities"))
 
 let discr_tac = function
   | None -> discrEverywhere
@@ -723,15 +729,9 @@ let make_iterated_tuple env sigma dflt (z,zty) =
 let rec build_injrec sigma env dflt c = function
   | [] -> make_iterated_tuple env sigma dflt (c,type_of env sigma c)
   | ((sp,cnum),argnum)::l ->
-      let cty = type_of env sigma c in
-      let (ity,_) = find_mrectype env sigma cty in
-      let (mib,mip) = lookup_mind_specif env ity in
-      let nparams = mib.mind_nparams in
       let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in
-      let newc = mkRel(cnum_nlams-(argnum-nparams)) in
-      let (subval,tuplety,dfltval) =
-      	build_injrec sigma cnum_env dflt newc l
-      in
+      let newc = mkRel(cnum_nlams-argnum) in
+      let (subval,tuplety,dfltval) = build_injrec sigma cnum_env dflt newc l in
       (kont subval (dfltval,tuplety),
        tuplety,dfltval)
 
@@ -739,6 +739,7 @@ let build_injector sigma env dflt c cpath =
   let (injcode,resty,_) = build_injrec sigma env dflt c cpath in
   (injcode,resty)
 
+(*
 let try_delta_expand env sigma t =
   let whdt = whd_betadeltaiota env sigma t  in 
   let rec hd_rec c  =
@@ -749,12 +750,39 @@ let try_delta_expand env sigma t =
       | _  -> t
   in 
   hd_rec whdt 
+*)
 
 (* Given t1=t2 Inj calculates the whd normal forms of t1 and t2 and it 
    expands then only when the whdnf has a constructor of an inductive type
    in hd position, otherwise delta expansion is not done *)
 
-let injEq (eq,(t,t1,t2)) id gls =
+let simplify_args env sigma t = 
+  (* Quick hack to reduce in arguments of eq only *)
+  match decompose_app t with
+    | eq, [t;c1;c2] -> applist (eq,[t;nf env sigma c1;nf env sigma c2])
+    | eq, [t1;c1;t2;c2] -> applist (eq,[t1;nf env sigma c1;t2;nf env sigma c2])
+    | _ -> t
+
+let inject_at_positions env sigma (eq,(t,t1,t2)) id posns =
+  let e = next_ident_away eq_baseid (ids_of_context env) in
+  let e_env = push_named (e,None,t) env in
+  let injectors =
+    map_succeed
+      (fun (cpath,t1',t2') ->
+        (* arbitrarily take t1' as the injector default value *)
+	let (injbody,resty) = build_injector sigma e_env t1' (mkVar e) cpath in
+	let injfun = mkNamedLambda e t injbody in
+	let pf = applist(eq.congr,[t;resty;injfun;t1;t2;mkVar id]) in
+	let ty = simplify_args env sigma (get_type_of env sigma pf) in
+	(pf,ty))
+      posns in
+  if injectors = [] then
+    errorlabstrm "Equality.inj" (str "Failed to decompose the equality");
+  tclMAP
+    (fun (pf,ty) -> tclTHENS (cut ty) [tclIDTAC; refine pf])
+    injectors
+
+let injEq ipats (eq,(t,t1,t2)) id gls =
   let sigma = project gls in
   let env = pf_env gls in
   match find_positions env sigma t1 t2 with
@@ -766,100 +794,38 @@ let injEq (eq,(t,t1,t2)) id gls =
 	errorlabstrm "Equality.inj" 
 	   (str"Nothing to do, it is an equality between convertible terms")
     | Inr posns ->
-	let e = pf_get_new_id (id_of_string "e") gls in
-	let e_env = push_named (e,None,t) env in
-	let injectors =
-	  map_succeed
-	    (fun (cpath,t1_0,t2_0) ->
-	      try 
-		let (injbody,resty) =
-                  (* take arbitrarily t1_0 as the injector default value *)
-		  build_injector sigma e_env t1_0 (mkVar e) cpath in
-		let injfun = mkNamedLambda e t injbody in
-		let _ = type_of env sigma injfun in (injfun,resty)
-	      with e when catchable_exception e ->
-		(* may fail because ill-typed or because of a Prop argument *)
-		(* error "find_sigma_data" *)
-		failwith "caught")
-            posns
-	in
-	if injectors = [] then
-	  errorlabstrm "Equality.inj" 
-	    (str "Failed to decompose the equality");
-	tclMAP 
-	  (fun (injfun,resty) ->
-	     let pf = applist(eq.congr,
-			      [t;resty;injfun;
-			       try_delta_expand env sigma t1;
-			       try_delta_expand env sigma t2;
-			       mkVar id]) 
-	     in
-	     let ty =
-	       try pf_nf gls (pf_type_of gls pf)
-               with
-		 | UserError("refiner__fail",_) -> 
-		     errorlabstrm "InjClause" 
-		(str (string_of_id id) ++ str" Not a projectable equality")
-	     in ((tclTHENS  (cut  ty) ([tclIDTAC;refine pf]))))
-	  injectors
+(* Est-ce utile à partir du moment où les arguments projetés subissent "nf" ?
+	let t1 = try_delta_expand env sigma t1 in
+	let t2 = try_delta_expand env sigma t2 in
+*)
+	tclTHEN 
+	  (inject_at_positions env sigma (eq,(t,t1,t2)) id posns)
+	  (intros_pattern None ipats)
 	  gls
 
-let inj = onEquality injEq
+let inj ipats = onEquality (injEq ipats)
 
-let injClause = function
-  | None -> onNegatedEquality injEq
-  | Some id -> try_intros_until inj id
+let injClause ipats = function
+  | None -> onNegatedEquality (injEq ipats)
+  | Some id -> try_intros_until (inj ipats) id
 
-let injConcl gls  = injClause None gls
-let injHyp id gls = injClause (Some id) gls
+let injConcl gls  = injClause [] None gls
+let injHyp id gls = injClause [] (Some id) gls
 
-let decompEqThen ntac (lbeq,(t,t1,t2)) id gls =
-  let sort = pf_type_of gls (pf_concl gls) in 
+let decompEqThen ntac (lbeq,(t,t1,t2) as u) id gls =
+  let sort = pf_apply get_type_of gls (pf_concl gls) in 
   let sigma = project gls in
   let env = pf_env gls in 
-  (match find_positions env sigma t1 t2 with
-     | Inl (cpath, (_,dirn), _) ->
-	 let e = pf_get_new_id (id_of_string "e") gls in
-	 let e_env = push_named (e,None,t) env in
-	 let discriminator =
-	   build_discriminator sigma e_env dirn (mkVar e) sort cpath in
-	 let (pf, absurd_term) =
-	   discrimination_pf e (t,t1,t2) discriminator lbeq gls in
-	 tclCOMPLETE
-	   ((tclTHENS (cut_intro absurd_term)
-	       ([onLastHyp gen_absurdity;
-		 refine (mkApp (pf, [| mkVar id |]))]))) gls
-     | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
-         ntac 0 gls
-     | Inr posns ->
-	 (let e = pf_get_new_id (id_of_string "e") gls in
-	  let e_env = push_named (e,None,t) env in
-	  let injectors =
-	    map_succeed
-	      (fun (cpath,t1_0,t2_0) ->
-		 let (injbody,resty) =
-                  (* take arbitrarily t1_0 as the injector default value *)
-		   build_injector sigma e_env t1_0 (mkVar e) cpath in
-		 let injfun = mkNamedLambda e t injbody in
-		 try 
-		   let _ = type_of env sigma injfun in (injfun,resty)
-		 with e when catchable_exception e -> failwith "caught")
-	      posns 
-	  in
-	  if injectors = [] then
-	    errorlabstrm "Equality.decompEqThen" 
-              (str "Discriminate failed to decompose the equality");
-	  (tclTHEN
-	      (tclMAP (fun (injfun,resty) ->
-			 let pf = applist(lbeq.congr,
-					  [t;resty;injfun;t1;t2;
-					   mkVar id]) in
-			 let ty = pf_nf gls (pf_type_of gls pf) in
-			 ((tclTHENS (cut ty) 
-			     ([tclIDTAC;refine pf]))))
-		 (List.rev injectors))
-	      (ntac (List.length injectors)))
-	  gls))
+  match find_positions env sigma t1 t2 with
+    | Inl (cpath, (_,dirn), _) ->
+	discr_positions env sigma u id cpath dirn sort gls
+    | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
+        ntac 0 gls
+    | Inr posns ->
+	tclTHEN
+	  (inject_at_positions env sigma (lbeq,(t,t1,t2)) id (List.rev posns))
+	  (ntac (List.length posns))
+	  gls
 
 let dEqThen ntac = function
   | None -> onNegatedEquality (decompEqThen ntac)
@@ -903,7 +869,7 @@ let find_elim sort_of_gl lbeq =
 
 let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
   (* find substitution scheme *)
-  let eq_elim = find_elim (pf_type_of gls (pf_concl gls)) lbeq in
+  let eq_elim = find_elim (pf_apply get_type_of gls (pf_concl gls)) lbeq in
   (* build substitution predicate *)
   let p = lambda_create (pf_env gls) (t,body) in
   (* apply substitution scheme *)
@@ -1013,7 +979,7 @@ let cutRewriteInHyp l2r eqn id = cutRewriteClause l2r eqn (Some id)
 let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None
 
 let substClause l2r c cls gls =
-  let eq = pf_type_of gls c in
+  let eq = pf_apply get_type_of gls c in
   tclTHENS (cutSubstClause l2r eq cls) [tclIDTAC; exact_no_check c] gls
 
 let rewriteClause l2r c cls = try_rewrite (substClause l2r c cls)
@@ -1147,28 +1113,10 @@ let subst_all gl =
   let ids = list_uniquize ids in
   subst ids gl
 
+
 (* Rewrite the first assumption for which the condition faildir does not fail 
    and gives the direction of the rewrite *)
 
-let rewrite_assumption_cond faildir gl =
-   let rec arec = function
-      | [] -> error "No such assumption"
-      | (id,_,t)::rest -> 
-	  (try let dir = faildir t gl in 
-	       general_rewrite dir (mkVar id) gl
-	   with Failure _ | UserError _  ->  arec rest)
-   in arec (pf_hyps gl)
-
-
-let rewrite_assumption_cond_in faildir hyp gl =
-   let rec arec = function
-      | [] -> error "No such assumption"
-      | (id,_,t)::rest -> 
-	  (try let dir = faildir t gl in 
-	       general_rewrite_in dir hyp (mkVar id) gl
-	   with Failure _ | UserError _ ->  arec rest)
-   in arec (pf_hyps gl)
-
 let cond_eq_term_left c t gl =
   try
     let (_,x,_) = snd (find_eq_data_decompose t) in
@@ -1189,6 +1137,48 @@ let cond_eq_term c t gl =
     else failwith "not convertible"
   with PatternMatchingFailure -> failwith "not an equality"
 
+let rewrite_mutli_assumption_cond cond_eq_term cl gl = 
+  let rec arec = function 
+    | [] -> error "No such assumption"
+    | (id,_,t) ::rest -> 
+	begin 
+	  try 
+	    let dir = cond_eq_term t gl in 
+	    general_multi_rewrite dir (mkVar id,NoBindings) cl gl
+	  with | Failure _ | UserError _ -> arec rest
+	end
+  in 
+  arec (pf_hyps gl)
+
+let replace_multi_term dir_opt c  = 
+  let cond_eq_fun = 
+    match dir_opt with 
+      | None -> cond_eq_term c
+      | Some true -> cond_eq_term_left c
+      | Some false -> cond_eq_term_right c
+  in 
+  rewrite_mutli_assumption_cond cond_eq_fun 
+
+(* JF. old version 
+let rewrite_assumption_cond faildir gl =
+   let rec arec = function
+      | [] -> error "No such assumption"
+      | (id,_,t)::rest ->
+	  (try let dir = faildir t gl in
+	       general_rewrite dir (mkVar id) gl
+	   with Failure _ | UserError _  ->  arec rest)
+   in arec (pf_hyps gl)
+
+
+let rewrite_assumption_cond_in faildir hyp gl =
+   let rec arec = function
+      | [] -> error "No such assumption"
+      | (id,_,t)::rest ->
+	  (try let dir = faildir t gl in
+	       general_rewrite_in dir hyp (mkVar id) gl
+	   with Failure _ | UserError _ ->  arec rest)
+   in arec (pf_hyps gl)
+
 let replace_term_left t = rewrite_assumption_cond (cond_eq_term_left t)
 
 let replace_term_right t = rewrite_assumption_cond (cond_eq_term_right t)
@@ -1200,6 +1190,27 @@ let replace_term_in_left t = rewrite_assumption_cond_in (cond_eq_term_left t)
 let replace_term_in_right t = rewrite_assumption_cond_in (cond_eq_term_right t)
    
 let replace_term_in t = rewrite_assumption_cond_in (cond_eq_term t)
+*)
+
+let replace_term_left t = replace_multi_term (Some true) t Tacticals.onConcl
+
+let replace_term_right t = replace_multi_term (Some false) t Tacticals.onConcl
+
+let replace_term t = replace_multi_term None t Tacticals.onConcl
+
+let replace_term_in_left t hyp = replace_multi_term (Some true) t (Tacticals.onHyp hyp)
+
+let replace_term_in_right t hyp = replace_multi_term (Some false) t (Tacticals.onHyp hyp)
+
+let replace_term_in t hyp = replace_multi_term None t (Tacticals.onHyp hyp)
+
+
+
+
+
+
+
+
 
-let _ = Setoid_replace.register_replace replace
+let _ = Setoid_replace.register_replace (fun tac_opt c2 c1 gl ->  replace_in_clause_maybe_by c2 c1 onConcl tac_opt gl)
 let _ = Setoid_replace.register_general_rewrite general_rewrite