Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 443 insertions, 344 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index bf199379..6522361e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: equality.ml 12886 2010-03-27 14:22:00Z herbelin $ *)
+(* $Id$ *)
 
 open Pp
 open Util
@@ -15,6 +15,7 @@ open Nameops
 open Univ
 open Term
 open Termops
+open Namegen
 open Inductive
 open Inductiveops
 open Environ
@@ -43,9 +44,36 @@ open Printer
 open Clenv
 open Clenvtac
 open Evd
+open Ind_tables
+open Eqschemes
+
+(* Options *)
+
+let discriminate_introduction = ref true
+
+let discr_do_intro () =
+  !discriminate_introduction && Flags.version_strictly_greater Flags.V8_2
+
+open Goptions
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optname  = "automatic introduction of hypotheses by discriminate";
+      optkey   = ["Discriminate";"Introduction"];
+      optread  = (fun () -> !discriminate_introduction);
+      optwrite = (:=) discriminate_introduction }
 
 (* Rewriting tactics *)
 
+type dep_proof_flag = bool (* true = support rewriting dependent proofs *)
+
+type orientation = bool
+
+type conditions =
+  | Naive (* Only try the first occurence of the lemma (default) *)
+  | FirstSolved (* Use the first match whose side-conditions are solved *)
+  | AllMatches (* Rewrite all matches whose side-conditions are solved *)
+
 (* Warning : rewriting from left to right only works
    if there exists in the context a theorem named <eqname>_<suffsort>_r
    with type (A:<sort>)(x:A)(P:A->Prop)(P x)->(y:A)(eqname A y x)->(P y).
@@ -54,161 +82,264 @@ open Evd
    -- Eduardo (19/8/97)
 *)
 
+let rewrite_unif_flags = {
+  Unification.modulo_conv_on_closed_terms = None;
+  Unification.use_metas_eagerly = true;
+  Unification.modulo_delta = empty_transparent_state;
+  Unification.resolve_evars = true;
+  Unification.use_evars_pattern_unification = true;
+}
+
+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 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
+      | [c1;c2] -> [],(c1, c2)
+      | x::y::z ->
+	  let l,res = split_last_two (y::z) in x::l, res
+      | _ -> 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
+  in
+  let occs =
+    Unification.w_unify_to_subterm_all ~flags:rewrite_unif_flags env
+      ((if l2r then c1 else c2),concl) eqclause.evd
+  in List.map try_occ occs
+
+let instantiate_lemma env sigma gl c ty l l2r concl =
+  let gl = { gl with sigma = sigma } in
+  let ct = pf_type_of gl c in
+  let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
+  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_elim_in with_evars id c e =
+  general_elim_clause_gen (elimination_in_clause_scheme with_evars id) c e
+
 (* Ad hoc asymmetric general_elim_clause *)
