Merge branch 'experimental/upstream' into upstream

1 files changed, 190 insertions, 103 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index a25f88e3..1c5e4b2f 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: equality.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Pp
 open Util
 open Names
@@ -35,7 +33,7 @@ open Tacexpr
 open Tacticals
 open Tactics
 open Tacred
-open Rawterm
+open Glob_term
 open Coqlib
 open Vernacexpr
 open Declarations
@@ -58,6 +56,7 @@ open Goptions
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "automatic introduction of hypotheses by discriminate";
       optkey   = ["Discriminate";"Introduction"];
       optread  = (fun () -> !discriminate_introduction);
@@ -66,6 +65,7 @@ let _ =
 (* Rewriting tactics *)
 
 type dep_proof_flag = bool (* true = support rewriting dependent proofs *)
+type freeze_evars_flag = bool (* true = don't instantiate existing evars *)
 
 type orientation = bool
 
@@ -84,18 +84,43 @@ type conditions =
 
 let rewrite_unif_flags = {
   Unification.modulo_conv_on_closed_terms = None;
-  Unification.use_metas_eagerly = true;
+  Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
   Unification.modulo_delta = empty_transparent_state;
+  Unification.modulo_delta_types = empty_transparent_state;
+  Unification.modulo_delta_in_merge = None;
+  Unification.check_applied_meta_types = true;
   Unification.resolve_evars = true;
-  Unification.use_evars_pattern_unification = true;
+  Unification.use_pattern_unification = true;
+  Unification.use_meta_bound_pattern_unification = true;
+  Unification.frozen_evars = ExistentialSet.empty;
+  Unification.restrict_conv_on_strict_subterms = false;
+  Unification.modulo_betaiota = false;
+  Unification.modulo_eta = true;
+  Unification.allow_K_in_toplevel_higher_order_unification = false
+    (* allow_K does not matter in practice because calls w_typed_unify *)
 }
 
+let freeze_initial_evars sigma flags clause =
+  (* We take evars of the type: this may include old evars! For excluding *)
+  (* all old evars, including the ones occurring in the rewriting lemma, *)
+  (* we would have to take the clenv_value *)
+  let newevars = Evd.collect_evars (clenv_type clause) in
+  let evars =
+    fold_undefined (fun evk _ evars ->
+      if ExistentialSet.mem evk newevars then evars
+      else ExistentialSet.add evk evars)
+      sigma ExistentialSet.empty in
+  { flags with Unification.frozen_evars = evars }
+
+let make_flags frzevars sigma flags clause =
+  if frzevars then freeze_initial_evars sigma flags clause else flags
+
 let side_tac tac sidetac =
   match sidetac with
   | None -> tac
   | Some sidetac -> tclTHENSFIRSTn tac [|tclIDTAC|] sidetac
 
-let instantiate_lemma_all env sigma gl c ty l l2r concl =
+let instantiate_lemma_all frzevars env sigma gl c ty l l2r concl =
   let eqclause = Clenv.make_clenv_binding { gl with sigma = sigma } (c,ty) l in
   let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
   let rec split_last_two = function
@@ -105,13 +130,12 @@ let instantiate_lemma_all env sigma gl c ty l l2r concl =
       | _ -> error "The term provided is not an applied relation." in
   let others,(c1,c2) = split_last_two args in
   let try_occ (evd', c') =
-    let cl' = {eqclause with evd = evd'} in
-    let mvs = clenv_dependent false cl' in
-      clenv_pose_metas_as_evars cl' mvs
+    clenv_pose_dependent_evars true {eqclause with evd = evd'}
   in
+  let flags = make_flags frzevars sigma rewrite_unif_flags eqclause in
   let occs =
-    Unification.w_unify_to_subterm_all ~flags:rewrite_unif_flags env
-      ((if l2r then c1 else c2),concl) eqclause.evd
+    Unification.w_unify_to_subterm_all ~flags env eqclause.evd
+      ((if l2r then c1 else c2),concl)
   in List.map try_occ occs
 
 let instantiate_lemma env sigma gl c ty l l2r concl =
@@ -121,28 +145,62 @@ let instantiate_lemma env sigma gl c ty l l2r concl =
   let eqclause = Clenv.make_clenv_binding gl (c,t) l in
    [eqclause]
 
-let rewrite_elim with_evars c e ?(allow_K=true) =
-  general_elim_clause_gen (elimination_clause_scheme with_evars allow_K) c e
+let rewrite_conv_closed_unif_flags = {
+  Unification.modulo_conv_on_closed_terms = Some full_transparent_state;
+    (* We have this flag for historical reasons, it has e.g. the consequence *)
+    (* to rewrite "?x+2" in "y+(1+1)=0" or to rewrite "?x+?x" in "2+(1+1)=0" *)
+
+  Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
+    (* Combined with modulo_conv_on_closed_terms, this flag allows since 8.2 *)
+    (* to rewrite e.g. "?x+(2+?x)" in "1+(1+2)=0" *)
+
+  Unification.modulo_delta = empty_transparent_state;
+  Unification.modulo_delta_types = full_transparent_state;
+  Unification.modulo_delta_in_merge = None;
+  Unification.check_applied_meta_types = true;
+  Unification.resolve_evars = false;
+  Unification.use_pattern_unification = true;
+    (* To rewrite "?n x y" in "y+x=0" when ?n is *)
+    (* a preexisting evar of the goal*)
+
+  Unification.use_meta_bound_pattern_unification = true;
+
+  Unification.frozen_evars = ExistentialSet.empty;
+    (* This is set dynamically *)
+
+  Unification.restrict_conv_on_strict_subterms = false;
+  Unification.modulo_betaiota = false;
+  Unification.modulo_eta = true;
+  Unification.allow_K_in_toplevel_higher_order_unification = false
+}
+
+let rewrite_elim with_evars frzevars c e gl =
+  let flags =
+    make_flags frzevars (project gl) rewrite_conv_closed_unif_flags c in
+  general_elim_clause_gen (elimination_clause_scheme with_evars ~flags) c e gl
 
-let rewrite_elim_in with_evars id c e =
-  general_elim_clause_gen (elimination_in_clause_scheme with_evars id) c e
+let rewrite_elim_in with_evars frzevars id c e gl =
+  let flags =
+    make_flags frzevars (project gl) rewrite_conv_closed_unif_flags c in
+  general_elim_clause_gen
+    (elimination_in_clause_scheme with_evars ~flags id) c e gl
 
 (* Ad hoc asymmetric general_elim_clause *)
-let general_elim_clause with_evars cls rew elim =
+let general_elim_clause with_evars frzevars cls rew elim =
   try
     (match cls with
       | None ->
 	  (* was tclWEAK_PROGRESS which only fails for tactics generating one
              subgoal and did not fail for useless conditional rewritings generating
              an extra condition *)
-	  tclNOTSAMEGOAL (rewrite_elim with_evars rew elim ~allow_K:false)
-      | Some id -> rewrite_elim_in with_evars id rew elim)
-  with Pretype_errors.PretypeError (env,
-				   (Pretype_errors.NoOccurrenceFound (c', _))) ->
+	  tclNOTSAMEGOAL (rewrite_elim with_evars frzevars rew elim)
+      | Some id -> rewrite_elim_in with_evars frzevars id rew elim)
+  with Pretype_errors.PretypeError (env,evd,
+				    Pretype_errors.NoOccurrenceFound (c', _)) ->
     raise (Pretype_errors.PretypeError
-	      (env, (Pretype_errors.NoOccurrenceFound (c', cls))))
+	      (env,evd,Pretype_errors.NoOccurrenceFound (c', cls)))
 
-let general_elim_clause with_evars tac cls sigma c t l l2r elim gl =
+let general_elim_clause with_evars frzevars tac cls sigma c t l l2r elim gl =
   let all, firstonly, tac =
     match tac with
     | None -> false, false, None
@@ -151,12 +209,15 @@ let general_elim_clause with_evars tac cls sigma c t l l2r elim gl =
     | Some (tac, AllMatches) -> true, false, Some (tclCOMPLETE tac)
   in
   let cs =
-    (if not all then instantiate_lemma else instantiate_lemma_all)
+    (if not all then instantiate_lemma else instantiate_lemma_all frzevars)
       (pf_env gl) sigma gl c t l l2r
       (match cls with None -> pf_concl gl | Some id -> pf_get_hyp_typ gl id)
   in
   let try_clause c =
-    side_tac (tclTHEN (Refiner.tclEVARS c.evd) (general_elim_clause with_evars cls c elim)) tac
+    side_tac
+      (tclTHEN
+         (Refiner.tclEVARS c.evd)
+         (general_elim_clause with_evars frzevars cls c elim)) tac
   in
     if firstonly then
       tclFIRST (List.map try_clause cs) gl
@@ -180,8 +241,8 @@ let register_is_applied_rewrite_relation = (:=) is_applied_rewrite_relation
 
 let find_elim hdcncl lft2rgt dep cls args gl =
   let inccl = (cls = None) in
-  if (hdcncl = constr_of_reference (Coqlib.glob_eq) ||
-      hdcncl = constr_of_reference (Coqlib.glob_jmeq) &&
+  if (eq_constr hdcncl (constr_of_reference (Coqlib.glob_eq)) ||
+      eq_constr hdcncl (constr_of_reference (Coqlib.glob_jmeq)) &&
       pf_conv_x gl (List.nth args 0) (List.nth args 2)) && not dep
     || Flags.version_less_or_equal Flags.V8_2
   then
@@ -195,7 +256,7 @@ let find_elim hdcncl lft2rgt dep cls args gl =
 	  let c1 = destConst pr1 in 
 	  let mp,dp,l = repr_con (constant_of_kn (canonical_con c1)) in 
 	  let l' = label_of_id (add_suffix (id_of_label l) "_r")  in 
-	  let c1' = Global.constant_of_delta (make_con mp dp l') in
+	  let c1' = Global.constant_of_delta_kn (make_kn mp dp l') in
 	  begin 
 	    try 
 	      let _ = Global.lookup_constant c1' in
@@ -211,20 +272,16 @@ let find_elim hdcncl lft2rgt dep cls args gl =
 	assert false
   else
   let scheme_name = match dep, lft2rgt, inccl with
-    (* Non dependent case with symmetric equality *)
-    | false, Some true, true | false, Some false, false -> rew_l2r_scheme_kind
-    | false, Some false, true | false, Some true, false -> rew_r2l_scheme_kind
-    (* Dependent case with symmetric equality *)
+    (* Non dependent case *)
+    | false, Some true, true -> rew_l2r_scheme_kind
+    | false, Some true, false -> rew_r2l_scheme_kind
+    | false, _, false -> rew_l2r_scheme_kind
+    | false, _, true -> rew_r2l_scheme_kind
+    (* Dependent case *)
     | true, Some true, true -> rew_l2r_dep_scheme_kind
     | true, Some true, false -> rew_l2r_forward_dep_scheme_kind
-    | true, Some false, true -> rew_r2l_dep_scheme_kind
-    | true, Some false, false -> rew_r2l_forward_dep_scheme_kind
-    (* Non dependent case with non-symmetric rewriting lemma *)
-    | false, None, true -> rew_r2l_scheme_kind
-    | false, None, false -> rew_asym_scheme_kind
-    (* Dependent case with non-symmetric rewriting lemma *)
-    | true, None, true -> rew_r2l_dep_scheme_kind
-    | true, None, false -> rew_r2l_forward_dep_scheme_kind
+    | true, _, true -> rew_r2l_dep_scheme_kind
+    | true, _, false -> rew_r2l_forward_dep_scheme_kind
   in
   match kind_of_term hdcncl with
   | Ind ind -> mkConst (find_scheme scheme_name ind)
@@ -234,12 +291,12 @@ let type_of_clause gl = function
   | None -> pf_concl gl
   | Some id -> pf_get_hyp_typ gl id
 
-let leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c t l with_evars dep_proof_ok gl hdcncl =
+let leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c t l with_evars frzevars dep_proof_ok gl hdcncl =
   let isatomic = isProd (whd_zeta hdcncl) in
   let dep_fun = if isatomic then dependent else dependent_no_evar in
   let dep = dep_proof_ok && dep_fun c (type_of_clause gl cls) in
   let elim = find_elim hdcncl lft2rgt dep cls (snd (decompose_app t)) gl in
-  general_elim_clause with_evars tac cls sigma c t l
+  general_elim_clause with_evars frzevars tac cls sigma c t l
     (match lft2rgt with None -> false | Some b -> b)
     {elimindex = None; elimbody = (elim,NoBindings)} gl
 
@@ -259,7 +316,7 @@ let rewrite_side_tac tac sidetac = side_tac tac (Option.map fst sidetac)
 
 (* Main function for dispatching which kind of rewriting it is about *)
 
-let general_rewrite_ebindings_clause cls lft2rgt occs dep_proof_ok ?tac
+let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
     ((c,l) : constr with_bindings) with_evars gl =
   if occs <> all_occurrences then (
     rewrite_side_tac (!general_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac gl)
@@ -272,39 +329,44 @@ let general_rewrite_ebindings_clause cls lft2rgt occs dep_proof_ok ?tac
       | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *)
 	  let lft2rgt = adjust_rewriting_direction args lft2rgt in
           leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c (it_mkProd_or_LetIn t rels)
-	    l with_evars dep_proof_ok gl hdcncl
+	    l with_evars frzevars dep_proof_ok gl hdcncl
       | None ->
 	  try
 	    rewrite_side_tac (!general_rewrite_clause cls
 				 lft2rgt occs (c,l) ~new_goals:[]) tac gl
-	  with e -> (* Try to see if there's an equality hidden *)
+	  with e when Errors.noncritical e ->
+            (* Try to see if there's an equality hidden *)
 	    let env' = push_rel_context rels env in
 	    let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *)
 	      match match_with_equality_type t' with
 	      | Some (hdcncl,args) ->
 		  let lft2rgt = adjust_rewriting_direction args lft2rgt in
 		    leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c
-		      (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars dep_proof_ok gl hdcncl
+		      (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars frzevars dep_proof_ok gl hdcncl
 	      | None -> raise e
 		  (* error "The provided term does not end with an equality or a declared rewrite relation." *)
 
 let general_rewrite_ebindings =
   general_rewrite_ebindings_clause None
 
-let general_rewrite_bindings l2r occs dep_proof_ok ?tac (c,bl) =
-  general_rewrite_ebindings_clause None l2r occs dep_proof_ok ?tac (c,bl)
+let general_rewrite_bindings l2r occs frzevars dep_proof_ok ?tac (c,bl) =
+  general_rewrite_ebindings_clause None l2r occs
+    frzevars dep_proof_ok ?tac (c,bl)
 
-let general_rewrite l2r occs dep_proof_ok ?tac c =
-  general_rewrite_bindings l2r occs dep_proof_ok ?tac (c,NoBindings) false
+let general_rewrite l2r occs frzevars dep_proof_ok ?tac c =
+  general_rewrite_bindings l2r occs
+    frzevars dep_proof_ok ?tac (c,NoBindings) false
 
-let general_rewrite_ebindings_in l2r occs dep_proof_ok ?tac id =
-  general_rewrite_ebindings_clause (Some id) l2r occs dep_proof_ok ?tac
+let general_rewrite_ebindings_in l2r occs frzevars dep_proof_ok ?tac id =
+  general_rewrite_ebindings_clause (Some id) l2r occs frzevars dep_proof_ok ?tac
 
-let general_rewrite_bindings_in l2r occs dep_proof_ok ?tac id (c,bl) =
-  general_rewrite_ebindings_clause (Some id) l2r occs dep_proof_ok ?tac (c,bl)
+let general_rewrite_bindings_in l2r occs frzevars dep_proof_ok ?tac id (c,bl) =
+  general_rewrite_ebindings_clause (Some id) l2r occs
+    frzevars dep_proof_ok ?tac (c,bl)
 
-let general_rewrite_in l2r occs dep_proof_ok ?tac id c =
-  general_rewrite_ebindings_clause (Some id) l2r occs dep_proof_ok ?tac (c,NoBindings)
+let general_rewrite_in l2r occs frzevars dep_proof_ok ?tac id c =
+  general_rewrite_ebindings_clause (Some id) l2r occs
+    frzevars dep_proof_ok ?tac (c,NoBindings)
 
 let general_multi_rewrite l2r with_evars ?tac c cl =
   let occs_of = on_snd (List.fold_left
@@ -320,12 +382,12 @@ let general_multi_rewrite l2r with_evars ?tac c cl =
 	  | [] -> tclIDTAC
 	  | ((occs,id),_) :: l ->
 	    tclTHENFIRST
-	      (general_rewrite_ebindings_in l2r (occs_of occs) true ?tac id c with_evars)
+	      (general_rewrite_ebindings_in l2r (occs_of occs) false true ?tac id c with_evars)
 	      (do_hyps l)
 	in
 	if cl.concl_occs = no_occurrences_expr then do_hyps l else
 	  tclTHENFIRST
-	   (general_rewrite_ebindings l2r (occs_of cl.concl_occs) true ?tac c with_evars)
+	   (general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars)
 	   (do_hyps l)
     | None ->
 	(* Otherwise, if we are told to rewrite in all hypothesis via the
@@ -334,7 +396,7 @@ let general_multi_rewrite l2r with_evars ?tac c cl =
 	  | [] -> (fun gl -> error "Nothing to rewrite.")
 	  | id :: l ->
 	    tclIFTHENTRYELSEMUST
-	     (general_rewrite_ebindings_in l2r all_occurrences true ?tac id c with_evars)
+	     (general_rewrite_ebindings_in l2r all_occurrences false true ?tac id c with_evars)
 	     (do_hyps_atleastonce l)
 	in
 	let do_hyps gl =
@@ -346,7 +408,7 @@ let general_multi_rewrite l2r with_evars ?tac c cl =
 	in
 	if cl.concl_occs = no_occurrences_expr then do_hyps else
 	  tclIFTHENTRYELSEMUST
-	   (general_rewrite_ebindings l2r (occs_of cl.concl_occs) true ?tac c with_evars)
+	   (general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars)
 	   do_hyps
 
 type delayed_open_constr_with_bindings =
@@ -371,8 +433,8 @@ let general_multi_multi_rewrite with_evars l cl tac =
     | (l2r,m,c)::l -> tclTHENFIRST (doN l2r c m) (loop l)
   in loop l
 
-let rewriteLR = general_rewrite true all_occurrences true
-let rewriteRL = general_rewrite false all_occurrences true
+let rewriteLR = general_rewrite true all_occurrences true true
+let rewriteRL = general_rewrite false all_occurrences true true
 
 (* Replacing tactics *)
 
@@ -512,7 +574,7 @@ let discriminable env sigma t1 t2 =
 
 let injectable env sigma t1 t2 =
     match find_positions env sigma t1 t2 with
-    | Inl _ | Inr [] -> false
+    | Inl _ | Inr [] | Inr [([],_,_)] -> false
     | Inr _ -> true
 
 
@@ -631,7 +693,7 @@ let construct_discriminator sigma env dirn c sort =
           CP : changed assert false in a more informative error
        *)
       errorlabstrm "Equality.construct_discriminator"
-	(str "Cannot discriminate on inductive constructors with
+	(str "Cannot discriminate on inductive constructors with \
 		 dependent types.") in
   let (ind,_) = dest_ind_family indf in
   let (mib,mip) = lookup_mind_specif env ind in
@@ -682,14 +744,13 @@ let gen_absurdity id gl =
 *)
 
 let ind_scheme_of_eq lbeq =
-  let ind = destInd lbeq.eq in
-  let (mib,mip) = Global.lookup_inductive ind in
+  let (mib,mip) = Global.lookup_inductive (destInd lbeq.eq) in
   let kind = inductive_sort_family mip in
   (* use ind rather than case by compatibility *)
   let kind =
     if kind = InProp then Elimschemes.ind_scheme_kind_from_prop
     else Elimschemes.ind_scheme_kind_from_type in
-  mkConst (find_scheme kind ind)
+  mkConst (find_scheme kind (destInd lbeq.eq))
 
 
 let discrimination_pf e (t,t1,t2) discriminator lbeq =
@@ -894,8 +955,8 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
       let rty = beta_applist(p_i_minus_1,[ev]) in
       let tuple_tail = sigrec_clausal_form (siglen-1) rty in
       match
-  	Evd.existential_opt_value !evdref
- 	  (destEvar ev)
+        Evd.existential_opt_value !evdref
+          (destEvar ev)
       with
 	| Some w ->
             let w_type = type_of env sigma w in
@@ -1057,6 +1118,8 @@ let injEq ipats (eq,_,(t,t1,t2) as u) eq_clause =
     | Inr [] ->
 	errorlabstrm "Equality.inj"
 	   (str"Nothing to do, it is an equality between convertible terms.")
+    | Inr [([],_,_)] when Flags.version_strictly_greater Flags.V8_3 ->
+        errorlabstrm "Equality.inj" (str"Nothing to inject.")
     | Inr posns ->
 (* Est-ce utile à partir du moment où les arguments projetés subissent "nf" ?
 	let t1 = try_delta_expand env sigma t1 in
@@ -1094,7 +1157,7 @@ let injEq ipats (eq,_,(t,t1,t2) as u) eq_clause =
                 ]
 (* not a dep eq or no decidable type found *)
             ) else (raise Not_dep_pair)
-        ) with _ ->
+        ) with e when Errors.noncritical e ->
 	  inject_at_positions env sigma u eq_clause posns
 	    (fun _ -> intros_pattern no_move ipats)
 
@@ -1186,26 +1249,37 @@ let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
 
 let decomp_tuple_term env c t =
   let rec decomprec inner_code ex exty =
+    let iterated_decomp =
     try
       let {proj1=p1; proj2=p2},(a,p,car,cdr) = find_sigma_data_decompose ex in
       let car_code = applist (p1,[a;p;inner_code])
       and cdr_code = applist (p2,[a;p;inner_code]) in
       let cdrtyp = beta_applist (p,[car]) in
-      ((car,a),car_code)::(decomprec cdr_code cdr cdrtyp)
+      List.map (fun l -> ((car,a),car_code)::l) (decomprec cdr_code cdr cdrtyp)
     with PatternMatchingFailure ->
-      [((ex,exty),inner_code)]
+      []
+    in
+    [((ex,exty),inner_code)]::iterated_decomp
   in
-  List.split (decomprec (mkRel 1) c t)
+  decomprec (mkRel 1) c t
 
 let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   let typ = get_type_of env sigma dep_pair1 in
+  (* We find all possible decompositions *)
+  let decomps1 = decomp_tuple_term env dep_pair1 typ in
+  let decomps2 = decomp_tuple_term env dep_pair2 typ in
+  (* We adjust to the shortest decomposition *)
+  let n = min (List.length decomps1) (List.length decomps2) in
+  let decomp1 = List.nth decomps1 (n-1) in
+  let decomp2 = List.nth decomps2 (n-1) in
   (* We rewrite dep_pair1 ... *)
-  let e1_list,proj_list = decomp_tuple_term env dep_pair1 typ in
+  let e1_list,proj_list = List.split decomp1 in
+  (* ... and use dep_pair2 to compute the expected goal *)
+  let e2_list,_ = List.split decomp2 in
+  (* We build the expected goal *)
   let abst_B =
     List.fold_right
       (fun (e,t) body -> lambda_create env (t,subst_term e body)) e1_list b in
-  (* ... and use dep_pair2 to compute the expected goal *)
-  let e2_list,_ = decomp_tuple_term env dep_pair2 typ in
   let pred_body = beta_applist(abst_B,proj_list) in
   let expected_goal = beta_applist (abst_B,List.map fst e2_list) in
   (* Simulate now the normalisation treatment made by Logic.mk_refgoals *)
@@ -1330,34 +1404,21 @@ exception FoundHyp of (identifier * constr * bool)
 let is_eq_x gl x (id,_,c) =
   try
     let (_,lhs,rhs) = snd (find_eq_data_decompose gl c) in
-    if (x = lhs) && not (occur_term x rhs) then raise (FoundHyp (id,rhs,true));
-    if (x = rhs) && not (occur_term x lhs) then raise (FoundHyp (id,lhs,false))
+    if (eq_constr x lhs) && not (occur_term x rhs) then raise (FoundHyp (id,rhs,true));
+    if (eq_constr x rhs) && not (occur_term x lhs) then raise (FoundHyp (id,lhs,false))
   with PatternMatchingFailure ->
     ()
 
-let subst_one dep_proof_ok x gl =
-  let hyps = pf_hyps gl in
-  let (_,xval,_) = pf_get_hyp gl x in
-  (* If x has a body, simply replace x with body and clear x *)
-  if xval <> None then tclTHEN (unfold_body x) (clear [x]) gl else
-  (* x is a variable: *)
-  let varx = mkVar x in
-  (* Find a non-recursive definition for x *)
-  let (hyp,rhs,dir) =
-    try
-      let test hyp _ = is_eq_x gl varx hyp in
-      Sign.fold_named_context test ~init:() hyps;
-      errorlabstrm "Subst"
-        (str "Cannot find any non-recursive equality over " ++ pr_id x ++
-	 str".")
-    with FoundHyp res -> res
-  in
+(* Rewrite "hyp:x=rhs" or "hyp:rhs=x" (if dir=false) everywhere and
+   erase hyp and x; proceed by generalizing all dep hyps *)
+
+let subst_one dep_proof_ok x (hyp,rhs,dir) gl =
   (* The set of hypotheses using x *)
   let depdecls =
     let test (id,_,c as dcl) =
       if id <> hyp && occur_var_in_decl (pf_env gl) x dcl then dcl
       else failwith "caught" in
-    List.rev (map_succeed test hyps) in
+    List.rev (map_succeed test (pf_hyps gl)) in
   let dephyps = List.map (fun (id,_,_) -> id) depdecls in
   (* Decides if x appears in conclusion *)
   let depconcl = occur_var (pf_env gl) x (pf_concl gl) in
@@ -1373,23 +1434,47 @@ let subst_one dep_proof_ok x gl =
       (id,None,_) -> intro_using id
     | (id,Some hval,htyp) ->
         letin_tac None (Name id)
-	  (replace_term varx rhs hval)
-	  (Some (replace_term varx rhs htyp)) nowhere
+	  (replace_term (mkVar x) rhs hval)
+	  (Some (replace_term (mkVar x) rhs htyp)) nowhere
   in
   let need_rewrite = dephyps <> [] || depconcl in
   tclTHENLIST
     ((if need_rewrite then
       [generalize abshyps;
-       general_rewrite dir all_occurrences dep_proof_ok (mkVar hyp);
+       general_rewrite dir all_occurrences true dep_proof_ok (mkVar hyp);
        thin dephyps;
        tclMAP introtac depdecls]
-    else
-      [thin dephyps;
-       tclMAP introtac depdecls]) @
+      else
+       [tclIDTAC]) @
      [tclTRY (clear [x;hyp])]) gl
 
+(* Look for an hypothesis hyp of the form "x=rhs" or "rhs=x", rewrite
+   it everywhere, and erase hyp and x; proceed by generalizing all dep hyps *)
+
+let subst_one_var dep_proof_ok x gl =
+  let hyps = pf_hyps gl in
+  let (_,xval,_) = pf_get_hyp gl x in
+  (* If x has a body, simply replace x with body and clear x *)
+  if xval <> None then tclTHEN (unfold_body x) (clear [x]) gl else
+  (* x is a variable: *)
+  let varx = mkVar x in
+  (* Find a non-recursive definition for x *)
+  let (hyp,rhs,dir) =
+    try
+      let test hyp _ = is_eq_x gl varx hyp in
+      Sign.fold_named_context test ~init:() hyps;
+      errorlabstrm "Subst"
+        (str "Cannot find any non-recursive equality over " ++ pr_id x ++
+	 str".")
+    with FoundHyp res -> res in
+  subst_one dep_proof_ok x (hyp,rhs,dir) gl
+
 let subst_gen dep_proof_ok ids =
-  tclTHEN tclNORMEVAR (tclMAP (subst_one dep_proof_ok) ids)
+  tclTHEN tclNORMEVAR (tclMAP (subst_one_var dep_proof_ok) ids)
+
+(* For every x, look for an hypothesis hyp of the form "x=rhs" or "rhs=x",
+   rewrite it everywhere, and erase hyp and x; proceed by generalizing
+   all dep hyps *)
 
 let subst = subst_gen true
 
@@ -1466,3 +1551,5 @@ let replace_multi_term dir_opt c  =
 
 let _ = Tactics.register_general_multi_rewrite
   (fun b evars t cls -> general_multi_rewrite b evars t cls)
+
+let _ = Tactics.register_subst_one (fun b -> subst_one b)