-let general_elim_clause with_evars cls sigma c l elim = 
-  try 
+let general_elim_clause with_evars cls rew elim =
+  try
     (match cls with
       | None ->
-	  (* was tclWEAK_PROGRESS which only fails for tactics generating one 
+	  (* was tclWEAK_PROGRESS which only fails for tactics generating one
              subgoal and did not fail for useless conditional rewritings generating
              an extra condition *)
-	  tclNOTSAMEGOAL (tclTHEN (Refiner.tclEVARS sigma)
-			     (general_elim with_evars (c,l) elim ~allow_K:false))
-      | Some id ->
-	  tclTHEN (Refiner.tclEVARS sigma) (general_elim_in with_evars id (c,l) elim))
+	  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', _))) ->
     raise (Pretype_errors.PretypeError
 	      (env, (Pretype_errors.NoOccurrenceFound (c', cls))))
-      
-(* The next function decides in particular whether to try a regular 
-  rewrite or a setoid rewrite. 
-  Approach is to break everything, if [eq] appears in head position 
-  then regular rewrite else try setoid rewrite. 
-  If occurrences are set, use setoid_rewrite.
-*)
 
-let general_setoid_rewrite_clause = ref (fun _ -> assert false)
-let register_general_setoid_rewrite_clause = (:=) general_setoid_rewrite_clause
+let general_elim_clause with_evars tac cls sigma c t l l2r elim gl =
+  let all, firstonly, tac =
+    match tac with
+    | None -> false, false, None
+    | Some (tac, Naive) -> false, false, Some tac
+    | Some (tac, FirstSolved) -> true, true, Some (tclCOMPLETE tac)
+    | Some (tac, AllMatches) -> true, false, Some (tclCOMPLETE tac)
+  in
+  let cs =
+    (if not all then instantiate_lemma else instantiate_lemma_all)
+      (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
+  in
+    if firstonly then
+      tclFIRST (List.map try_clause cs) gl
+    else tclMAP try_clause cs gl
+
+(* The next function decides in particular whether to try a regular
+  rewrite or a generalized rewrite.
+  Approach is to break everything, if [eq] appears in head position
+  then regular rewrite else try general rewrite.
+  If occurrences are set, use general rewrite.
+*)
 
-let is_applied_setoid_relation = ref (fun _ -> false)
-let register_is_applied_setoid_relation = (:=) is_applied_setoid_relation
+let general_rewrite_clause = ref (fun _ -> assert false)
+let register_general_rewrite_clause = (:=) general_rewrite_clause
 
-let is_applied_relation t =
-  match kind_of_term t with
-  | App (c, args) when Array.length args >= 2 -> true
-  | _ -> false
+let is_applied_rewrite_relation = ref (fun _ _ _ _ -> None)
+let register_is_applied_rewrite_relation = (:=) is_applied_rewrite_relation
 
 (* find_elim determines which elimination principle is necessary to
    eliminate lbeq on sort_of_gl. *)
 
-let find_elim hdcncl lft2rgt cls gl =
-  let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in
-  let hdcncls = string_of_inductive hdcncl ^ suffix in 
-  let rwr_thm = if lft2rgt = (cls = None) then hdcncls^"_r" else hdcncls in
-  try pf_global gl (id_of_string rwr_thm)
-  with Not_found -> error ("Cannot find rewrite principle "^rwr_thm^".")
-
-let leibniz_rewrite_ebindings_clause cls lft2rgt sigma c l with_evars gl hdcncl =
-  let elim = find_elim hdcncl lft2rgt cls gl in
-  general_elim_clause with_evars cls sigma c l (elim,NoBindings) gl
+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) &&
+      pf_conv_x gl (List.nth args 0) (List.nth args 2)) && not dep
+    || Flags.version_less_or_equal Flags.V8_2
+  then
+    (* use eq_rect, eq_rect_r, JMeq_rect, etc for compatibility *)
+    let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in
+    let hdcncls = string_of_inductive hdcncl ^ suffix in
+    let rwr_thm = if lft2rgt = Some (cls=None) then hdcncls^"_r" else hdcncls in
+    try pf_global gl (id_of_string rwr_thm)
+    with Not_found -> error ("Cannot find rewrite principle "^rwr_thm^".")
+  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 *)
+    | 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
+  in
+  match kind_of_term hdcncl with
+  | Ind ind -> mkConst (find_scheme scheme_name ind)
+  | _ -> assert false
+
+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 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
+    (match lft2rgt with None -> false | Some b -> b)
+    {elimindex = None; elimbody = (elim,NoBindings)} gl
 
 let adjust_rewriting_direction args lft2rgt =
-  if List.length args = 1 then
+  if List.length args = 1 then begin
     (* equality to a constant, like in eq_true *)
     (* more natural to see -> as the rewriting to the constant *)
-    not lft2rgt
+    if not lft2rgt then
+      error "Rewriting non-symmetric equality not allowed from right-to-left.";
+    None
+  end
   else
     (* other equality *)
-    lft2rgt
+    Some lft2rgt
+
+let rewrite_side_tac tac sidetac = side_tac tac (Option.map fst sidetac)
 
-let general_rewrite_ebindings_clause cls lft2rgt occs ((c,l) : open_constr with_bindings) with_evars gl =
+(* Main function for dispatching which kind of rewriting it is about *)
+
+let general_rewrite_ebindings_clause cls lft2rgt occs dep_proof_ok ?tac
+    ((c,l) : constr with_bindings) with_evars gl =
   if occs <> all_occurrences then (
-    !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl)
+    rewrite_side_tac (!general_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac gl)
   else
     let env = pf_env gl in
-    let sigma, c' = c in
-    let sigma = Evd.merge sigma (project gl) in
-    let ctype = get_type_of env sigma c' in 
-    let rels, t = decompose_prod (whd_betaiotazeta sigma ctype) in
+    let sigma = project gl in
+    let ctype = get_type_of env sigma c in
+    let rels, t = decompose_prod_assum (whd_betaiotazeta sigma ctype) in
       match match_with_equality_type t with
-      | Some (hdcncl,args) -> (* Fast path: direct leibniz rewrite *)
+      | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *)
 	  let lft2rgt = adjust_rewriting_direction args lft2rgt in
-	  leibniz_rewrite_ebindings_clause cls lft2rgt sigma c' l with_evars gl hdcncl
+          leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c (it_mkProd_or_LetIn t rels)
+	    l with_evars dep_proof_ok gl hdcncl
       | None ->
-	  let env' = List.fold_left (fun env (n,t) -> push_rel (n, None, t) env) env rels in
-	  let _,t' = splay_prod env' sigma t in (* Search for underlying eq *)
-	    match match_with_equality_type t' with
-	    | Some (hdcncl,args) -> (* Maybe a setoid relation with eq inside *)
-		let lft2rgt = adjust_rewriting_direction args lft2rgt in
-		if l = NoBindings && !is_applied_setoid_relation t then
-		  !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl
-		else
-		  (try leibniz_rewrite_ebindings_clause cls lft2rgt sigma c' l with_evars gl hdcncl
-		    with e -> 
-		      try !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl
-		      with _ -> raise e)
-	    | None -> (* Can't be leibniz, try setoid *)
-		if l = NoBindings
-		then !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl
-		else error "The term provided does not end with an equation."
-
-let general_rewrite_ebindings = 
+	  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 *)
+	    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
+	      | 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 (c,bl) = 
-  general_rewrite_ebindings_clause None l2r occs (inj_open c,inj_ebindings bl)
 
-let general_rewrite l2r occs c =
-  general_rewrite_bindings l2r occs (c,NoBindings) false
+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 l2r occs dep_proof_ok ?tac c =
+  general_rewrite_bindings l2r occs 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_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_ebindings_in l2r occs id =
-  general_rewrite_ebindings_clause (Some id) l2r occs
-let general_rewrite_bindings_in l2r occs id (c,bl) =
-  general_rewrite_ebindings_clause (Some id) l2r occs (inj_open c,inj_ebindings bl)
-let general_rewrite_in l2r occs id c = 
-  general_rewrite_ebindings_clause (Some id) l2r occs (inj_open c,NoBindings)
+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_multi_rewrite l2r with_evars c cl = 
-  let occs_of = on_snd (List.fold_left 
+let general_multi_rewrite l2r with_evars ?tac c cl =
+  let occs_of = on_snd (List.fold_left
     (fun acc ->
       function ArgArg x -> x :: acc | ArgVar _ -> acc)
     [])
   in
-  match cl.onhyps with 
-    | Some l -> 
+  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 
+	let rec do_hyps = function
 	  | [] -> tclIDTAC
-	  | ((occs,id),_) :: l -> 
+	  | ((occs,id),_) :: l ->
 	    tclTHENFIRST
-	      (general_rewrite_ebindings_in l2r (occs_of occs) id c with_evars)
+	      (general_rewrite_ebindings_in l2r (occs_of occs) true ?tac id c with_evars)
 	      (do_hyps l)
-	in 
+	in
 	if cl.concl_occs = no_occurrences_expr then do_hyps l else
 	  tclTHENFIRST
-	   (general_rewrite_ebindings l2r (occs_of cl.concl_occs) c with_evars)
+	   (general_rewrite_ebindings l2r (occs_of cl.concl_occs) true ?tac c with_evars)
 	   (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 
+    | 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_ebindings_in l2r all_occurrences id c with_evars)
+	  | id :: l ->
+	    tclIFTHENTRYELSEMUST
+	     (general_rewrite_ebindings_in l2r all_occurrences true ?tac id c with_evars)
 	     (do_hyps_atleastonce l)
-	in 
-	let do_hyps gl = 
+	in
+	let do_hyps gl =
 	  (* If the term to rewrite uses an hypothesis H, don't rewrite in H *)
-	  let ids = 
-	    let ids_in_c = Environ.global_vars_set (Global.env()) (snd (fst c)) in
+	  let ids =
+	    let ids_in_c = Environ.global_vars_set (Global.env()) (fst c) in
 	      Idset.fold (fun id l -> list_remove id l) ids_in_c (pf_ids_of_hyps gl)
 	  in do_hyps_atleastonce ids gl
-	in 
+	in
 	if cl.concl_occs = no_occurrences_expr then do_hyps else
-	  tclIFTHENTRYELSEMUST 
-	   (general_rewrite_ebindings l2r (occs_of cl.concl_occs) c with_evars)
+	  tclIFTHENTRYELSEMUST
+	   (general_rewrite_ebindings l2r (occs_of cl.concl_occs) true ?tac c with_evars)
 	   do_hyps
 
-let general_multi_multi_rewrite with_evars l cl tac = 
-  let do1 l2r c = 
-    match tac with
-	None -> general_multi_rewrite l2r with_evars c cl
-      | Some tac -> tclTHENSFIRSTn (general_multi_rewrite l2r with_evars c cl)
-	  [|tclIDTAC|] (tclCOMPLETE tac)
-  in
-  let rec doN l2r c = function 
+type delayed_open_constr_with_bindings =
+    env -> evar_map -> evar_map * constr with_bindings
+
+let general_multi_multi_rewrite with_evars l cl tac =
+  let do1 l2r f gl =
+    let sigma,c = f (pf_env gl) (project gl) in
+    Refiner.tclWITHHOLES with_evars
+      (general_multi_rewrite l2r with_evars ?tac c) sigma cl gl in
+  let rec doN l2r c = function
     | Precisely n when n <= 0 -> tclIDTAC
     | Precisely 1 -> do1 l2r c
     | Precisely n -> tclTHENFIRST (do1 l2r c) (doN l2r c (Precisely (n-1)))
@@ -216,62 +347,39 @@ let general_multi_multi_rewrite with_evars l cl tac =
     | RepeatPlus -> tclTHENFIRST (do1 l2r c) (doN l2r c RepeatStar)
     | UpTo n when n<=0 -> tclIDTAC
     | UpTo n -> tclTHENFIRST (tclTRY (do1 l2r c)) (doN l2r c (UpTo (n-1)))
-  in 
+  in
   let rec loop = function
     | [] -> tclIDTAC
     | (l2r,m,c)::l -> tclTHENFIRST (doN l2r c m) (loop l)
   in loop l
 
-(* Conditional rewriting, the success of a rewriting is related 
-   to the resolution of the conditions by a given tactic *)
-
-let conditional_rewrite lft2rgt tac (c,bl) = 
-  tclTHENSFIRSTn
-    (general_rewrite_ebindings lft2rgt all_occurrences (c,bl) false)
-    [|tclIDTAC|] (tclCOMPLETE tac)
-
-let rewriteLR_bindings = general_rewrite_bindings true all_occurrences
-let rewriteRL_bindings = general_rewrite_bindings false all_occurrences
-
-let rewriteLR = general_rewrite true all_occurrences
-let rewriteRL = general_rewrite false all_occurrences
-
-let rewriteLRin_bindings = general_rewrite_bindings_in true all_occurrences
-let rewriteRLin_bindings = general_rewrite_bindings_in false all_occurrences
-
-let conditional_rewrite_in lft2rgt id tac (c,bl) = 
-  tclTHENSFIRSTn
-    (general_rewrite_ebindings_in lft2rgt all_occurrences id (c,bl) false)
-    [|tclIDTAC|] (tclCOMPLETE tac)
-
-let rewriteRL_clause = function
-  | None -> rewriteRL_bindings
-  | Some id -> rewriteRLin_bindings id
+let rewriteLR = general_rewrite true all_occurrences true
+let rewriteRL = general_rewrite false all_occurrences true
 
 (* Replacing tactics *)
 
 (* eq,sym_eq : equality on Type and its symmetry theorem
    c2 c1 : c1 is to be replaced by c2
    unsafe : If true, do not check that c1 and c2 are convertible
-   tac : Used to prove the equality c1 = c2 
+   tac : Used to prove the equality c1 = c2
    gl : goal *)
 
-let multi_replace clause c2 c1 unsafe try_prove_eq_opt gl = 
-  let try_prove_eq = 
-    match try_prove_eq_opt with 
+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 ->  tclCOMPLETE tac
   in
-  let t1 = pf_apply get_type_of gl c1 
+  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
+    let sym = build_coq_eq_sym () in
     let eq = applist (e, [t1;c1;c2]) in
     tclTHENS (assert_as false None eq)
-      [onLastHyp (fun id -> 
-	tclTHEN 
-	  (tclTRY (general_multi_rewrite false false (inj_open (mkVar id),NoBindings) clause))
+      [onLastHypId (fun id ->
+	tclTHEN
+	  (tclTRY (general_multi_rewrite false false (mkVar id,NoBindings) clause))
 	  (clear [id]));
        tclFIRST
 	 [assumption;
@@ -281,7 +389,7 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt gl =
       ] gl
   else
     error "Terms do not have convertible types."
-  
+
 
 let replace c2 c1 gl = multi_replace onConcl c2 c1 false None gl
 
@@ -291,7 +399,7 @@ 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 = multi_replace (onHyp id) c2 c1 false (Some tac) gl
 
-let replace_in_clause_maybe_by c2 c1 cl tac_opt 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
@@ -346,8 +454,8 @@ let find_positions env sigma 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 
+
+      | Construct sp1, Construct sp2
           when List.length args1 = mis_constructor_nargs_env env sp1
             ->
 	  let sorts = list_intersect sorts (allowed_sorts env (fst sp1)) in
@@ -365,14 +473,14 @@ let find_positions env sigma t1 t2 =
 	  else []
 
       | _ ->
-	  let t1_0 = applist (hd1,args1) 
+	  let t1_0 = applist (hd1,args1)
           and t2_0 = applist (hd2,args2) in
-          if is_conv env sigma t1_0 t2_0 then 
+          if is_conv env sigma t1_0 t2_0 then
 	    []
           else
 	    let ty1_0 = get_type_of env sigma t1_0 in
 	    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 
+	    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)
@@ -384,7 +492,7 @@ let discriminable env sigma t1 t2 =
     | Inl _ -> true
     | _ -> false
 
-let injectable env sigma t1 t2 = 
+let injectable env sigma t1 t2 =
     match find_positions env sigma t1 t2 with
     | Inl _ | Inr [] -> false
     | Inr _ -> true
@@ -458,7 +566,7 @@ let descend_then sigma env head dirn =
     try find_rectype env sigma (get_type_of env sigma head)
     with Not_found ->
       error "Cannot project on an inductive type derived from a dependency." in
-  let ind,_ = dest_ind_family indf in
+   let ind,_ = dest_ind_family indf in
   let (mib,mip) = lookup_mind_specif env ind in
   let cstr = get_constructors env indf in
   let dirn_nlams = cstr.(dirn-1).cs_nargs in
@@ -499,13 +607,13 @@ let construct_discriminator sigma env dirn c sort =
   let IndType(indf,_) =
     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 
+       (* one can find Rel(k) in case of dependent constructors
+          like T := c : (A:Set)A->T and a discrimination
           on (c bool true) = (c bool false)
           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
@@ -520,7 +628,7 @@ let construct_discriminator sigma env dirn c sort =
     List.map build_branch(interval 1 (Array.length mip.mind_consnames)) in
   let ci = make_case_info env ind RegularStyle in
   mkCase (ci, p, c, Array.of_list brl)
-    
+
 let rec build_discriminator sigma env dirn c sort = function
   | [] -> construct_discriminator sigma env dirn c sort
   | ((sp,cnum),argnum)::l ->
@@ -541,17 +649,17 @@ let rec build_discriminator sigma env dirn c sort = function
 *)
 
 let gen_absurdity id gl =
-  if is_empty_type (clause_type (onHyp id) gl)
+  if is_empty_type (pf_get_hyp_typ gl id)
   then
     simplest_elim (mkVar id) gl
   else
-    errorlabstrm "Equality.gen_absurdity" 
+    errorlabstrm "Equality.gen_absurdity"
       (str "Not the negation of an equality.")
 
 (* Precondition: eq is leibniz equality
- 
+
    returns ((eq_elim t t1 P i t2), absurd_term)
-   where  P=[e:t]discriminator 
+   where  P=[e:t]discriminator
           absurd_term=False
 *)
 
@@ -566,18 +674,17 @@ exception NotDiscriminable
 let eq_baseid = id_of_string "e"
 
 let apply_on_clause (f,t) clause =
-  let sigma = Evd.evars_of clause.evd in
+  let sigma =  clause.evd in
   let f_clause = mk_clenv_from_env clause.env sigma None (f,t) in
-  let argmv = 
+  let argmv =
     (match kind_of_term (last_arg f_clause.templval.Evd.rebus) with
      | Meta mv -> mv
      | _  -> errorlabstrm "" (str "Ill-formed clause applicator.")) in
   clenv_fchain argmv f_clause clause
 
-let discr_positions env sigma (lbeq,(t,t1,t2)) eq_clause cpath dirn sort =
+let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause 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 eqn = mkApp(lbeq.eq,[|t;t1;t2|]) 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
@@ -585,16 +692,16 @@ let discr_positions env sigma (lbeq,(t,t1,t2)) eq_clause cpath dirn sort =
   let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
   let pf = clenv_value_cast_meta absurd_clause in
   tclTHENS (cut_intro absurd_term)
-    [onLastHyp gen_absurdity; refine pf]
+    [onLastHypId gen_absurdity; refine pf]
 
-let discrEq (lbeq,(t,t1,t2) as u) eq_clause gls =
-  let sigma = Evd.evars_of eq_clause.evd in
+let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause gls =
+  let sigma = eq_clause.evd 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 sort = pf_apply get_type_of gls (pf_concl gls) in 
+	let sort = pf_apply get_type_of gls (pf_concl gls) in
 	discr_positions env sigma u eq_clause cpath dirn sort gls
 
 let onEquality with_evars tac (c,lbindc) gls =
@@ -603,39 +710,43 @@ let onEquality with_evars tac (c,lbindc) gls =
   let eq_clause = make_clenv_binding gls (c,t') lbindc in
   let eq_clause' = clenv_pose_dependent_evars with_evars eq_clause in
   let eqn = clenv_type eq_clause' in
-  let eq =
-    try find_eq_data_decompose eqn
-    with PatternMatchingFailure ->
-      errorlabstrm "" (str"No primitive equality found.") in
+  let eq,eq_args = find_this_eq_data_decompose gls eqn in
   tclTHEN
-    (Refiner.tclEVARS (Evd.evars_of eq_clause'.evd)) 
-    (tac eq eq_clause') gls
+    (Refiner.tclEVARS eq_clause'.evd)
+    (tac (eq,eqn,eq_args) eq_clause') gls
 
 let onNegatedEquality with_evars tac gls =
   let ccl = pf_concl gls in
   match kind_of_term (hnf_constr (pf_env gls) (project gls) ccl) with
   | Prod (_,t,u) when is_empty_type u ->
       tclTHEN introf
-        (onLastHyp (fun id -> 
+        (onLastHypId (fun id ->
           onEquality with_evars tac (mkVar id,NoBindings))) gls
-  | _ -> 
+  | _ ->
       errorlabstrm "" (str "Not a negated primitive equality.")
 
 let discrSimpleClause with_evars = function
   | None -> onNegatedEquality with_evars discrEq
-  | Some ((_,id),_) -> onEquality with_evars discrEq (mkVar id,NoBindings)
+  | Some id -> onEquality with_evars discrEq (mkVar id,NoBindings)
 
 let discr with_evars = onEquality with_evars discrEq
 
-let discrClause with_evars = onClauses (discrSimpleClause with_evars)
+let discrClause with_evars = onClause (discrSimpleClause with_evars)
 
-let discrEverywhere with_evars = 
+let discrEverywhere with_evars =
+(*
   tclORELSE
-    (Tacticals.tryAllClauses
-      (fun cl -> tclCOMPLETE (discrSimpleClause with_evars cl)))
-    (fun gls -> 
+*)
+    (if discr_do_intro () then
+      (tclTHEN
+	(tclREPEAT introf)
+	(Tacticals.tryAllHyps
+          (fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings)))))
+     else (* <= 8.2 compat *)
+       Tacticals.tryAllHypsAndConcl (discrSimpleClause with_evars))
+(*    (fun gls ->
        errorlabstrm "DiscrEverywhere" (str"No discriminable equalities."))
-
+*)
 let discr_tac with_evars = function
   | None -> discrEverywhere with_evars
   | Some c -> onInductionArg (discr with_evars) c
@@ -645,8 +756,8 @@ let discrHyp id gls = discrClause false (onHyp id) gls
 
 (* returns the sigma type (sigS, sigT) with the respective
     constructor depending on the sort *)
-(* J.F.: correction du bug #1167 en accord avec Hugo. *) 
-   
+(* J.F.: correction du bug #1167 en accord avec Hugo. *)
+
 let find_sigma_data s = build_sigma_type ()
 
 (* [make_tuple env sigma (rterm,rty) lind] assumes [lind] is the lesser
@@ -699,8 +810,8 @@ let minimal_free_rels_rec env sigma =
   in minimalrec_free_rels_rec Intset.empty
 
 (* [sig_clausal_form siglen ty]
-    
-   Will explode [siglen] [sigS,sigT ]'s on [ty] (depending on the 
+
+   Will explode [siglen] [sigS,sigT ]'s on [ty] (depending on the
    type of ty), and return:
 
    (1) a pattern, with meta-variables in it for various arguments,
@@ -714,9 +825,9 @@ let minimal_free_rels_rec env sigma =
 
    (4) a typing for each patvar
 
-   WARNING: No checking is done to make sure that the 
+   WARNING: No checking is done to make sure that the
             sigS(or sigT)'s are actually there.
-          - Only homogeneous pairs are built i.e. pairs where all the 
+          - Only homogeneous pairs are built i.e. pairs where all the
    dependencies are of the same sort
 
    [sig_clausal_form] proceed as follows: the default tuple is
@@ -735,7 +846,7 @@ let minimal_free_rels_rec env sigma =
  *)
 
 let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
-  let { intro = exist_term } = find_sigma_data sort_of_ty in 
+  let { intro = exist_term } = find_sigma_data sort_of_ty in
   let evdref = ref (Evd.create_goal_evar_defs sigma) in
   let rec sigrec_clausal_form siglen p_i =
     if siglen = 0 then
@@ -745,17 +856,17 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
 	(* the_conv_x had a side-effect on evdref *)
 	dflt
       else
-	error "Cannot solve an unification problem."
+	error "Cannot solve a unification problem."
     else
-      let (a,p_i_minus_1) = match whd_beta_stack (evars_of !evdref) p_i with
+      let (a,p_i_minus_1) = match whd_beta_stack !evdref p_i with
 	| (_sigS,[a;p]) -> (a,p)
  	| _ -> anomaly "sig_clausal_form: should be a sigma type" in
       let ev = Evarutil.e_new_evar evdref env a in
       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 (Evd.evars_of !evdref) 
-	(destEvar ev)
+  	Evd.existential_opt_value !evdref
+ 	  (destEvar ev)
       with
 	| Some w ->
             let w_type = type_of env sigma w in
@@ -766,7 +877,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
 	| None -> anomaly "Not enough components to build the dependent tuple"
   in
   let scf = sigrec_clausal_form siglen ty in
-  Evarutil.nf_evar (Evd.evars_of !evdref) scf
+  Evarutil.nf_evar !evdref scf
 
 (* The problem is to build a destructor (a generalization of the
    predecessor) which, when applied to a term made of constructors
@@ -831,7 +942,7 @@ let make_iterated_tuple env sigma dflt (z,zty) =
   let sort_of_zty = get_sort_of env sigma zty in
   let sorted_rels = Sort.list (<) (Intset.elements rels) in
   let (tuple,tuplety) =
-    List.fold_left (make_tuple env sigma) (z,zty) sorted_rels 
+    List.fold_left (make_tuple env sigma) (z,zty) sorted_rels
   in
   assert (closed0 tuplety);
   let n = List.length sorted_rels in
@@ -856,29 +967,29 @@ let build_injector sigma env dflt c cpath =
 
 (*
 let try_delta_expand env sigma t =
-  let whdt = whd_betadeltaiota env sigma t  in 
+  let whdt = whd_betadeltaiota env sigma t  in
   let rec hd_rec c  =
     match kind_of_term c with
       | Construct _ -> whdt
       | App (f,_)  -> hd_rec f
       | Cast (c,_,_) -> hd_rec c
       | _  -> t
-  in 
-  hd_rec whdt 
+  in
+  hd_rec whdt
 *)
 
-(* Given t1=t2 Inj calculates the whd normal forms of t1 and t2 and it 
+(* 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 simplify_args env sigma t = 
+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])
+    | eq, [t;c1;c2] -> applist (eq,[t;simpl env sigma c1;simpl env sigma c2])
+    | eq, [t1;c1;t2;c2] -> applist (eq,[t1;simpl env sigma c1;t2;simpl env sigma c2])
     | _ -> t
 
-let inject_at_positions env sigma (eq,(t,t1,t2)) eq_clause posns =
+let inject_at_positions env sigma (eq,_,(t,t1,t2)) eq_clause posns tac =
   let e = next_ident_away eq_baseid (ids_of_context env) in
   let e_env = push_named (e,None,t) env in
   let injectors =
@@ -896,25 +1007,29 @@ let inject_at_positions env sigma (eq,(t,t1,t2)) eq_clause posns =
       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
+  tclTHEN
+    (tclMAP
+      (fun (pf,ty) -> tclTHENS (cut ty) [tclIDTAC; refine pf])
+      injectors)
+    (tac (List.length injectors))
 
 exception Not_dep_pair
 
+let eq_dec_scheme_kind_name = ref (fun _ -> failwith "eq_dec_scheme undefined")
+let set_eq_dec_scheme_kind k = eq_dec_scheme_kind_name := (fun _ -> k)
 
-let injEq ipats (eq,(t,t1,t2)) eq_clause =
-  let sigma = Evd.evars_of eq_clause.evd in
+let injEq ipats (eq,_,(t,t1,t2) as u) eq_clause =
+  let sigma = eq_clause.evd in
   let env = eq_clause.env in
   match find_positions env sigma t1 t2 with
     | Inl _ ->
 	errorlabstrm "Inj"
 	  (str"Not a projectable equality but a discriminable one.")
     | Inr [] ->
-	errorlabstrm "Equality.inj" 
+	errorlabstrm "Equality.inj"
 	   (str"Nothing to do, it is an equality between convertible terms.")
     | Inr posns ->
-(* Est-ce utile à partir du moment où les arguments projetés subissent "nf" ?
+(* 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
 *)
@@ -922,7 +1037,7 @@ let injEq ipats (eq,(t,t1,t2)) eq_clause =
 (* fetch the informations of the  pair *)
         let ceq = constr_of_global Coqlib.glob_eq in
         let sigTconstr () = (Coqlib.build_sigma_type()).Coqlib.typ in
-        let eqTypeDest = fst (destApp t) in 
+        let eqTypeDest = fst (destApp t) in
         let _,ar1 = destApp t1 and
             _,ar2 = destApp t2 in
         let ind = destInd ar1.(0) in
@@ -933,27 +1048,26 @@ let injEq ipats (eq,(t,t1,t2)) eq_clause =
 (* and compare the fst arguments of the dep pair *)
         let new_eq_args = [|type_of env sigma (ar1.(3));ar1.(3);ar2.(3)|] in
         if ( (eqTypeDest = sigTconstr()) &&
-             (Ind_tables.check_dec_proof ind=true) &&
+             (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) ind=true) &&
              (is_conv env sigma (ar1.(2)) (ar2.(2)) = true))
-              then ( 
+              then (
 (* Require Import Eqdec_dec copied from vernac_require in vernacentries.ml*)
-              let qidl = qualid_of_reference 
+              let qidl = qualid_of_reference
                 (Ident (dummy_loc,id_of_string "Eqdep_dec")) in
-              Library.require_library [qidl] (Some false); 
+              Library.require_library [qidl] (Some false);
 (* cut with the good equality and prove the requested goal *)
               tclTHENS (cut (mkApp (ceq,new_eq_args)) )
                [tclIDTAC; tclTHEN (apply (
                   mkApp(inj2,
-                        [|ar1.(0);Ind_tables.find_eq_dec_proof ind;
+                        [|ar1.(0);mkConst (find_scheme (!eq_dec_scheme_kind_name()) ind);
                           ar1.(1);ar1.(2);ar1.(3);ar2.(3)|])
                   )) (Auto.trivial [] [])
                 ]
 (* not a dep eq or no decidable type found *)
-            ) else (raise Not_dep_pair) 
+            ) else (raise Not_dep_pair)
         ) with _ ->
-	tclTHEN
-	  (inject_at_positions env sigma (eq,(t,t1,t2)) eq_clause posns)
-	  (intros_pattern no_move ipats)
+	  inject_at_positions env sigma u eq_clause posns
+	    (fun _ -> intros_pattern no_move ipats)
 
 let inj ipats with_evars = onEquality with_evars (injEq ipats)
 
@@ -964,21 +1078,17 @@ let injClause ipats with_evars = function
 let injConcl gls  = injClause [] false None gls
 let injHyp id gls = injClause [] false (Some (ElimOnIdent (dummy_loc,id))) gls
 
-let decompEqThen ntac (lbeq,(t,t1,t2) as u) clause gls =
-  let sort = pf_apply get_type_of gls (pf_concl gls) in 
-  let sigma = Evd.evars_of clause.evd in
-  let env = pf_env gls in 
+let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause gls =
+  let sort = pf_apply get_type_of gls (pf_concl gls) in
+  let sigma =  clause.evd in
+  let env = pf_env gls in
   match find_positions env sigma t1 t2 with
     | Inl (cpath, (_,dirn), _) ->
 	discr_positions env sigma u clause 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)) clause
-	    (List.rev posns))
-	  (ntac (List.length posns))
-	  gls
+	inject_at_positions env sigma u clause (List.rev posns) ntac gls
 
 let dEqThen with_evars ntac = function
   | None -> onNegatedEquality with_evars (decompEqThen ntac)
@@ -986,28 +1096,27 @@ let dEqThen with_evars ntac = function
 
 let dEq with_evars = dEqThen with_evars (fun x -> tclIDTAC)
 
-let rewrite_msg = function 
-  | None -> str "passed term is not a primitive equality" 
-  | Some id -> pr_id id ++ str "does not satisfy preconditions "
+let swap_equality_args = function
+  | MonomorphicLeibnizEq (e1,e2) -> [e2;e1]
+  | PolymorphicLeibnizEq (t,e1,e2) -> [t;e2;e1]
+  | HeterogenousEq (t1,e1,t2,e2) -> [t2;e2;t1;e1]
 
 let swap_equands gls eqn =
-  let (lbeq,(t,e1,e2)) = find_eq_data_decompose eqn in 
-  applist(lbeq.eq,[t;e2;e1])
+  let (lbeq,eq_args) = find_eq_data eqn in
+  applist(lbeq.eq,swap_equality_args eq_args)
 
 let swapEquandsInConcl gls =
-  let (lbeq,(t,e1,e2)) = find_eq_data_decompose (pf_concl gls) in
+  let (lbeq,eq_args) = find_eq_data (pf_concl gls) in
   let sym_equal = lbeq.sym in
-  refine (applist(sym_equal,[t;e2;e1;Evarutil.mk_new_meta()])) gls
-
-let swapEquandsInHyp id gls =
-  cut_replacing id (swap_equands gls (pf_get_hyp_typ gls id))
-    (tclTHEN swapEquandsInConcl) gls
+  refine
+    (applist(sym_equal,(swap_equality_args eq_args@[Evarutil.mk_new_meta()])))
+    gls
 
 (* Refine from [|- P e2] to [|- P e1] and [|- e1=e2:>t] (body is P (Rel 1)) *)
 
 let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
   (* find substitution scheme *)
-  let eq_elim = find_elim lbeq.eq false None gls in
+  let eq_elim = find_elim lbeq.eq (Some false) false None [e1;e2] gls in
   (* build substitution predicate *)
   let p = lambda_create (pf_env gls) (t,body) in
   (* apply substitution scheme *)
@@ -1020,17 +1129,22 @@ let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
 
    (existT e1 (existT e2 ... (existT en en+1) ... ))
 
+   of type {x1:T1 & {x2:T2(x1) & ... {xn:Tn(x1..xn-1) & en+1 } } }
+
    and B might contain instances of the ei, we will return the term:
 
-   ([x1:ty(e1)]...[xn:ty(en)]B
-    (projS1 (mkRel 1))
-    (projS1 (projS2 (mkRel 1)))
-    ... etc ...)
+   ([x1:ty1]...[xn+1:tyn+1]B
+    (projT1 (mkRel 1))
+    (projT1 (projT2 (mkRel 1)))
+    ...
+    (projT1 (projT2^n (mkRel 1)))
+    (projT2 (projT2^n (mkRel 1)))
 
-   That is, we will abstract out the terms e1...en+1 as usual, but
+   That is, we will abstract out the terms e1...en+1 of types
+   t1 (=_beta T1), ..., tn+1 (=_beta Tn+1(e1..en)) as usual, but
    will then produce a term in which the abstraction is on a single
    term - the debruijn index [mkRel 1], which will be of the same type
-   as dep_pair.
+   as dep_pair (note that the abstracted body may not be typable!).
 
    ALGORITHM for abstraction:
 
@@ -1041,7 +1155,7 @@ let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
 
  *)
 
-let decomp_tuple_term env c t = 
+let decomp_tuple_term env c t =
   let rec decomprec inner_code ex exty =
     try
       let {proj1=p1; proj2=p2},(a,p,car,cdr) = find_sigma_data_decompose ex in
@@ -1054,23 +1168,32 @@ let decomp_tuple_term env c t =
   in
   List.split (decomprec (mkRel 1) c t)
 
-let subst_tuple_term env sigma dep_pair b =
-  let typ = get_type_of env sigma dep_pair in
-  let e_list,proj_list = decomp_tuple_term env dep_pair typ in
+let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
+  let typ = get_type_of env sigma dep_pair1 in
+  (* We rewrite dep_pair1 ... *)
+  let e1_list,proj_list = decomp_tuple_term env dep_pair1 typ in
   let abst_B =
     List.fold_right
-      (fun (e,t) body -> lambda_create env (t,subst_term e body)) e_list b in
-  beta_applist(abst_B,proj_list)
+      (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 *)
+  let expected_goal = nf_betaiota sigma expected_goal in
+  pred_body,expected_goal
 
-(* Comme "replace" mais decompose les egalites dependantes *)
+(* Like "replace" but decompose dependent equalities *)
 
 exception NothingToRewrite
 
 let cutSubstInConcl_RL eqn gls =
-  let (lbeq,(t,e1,e2 as eq)) = find_eq_data_decompose eqn in
-  let body = pf_apply subst_tuple_term gls e2 (pf_concl gls) in
+  let (lbeq,(t,e1,e2 as eq)) = find_eq_data_decompose gls eqn in
+  let body,expected_goal = pf_apply subst_tuple_term gls e2 e1 (pf_concl gls) in
   if not (dependent (mkRel 1) body) then raise NothingToRewrite;
-  bareRevSubstInConcl lbeq body eq gls
+  tclTHENFIRST
+    (bareRevSubstInConcl lbeq body eq)
+    (convert_concl expected_goal DEFAULTcast) gls
 
 (* |- (P e1)
      BY CutSubstInConcl_LR (eq T e1 e2)
@@ -1085,11 +1208,14 @@ let cutSubstInConcl_LR eqn gls =
 let cutSubstInConcl l2r =if l2r then cutSubstInConcl_LR else cutSubstInConcl_RL
 
 let cutSubstInHyp_LR eqn id gls =
-  let (lbeq,(t,e1,e2 as eq)) = find_eq_data_decompose eqn in 
-  let body = pf_apply subst_tuple_term gls e1 (pf_get_hyp_typ gls id) in
+  let (lbeq,(t,e1,e2 as eq)) = find_eq_data_decompose gls eqn in
+  let idtyp = pf_get_hyp_typ gls id in
+  let body,expected_goal = pf_apply subst_tuple_term gls e1 e2 idtyp in
   if not (dependent (mkRel 1) body) then raise NothingToRewrite;
-  cut_replacing id (subst1 e2 body)
-    (tclTHENFIRST (bareRevSubstInConcl lbeq body eq)) gls
+  cut_replacing id expected_goal
+    (tclTHENFIRST
+      (bareRevSubstInConcl lbeq body eq)
+      (refine_no_check (mkVar id))) gls
 
 let cutSubstInHyp_RL eqn id gls =
   (tclTHENS (cutSubstInHyp_LR (swap_equands gls eqn) id)
@@ -1099,12 +1225,12 @@ let cutSubstInHyp_RL eqn id gls =
 let cutSubstInHyp l2r = if l2r then cutSubstInHyp_LR else cutSubstInHyp_RL
 
 let try_rewrite tac gls =
-  try 
+  try
     tac gls
-  with 
+  with
     | PatternMatchingFailure ->
 	errorlabstrm "try_rewrite" (str "Not a primitive equality here.")
-    | e when catchable_exception e -> 
+    | e when catchable_exception e ->
 	errorlabstrm "try_rewrite"
           (strbrk "Cannot find a well-typed generalization of the goal that makes the proof progress.")
     | NothingToRewrite ->
@@ -1122,7 +1248,8 @@ let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None
 
 let substClause l2r c cls gls =
   let eq = pf_apply get_type_of gls c in
-  tclTHENS (cutSubstClause l2r eq cls) [tclIDTAC; exact_no_check c] gls
+  tclTHENS (cutSubstClause l2r eq cls)
+    [tclIDTAC; exact_no_check c] gls
 
 let rewriteClause l2r c cls = try_rewrite (substClause l2r c cls)
 let rewriteInHyp l2r c id = rewriteClause l2r c (Some id)
@@ -1155,8 +1282,7 @@ let unfold_body x gl =
       | _ -> errorlabstrm "unfold_body"
           (pr_id x ++ str" is not a defined hypothesis.") in
   let aft = afterHyp x gl in
-  let hl = List.fold_right 
-    (fun (y,yval,_) cl -> ((all_occurrences_expr,y),InHyp) :: cl) aft [] in
+  let hl = List.fold_right (fun (y,yval,_) cl -> (y,InHyp) :: cl) aft [] in
   let xvar = mkVar x in
   let rfun _ _ c = replace_term xvar xval c in
   tclTHENLIST
@@ -1165,19 +1291,22 @@ let unfold_body x gl =
 
 
 
+let restrict_to_eq_and_identity eq = (* compatibility *)
+  if eq <> constr_of_global glob_eq && eq <> constr_of_global glob_identity then
+    raise PatternMatchingFailure
 
 exception FoundHyp of (identifier * constr * bool)
 
 (* tests whether hyp [c] is [x = t] or [t = x], [x] not occuring in [t] *)
-let is_eq_x x (id,_,c) =
+let is_eq_x gl x (id,_,c) =
   try
-    let (_,lhs,rhs) = snd (find_eq_data_decompose c) in
+    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))
   with PatternMatchingFailure ->
     ()
 
-let subst_one x gl = 
+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 *)
@@ -1185,9 +1314,9 @@ let subst_one x gl =
   (* x is a variable: *)
   let varx = mkVar x in
   (* Find a non-recursive definition for x *)
-  let (hyp,rhs,dir) = 
+  let (hyp,rhs,dir) =
     try
-      let test hyp _ = is_eq_x varx hyp in
+      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 ++
@@ -1195,8 +1324,8 @@ let subst_one x gl =
     with FoundHyp res -> res
   in
   (* The set of hypotheses using x *)
-  let depdecls = 
-    let test (id,_,c as dcl) = 
+  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
@@ -1219,10 +1348,10 @@ let subst_one x gl =
 	  (Some (replace_term varx rhs htyp)) nowhere
   in
   let need_rewrite = dephyps <> [] || depconcl in
-  tclTHENLIST 
+  tclTHENLIST
     ((if need_rewrite then
       [generalize abshyps;
-       (if dir then rewriteLR else rewriteRL) (mkVar hyp);
+       general_rewrite dir all_occurrences dep_proof_ok (mkVar hyp);
        thin dephyps;
        tclMAP introtac depdecls]
     else
@@ -1230,111 +1359,81 @@ let subst_one x gl =
        tclMAP introtac depdecls]) @
      [tclTRY (clear [x;hyp])]) gl
 
-let subst ids = tclTHEN tclNORMEVAR (tclMAP subst_one ids)
+let subst_gen dep_proof_ok ids =
+  tclTHEN tclNORMEVAR (tclMAP (subst_one dep_proof_ok) ids)
+
+let subst = subst_gen true
 
-let subst_all gl =
+type subst_tactic_flags = {
+  only_leibniz : bool;
+  rewrite_dependent_proof : bool
+}
+
+let default_subst_tactic_flags () =
+  if Flags.version_strictly_greater Flags.V8_2 then
+    { only_leibniz = false; rewrite_dependent_proof = true }
+  else
+    { only_leibniz = true; rewrite_dependent_proof = false }
+
+let subst_all ?(flags=default_subst_tactic_flags ()) gl =
   let test (_,c) =
     try
-      let (_,x,y) = snd (find_eq_data_decompose c) in
+      let lbeq,(_,x,y) = find_eq_data_decompose gl c in
+      if flags.only_leibniz then restrict_to_eq_and_identity lbeq.eq;
       (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
       if eq_constr x y then failwith "caught";
-      match kind_of_term x with Var x -> x | _ -> 
+      match kind_of_term x with Var x -> x | _ ->
       match kind_of_term y with Var y -> y | _ -> failwith "caught"
     with PatternMatchingFailure -> failwith "caught"
   in
   let ids = map_succeed test (pf_hyps_types gl) in
   let ids = list_uniquize ids in
-  subst ids gl
-
+  subst_gen flags.rewrite_dependent_proof ids gl
 
-(* Rewrite the first assumption for which the condition faildir does not fail 
+(* Rewrite the first assumption for which the condition faildir does not fail
    and gives the direction of the rewrite *)
 
 let cond_eq_term_left c t gl =
   try
-    let (_,x,_) = snd (find_eq_data_decompose t) in
+    let (_,x,_) = snd (find_eq_data_decompose gl t) in
     if pf_conv_x gl c x then true else failwith "not convertible"
   with PatternMatchingFailure -> failwith "not an equality"
 
-let cond_eq_term_right c t gl = 
+let cond_eq_term_right c t gl =
   try
-    let (_,_,x) = snd (find_eq_data_decompose t) in
+    let (_,_,x) = snd (find_eq_data_decompose gl t) in
     if pf_conv_x gl c x then false else failwith "not convertible"
   with PatternMatchingFailure -> failwith "not an equality"
 
-let cond_eq_term c t gl = 
+let cond_eq_term c t gl =
   try
-    let (_,x,y) = snd (find_eq_data_decompose t) in
-    if pf_conv_x gl c x then true 
+    let (_,x,y) = snd (find_eq_data_decompose gl t) in
+    if pf_conv_x gl c x then true
     else if pf_conv_x gl c y then false
     else failwith "not convertible"
   with PatternMatchingFailure -> failwith "not an equality"
 
-let rewrite_multi_assumption_cond cond_eq_term cl gl = 
-  let rec arec = function 
+let rewrite_multi_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 false (inj_open (mkVar id),NoBindings) cl gl
+    | (id,_,t) ::rest ->
+	begin
+	  try
+	    let dir = cond_eq_term t gl in
+	    general_multi_rewrite dir false (mkVar id,NoBindings) cl gl
 	  with | Failure _ | UserError _ -> arec rest
 	end
-  in 
+  in
   arec (pf_hyps gl)
 
-let replace_multi_term dir_opt c  = 
-  let cond_eq_fun = 
-    match dir_opt with 
+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_multi_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)
-   
-let replace_term t = rewrite_assumption_cond (cond_eq_term t)
-   
-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)
+  in
+  rewrite_multi_assumption_cond cond_eq_fun
 
-let _ = Tactics.register_general_multi_rewrite general_multi_rewrite
+let _ = Tactics.register_general_multi_rewrite
+  (fun b evars t cls -> general_multi_rewrite b evars t cls)