path: root/tactics/rewrite.ml

(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <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        *)
(************************************************************************)

(*i camlp4deps: "grammar/grammar.cma" i*)

open Errors
open Util
open Nameops
open Namegen
open Term
open Vars
open Reduction
open Tacticals
open Tacmach
open Tactics
open Clenv
open Typeclasses
open Typeclasses_errors
open Classes
open Constrexpr
open Globnames
open Evd
open Misctypes
open Locus
open Locusops
open Decl_kinds
open Elimschemes
open Goal
open Environ
open Pp
open Names
open Tacinterp
open Termops
open Entries
open Libnames

(** Typeclass-based generalized rewriting. *)

(** Constants used by the tactic. *)

let classes_dirpath =
  DirPath.make (List.map Id.of_string ["Classes";"Coq"])

let init_setoid () =
  if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
  else Coqlib.check_required_library ["Coq";"Setoids";"Setoid"]

let get_class str =
  let qualid = Qualid (Loc.ghost, qualid_of_string str) in
    lazy (class_info (Nametab.global qualid))

let proper_class = get_class "Coq.Classes.Morphisms.Proper"
let proper_proxy_class = get_class "Coq.Classes.Morphisms.ProperProxy"

let proper_proj = lazy (mkConst (Option.get (pi3 (List.hd (Lazy.force proper_class).cl_projs))))

let make_dir l = DirPath.make (List.rev_map Id.of_string l)

let try_find_global_reference dir s =
  let sp = Libnames.make_path (make_dir ("Coq"::dir)) (Id.of_string s) in
    Nametab.global_of_path sp

let try_find_reference dir s =
  constr_of_global (try_find_global_reference dir s)

let gen_constant dir s = Coqlib.gen_constant "rewrite" dir s
let coq_eq = lazy(gen_constant ["Init"; "Logic"] "eq")
let coq_f_equal = lazy (gen_constant ["Init"; "Logic"] "f_equal")
let coq_all = lazy (gen_constant ["Init"; "Logic"] "all")
let coq_forall = lazy (gen_constant ["Classes"; "Morphisms"] "forall_def")
let impl = lazy (gen_constant ["Program"; "Basics"] "impl")
let arrow = lazy (gen_constant ["Program"; "Basics"] "arrow")

let reflexive_type = lazy (try_find_reference ["Classes"; "RelationClasses"] "Reflexive")
let reflexive_proof = lazy (try_find_reference ["Classes"; "RelationClasses"] "reflexivity")

let symmetric_type = lazy (try_find_reference ["Classes"; "RelationClasses"] "Symmetric")
let symmetric_proof = lazy (try_find_reference ["Classes"; "RelationClasses"] "symmetry")

let transitive_type = lazy (try_find_reference ["Classes"; "RelationClasses"] "Transitive")
let transitive_proof = lazy (try_find_reference ["Classes"; "RelationClasses"] "transitivity")

let coq_inverse = lazy (gen_constant ["Program"; "Basics"] "flip")

let inverse car rel = mkApp (Lazy.force coq_inverse, [| car ; car; mkProp; rel |])

let forall_relation = lazy (gen_constant ["Classes"; "Morphisms"] "forall_relation")
let pointwise_relation = lazy (gen_constant ["Classes"; "Morphisms"] "pointwise_relation")
let respectful = lazy (gen_constant ["Classes"; "Morphisms"] "respectful")
let default_relation = lazy (gen_constant ["Classes"; "SetoidTactics"] "DefaultRelation")
let subrelation = lazy (gen_constant ["Classes"; "RelationClasses"] "subrelation")
let do_subrelation = lazy (gen_constant ["Classes"; "Morphisms"] "do_subrelation")
let apply_subrelation = lazy (gen_constant ["Classes"; "Morphisms"] "apply_subrelation")
let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "relation")
let mk_relation a = mkApp (Lazy.force coq_relation, [| a |])
let rewrite_relation_class = lazy (gen_constant ["Classes"; "RelationClasses"] "RewriteRelation")

let proper_type = lazy (constr_of_global (Lazy.force proper_class).cl_impl)
let proper_proxy_type = lazy (constr_of_global (Lazy.force proper_proxy_class).cl_impl)

(** Utility functions *)

let split_head = function
    hd :: tl -> hd, tl
  | [] -> assert(false)

let evd_convertible env evd x y =
  try ignore(Evarconv.the_conv_x env x y evd); true
  with e when Errors.noncritical e -> false

let convertible env evd x y =
  Reductionops.is_conv env evd x y

(** Bookkeeping which evars are constraints so that we can
    remove them at the end of the tactic. *)

let goalevars evars = fst evars
let cstrevars evars = snd evars

let new_cstr_evar (evd,cstrs) env t =
  let evd', t = Evarutil.new_evar evd env t in
    (evd', Evar.Set.add (fst (destEvar t)) cstrs), t

(** Building or looking up instances. *)

let proper_proof env evars carrier relation x =
  let goal = mkApp (Lazy.force proper_proxy_type, [| carrier ; relation; x |])
  in new_cstr_evar evars env goal

let extends_undefined evars evars' =
  let f ev evi found = found || not (Evd.mem evars ev)
  in fold_undefined f evars' false

let find_class_proof proof_type proof_method env evars carrier relation =
  try
    let goal = mkApp (Lazy.force proof_type, [| carrier ; relation |]) in
    let evars', c = Typeclasses.resolve_one_typeclass env evars goal in
      if extends_undefined evars evars' then raise Not_found
      else mkApp (Lazy.force proof_method, [| carrier; relation; c |])
  with e when Logic.catchable_exception e -> raise Not_found

let get_reflexive_proof env = find_class_proof reflexive_type reflexive_proof env
let get_symmetric_proof env = find_class_proof symmetric_type symmetric_proof env
let get_transitive_proof env = find_class_proof transitive_type transitive_proof env

(** Build an infered signature from constraints on the arguments and expected output
    relation *)

let build_signature evars env m (cstrs : (types * types option) option list)
    (finalcstr : (types * types option) option) =
  let mk_relty evars newenv ty obj =
    match obj with
      | None | Some (_, None) ->
	  let relty = mk_relation ty in
	    if closed0 ty then
	      let env' = Environ.reset_with_named_context (Environ.named_context_val env) env in
		new_cstr_evar evars env' relty
	    else new_cstr_evar evars newenv relty
      | Some (x, Some rel) -> evars, rel
  in
  let rec aux env evars ty l =
    let t = Reductionops.whd_betadeltaiota env (fst evars) ty in
      match kind_of_term t, l with
      | Prod (na, ty, b), obj :: cstrs ->
	  if noccurn 1 b (* non-dependent product *) then
	    let ty = Reductionops.nf_betaiota (fst evars) ty in
	    let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in
	    let evars, relty = mk_relty evars env ty obj in
	    let newarg = mkApp (Lazy.force respectful, [| ty ; b' ; relty ; arg |]) in
	      evars, mkProd(na, ty, b), newarg, (ty, Some relty) :: cstrs
	  else
	    let (evars, b, arg, cstrs) = aux (Environ.push_rel (na, None, ty) env) evars b cstrs in
	    let ty = Reductionops.nf_betaiota (fst evars) ty in
	    let pred = mkLambda (na, ty, b) in
	    let liftarg = mkLambda (na, ty, arg) in
	    let arg' = mkApp (Lazy.force forall_relation, [| ty ; pred ; liftarg |]) in
	      if Option.is_empty obj then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs
	      else error "build_signature: no constraint can apply on a dependent argument"
      | _, obj :: _ -> anomaly ~label:"build_signature" (Pp.str "not enough products")
      | _, [] ->
	  (match finalcstr with
	  | None | Some (_, None) ->
	      let t = Reductionops.nf_betaiota (fst evars) ty in
	      let evars, rel = mk_relty evars env t None in
		evars, t, rel, [t, Some rel]
	  | Some (t, Some rel) -> evars, t, rel, [t, Some rel])
  in aux env evars m cstrs

type hypinfo = {
  cl : clausenv;
  ext : Evar.Set.t; (* New evars in this clausenv *)
  prf : constr;
  car : constr;
  rel : constr;
  c1 : constr;
  c2 : constr;
  c  : (Tacinterp.interp_sign * Tacexpr.glob_constr_and_expr with_bindings) option;
  abs : bool;
}

(** Looking up declared rewrite relations (instances of [RewriteRelation]) *)
let is_applied_rewrite_relation env sigma rels t =
  match kind_of_term t with
  | App (c, args) when Array.length args >= 2 ->
      let head = if isApp c then fst (destApp c) else c in
	if eq_constr (Lazy.force coq_eq) head then None
	else
	  (try
	      let params, args = Array.chop (Array.length args - 2) args in
	      let env' = Environ.push_rel_context rels env in
	      let evd, evar = Evarutil.new_evar sigma env' (new_Type ()) in
	      let inst = mkApp (Lazy.force rewrite_relation_class, [| evar; mkApp (c, params) |]) in
	      let _ = Typeclasses.resolve_one_typeclass env' evd inst in
		Some (it_mkProd_or_LetIn t rels)
	  with e when Errors.noncritical e -> None)
  | _ -> None

let rec decompose_app_rel env evd t =
  match kind_of_term t with
  | App (f, args) ->
      if Array.length args > 1 then
	let fargs, args = Array.chop (Array.length args - 2) args in
	  mkApp (f, fargs), args
      else
	let (f', args) = decompose_app_rel env evd args.(0) in
	let ty = Typing.type_of env evd args.(0) in
	let f'' = mkLambda (Name (Id.of_string "x"), ty,
	  mkLambda (Name (Id.of_string "y"), lift 1 ty,
	    mkApp (lift 2 f, [| mkApp (lift 2 f', [| mkRel 2; mkRel 1 |]) |])))
	in (f'', args)
  | _ -> error "The term provided is not an applied relation."

let decompose_applied_relation env sigma orig (c,l) =
  let ctype = Typing.type_of env sigma c in
  let find_rel ty =
    let eqclause = Clenv.make_clenv_binding_env_apply env sigma None (c, ty) l in
    let (equiv, args) = decompose_app_rel env eqclause.evd (Clenv.clenv_type eqclause) in
    let c1 = args.(0) and c2 = args.(1) in
    let ty1, ty2 =
      Typing.type_of env eqclause.evd c1, Typing.type_of env eqclause.evd c2
    in
      if not (evd_convertible env eqclause.evd ty1 ty2) then None
      else
	let value = Clenv.clenv_value eqclause in
	let ext = Evarutil.evars_of_term value in
	  Some { cl=eqclause; ext=ext; prf=value;
		 car=ty1; rel = equiv; c1=c1; c2=c2; c=orig; abs=false; }
  in
    match find_rel ctype with
    | Some c -> c
    | None ->
	let ctx,t' = Reductionops.splay_prod_assum env sigma ctype in (* Search for underlying eq *)
	match find_rel (it_mkProd_or_LetIn t' ctx) with
	| Some c -> c
	| None -> error "The term does not end with an applied homogeneous relation."

let decompose_applied_relation_expr env sigma (is, (c,l)) =
  let sigma, cbl = Tacinterp.interp_open_constr_with_bindings is env sigma (c,l) in
  decompose_applied_relation env sigma (Some (is, (c,l))) cbl

(** Hint database named "rewrite", now created directly in Auto *)

let rewrite_db = Auto.rewrite_db

let rewrite_transparent_state () =
  Auto.Hint_db.transparent_state (Auto.searchtable_map rewrite_db)

let rewrite_unif_flags = {
  Unification.modulo_conv_on_closed_terms = None;
  Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
  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;
  Unification.use_meta_bound_pattern_unification = true;
  Unification.frozen_evars = Evar.Set.empty;
  Unification.restrict_conv_on_strict_subterms = false;
  Unification.modulo_betaiota = false;
  Unification.modulo_eta = true;
  Unification.allow_K_in_toplevel_higher_order_unification = true
}

let rewrite2_unif_flags =
  {  Unification.modulo_conv_on_closed_terms = Some cst_full_transparent_state;
     Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
     Unification.modulo_delta = empty_transparent_state;
     Unification.modulo_delta_types = cst_full_transparent_state;
     Unification.modulo_delta_in_merge = None;
     Unification.check_applied_meta_types = true;
     Unification.resolve_evars = false;
     Unification.use_pattern_unification = true;
     Unification.use_meta_bound_pattern_unification = true;
     Unification.frozen_evars = Evar.Set.empty;
     Unification.restrict_conv_on_strict_subterms = false;
     Unification.modulo_betaiota = true;
     Unification.modulo_eta = true;
     Unification.allow_K_in_toplevel_higher_order_unification = true
  }

let general_rewrite_unif_flags () =
  let ts = rewrite_transparent_state () in
    {  Unification.modulo_conv_on_closed_terms = Some ts;
       Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
       Unification.modulo_delta = ts;
       Unification.modulo_delta_types = ts;
       Unification.modulo_delta_in_merge = None;
       Unification.check_applied_meta_types = true;
       Unification.resolve_evars = false;
       Unification.use_pattern_unification = true;
       Unification.use_meta_bound_pattern_unification = true;
       Unification.frozen_evars = Evar.Set.empty;
       Unification.restrict_conv_on_strict_subterms = false;
       Unification.modulo_betaiota = true;
       Unification.modulo_eta = true;
       Unification.allow_K_in_toplevel_higher_order_unification = true }

let refresh_hypinfo env sigma hypinfo =
    let {c=c} = hypinfo in
      match c with
	| Some c ->
	    (* Refresh the clausenv to not get the same meta twice in the goal. *)
	    decompose_applied_relation_expr env sigma c
	| _ -> hypinfo


let solve_remaining_by by env prf =
  match by with
  | None -> env, prf
  | Some tac ->
    let indep = clenv_independent env in
    let tac = eval_tactic tac in
    let evd' =
      List.fold_right (fun mv evd ->
        let ty = Clenv.clenv_nf_meta env (meta_type evd mv) in
	let c,_ = Pfedit.build_by_tactic env.env ty (Tacticals.New.tclCOMPLETE tac) in
	  meta_assign mv (c, (Conv,TypeNotProcessed)) evd)
      indep env.evd
    in { env with evd = evd' }, prf

let extend_evd sigma ext sigma' =
  Evar.Set.fold (fun i acc ->
    Evd.add acc i (Evarutil.nf_evar_info sigma' (Evd.find sigma' i)))
    ext sigma

let shrink_evd sigma ext =
  Evar.Set.fold (fun i acc -> Evd.remove acc i) ext sigma

let no_constraints cstrs =
  fun ev _ -> not (Evar.Set.mem ev cstrs)

let eq_env x y = x == y

let unify_eqn l2r flags env (sigma, cstrs) hypinfo by t =
  if isEvar t then None
  else try
    let hypinfo =
      if hypinfo.abs || eq_env hypinfo.cl.env env then hypinfo
      else refresh_hypinfo env sigma hypinfo
    in
    let {cl=cl; ext=ext; prf=prf; car=car; rel=rel; c1=c1; c2=c2; abs=abs} =
      hypinfo in
    let left = if l2r then c1 else c2 in
    let evd' = Evd.evars_reset_evd ~with_conv_pbs:true sigma cl.evd in
    let evd'' = extend_evd evd' ext cl.evd in
    let cl = { cl with evd = evd'' } in
    let hypinfo, evd', prf, c1, c2, car, rel =
      if abs then
	  let env' = clenv_unify ~flags:rewrite_unif_flags CONV left t cl in
	    hypinfo, env'.evd, prf, c1, c2, car, rel
      else
	  let env' = clenv_unify ~flags CONV left t cl in
	  let env' = Clenvtac.clenv_pose_dependent_evars true env' in
	  let evd' = Typeclasses.resolve_typeclasses ~filter:(no_constraints cstrs)
	    ~fail:true env'.env env'.evd in
	  let env' = { env' with evd = evd' } in
	  let env', prf = solve_remaining_by by env' (Clenv.clenv_value env') in
	  let nf c = Evarutil.nf_evar env'.evd (Clenv.clenv_nf_meta env' c) in
	  let c1 = nf c1 and c2 = nf c2
	  and car = nf car and rel = nf rel
	  and prf = nf prf in
	  let ty1 = Typing.type_of env'.env env'.evd c1
	  and ty2 = Typing.type_of env'.env env'.evd c2
	  in
	    if convertible env env'.evd ty1 ty2 then
	      (if occur_meta_or_existential prf then
		let hypinfo = refresh_hypinfo env env'.evd hypinfo in
		 (hypinfo, env'.evd, prf, c1, c2, car, rel)
	       else (** Evars have been solved, we can go back to the initial evd,
			but keep the potential refinement of existing evars. *)
		let evd' = shrink_evd env'.evd ext in
		  (hypinfo, evd', prf, c1, c2, car, rel))
	    else raise Reduction.NotConvertible
    in
    let res =
      if l2r then (prf, (car, rel, c1, c2))
      else
	try (mkApp (get_symmetric_proof env evd' car rel,
		   [| c1 ; c2 ; prf |]),
	    (car, rel, c2, c1))
	with Not_found ->
	  (prf, (car, inverse car rel, c2, c1))
    in Some (hypinfo, evd', res)
  with e when Class_tactics.catchable e -> None

let unfold_impl t =
  match kind_of_term t with
    | App (arrow, [| a; b |])(*  when eq_constr arrow (Lazy.force impl) *) ->
	mkProd (Anonymous, a, lift 1 b)
    | _ -> assert false

let unfold_all t =
  match kind_of_term t with
    | App (id, [| a; b |]) (* when eq_constr id (Lazy.force coq_all) *) ->
	(match kind_of_term b with
	  | Lambda (n, ty, b) -> mkProd (n, ty, b)
	  | _ -> assert false)
    | _ -> assert false

let unfold_forall t =
  match kind_of_term t with
    | App (id, [| a; b |]) (* when eq_constr id (Lazy.force coq_all) *) ->
	(match kind_of_term b with
	  | Lambda (n, ty, b) -> mkProd (n, ty, b)
	  | _ -> assert false)
    | _ -> assert false

let arrow_morphism ta tb a b =
  let ap = is_Prop ta and bp = is_Prop tb in
    if ap && bp then mkApp (Lazy.force impl, [| a; b |]), unfold_impl
    else if ap then (* Domain in Prop, CoDomain in Type *)
      mkProd (Anonymous, a, b), (fun x -> x)
    else if bp then (* Dummy forall *)
      mkApp (Lazy.force coq_all, [| a; mkLambda (Anonymous, a, b) |]), unfold_forall
    else (* None in Prop, use arrow *)
      mkApp (Lazy.force arrow, [| a; b |]), unfold_impl

let rec decomp_pointwise n c =
  if Int.equal n 0 then c
  else
    match kind_of_term c with
    | App (f, [| a; b; relb |]) when eq_constr f (Lazy.force pointwise_relation) ->
	decomp_pointwise (pred n) relb
    | App (f, [| a; b; arelb |]) when eq_constr f (Lazy.force forall_relation) ->
	decomp_pointwise (pred n) (Reductionops.beta_applist (arelb, [mkRel 1]))
    | _ -> invalid_arg "decomp_pointwise"

let rec apply_pointwise rel = function
  | arg :: args ->
      (match kind_of_term rel with
      | App (f, [| a; b; relb |]) when eq_constr f (Lazy.force pointwise_relation) ->
	  apply_pointwise relb args
      | App (f, [| a; b; arelb |]) when eq_constr f (Lazy.force forall_relation) ->
	  apply_pointwise (Reductionops.beta_applist (arelb, [arg])) args
      | _ -> invalid_arg "apply_pointwise")
  | [] -> rel

let pointwise_or_dep_relation n t car rel =
  if noccurn 1 car && noccurn 1 rel then
    mkApp (Lazy.force pointwise_relation, [| t; lift (-1) car; lift (-1) rel |])
  else
    mkApp (Lazy.force forall_relation,
	  [| t; mkLambda (n, t, car); mkLambda (n, t, rel) |])

let lift_cstr env evars (args : constr list) c ty cstr =
  let start evars env car =
    match cstr with
    | None | Some (_, None) ->
      new_cstr_evar evars env (mk_relation car)
    | Some (ty, Some rel) -> evars, rel
  in
  let rec aux evars env prod n =
    if Int.equal n 0 then start evars env prod
    else
      match kind_of_term (Reduction.whd_betadeltaiota env prod) with
      | Prod (na, ty, b) ->
	  if noccurn 1 b then
	    let b' = lift (-1) b in
	    let evars, rb = aux evars env b' (pred n) in
	      evars, mkApp (Lazy.force pointwise_relation, [| ty; b'; rb |])
	  else
	    let evars, rb = aux evars (Environ.push_rel (na, None, ty) env) b (pred n) in
	      evars, mkApp (Lazy.force forall_relation,
		    [| ty; mkLambda (na, ty, b); mkLambda (na, ty, rb) |])
      | _ -> raise Not_found
  in
  let rec find env c ty = function
    | [] -> None
    | arg :: args ->
	try let evars, found = aux evars env ty (succ (List.length args)) in
	      Some (evars, found, c, ty, arg :: args)
	with Not_found ->
	  find env (mkApp (c, [| arg |])) (prod_applist ty [arg]) args
  in find env c ty args

let unlift_cstr env sigma = function
  | None -> None
  | Some codom -> Some (decomp_pointwise 1 codom)

type rewrite_flags = { under_lambdas : bool; on_morphisms : bool }

let default_flags = { under_lambdas = true; on_morphisms = true; }

type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *)

type rewrite_proof =
  | RewPrf of constr * constr
  | RewCast of cast_kind

let get_opt_rew_rel = function RewPrf (rel, prf) -> Some rel | _ -> None

type rewrite_result_info = {
  rew_car : constr;
  rew_from : constr;
  rew_to : constr;
  rew_prf : rewrite_proof;
  rew_evars : evars;
}

type 'a rewrite_result =
| Fail
| Same
| Info of 'a

type 'a pure_strategy = 'a -> Environ.env -> Id.t list -> constr -> types ->
  constr option -> evars -> 'a * rewrite_result_info rewrite_result

type strategy = unit pure_strategy

let get_rew_prf r = match r.rew_prf with
  | RewPrf (rel, prf) -> rel, prf
  | RewCast c ->
    let rel = mkApp (Coqlib.build_coq_eq (), [| r.rew_car |]) in
      rel, mkCast (mkApp (Coqlib.build_coq_eq_refl (), [| r.rew_car; r.rew_from |]),
		   c, mkApp (rel, [| r.rew_from; r.rew_to |]))

let resolve_subrelation env avoid car rel prf rel' res =
  if eq_constr rel rel' then res
  else
    let app = mkApp (Lazy.force subrelation, [|car; rel; rel'|]) in
    let evars, subrel = new_cstr_evar res.rew_evars env app in
    let appsub = mkApp (subrel, [| res.rew_from ; res.rew_to ; prf |]) in
      { res with
	rew_prf = RewPrf (rel', appsub);
	rew_evars = evars }

let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' cstr evars =
  let evars, morph_instance, proj, sigargs, m', args, args' =
    let first = match (Array.findi (fun _ b -> not (Option.is_empty b)) args') with
    | Some i -> i
    | None -> invalid_arg "resolve_morphism" in
    let morphargs, morphobjs = Array.chop first args in
    let morphargs', morphobjs' = Array.chop first args' in
    let appm = mkApp(m, morphargs) in
    let appmtype = Typing.type_of env (goalevars evars) appm in
    let cstrs = List.map
      (Option.map (fun r -> r.rew_car, get_opt_rew_rel r.rew_prf))
      (Array.to_list morphobjs')
    in
      (* Desired signature *)
    let evars, appmtype', signature, sigargs =
      build_signature evars env appmtype cstrs cstr
    in
      (* Actual signature found *)
    let cl_args = [| appmtype' ; signature ; appm |] in
    let app = mkApp (Lazy.force proper_type, cl_args) in
    let env' = Environ.push_named
      (Id.of_string "do_subrelation",
       Some (Lazy.force do_subrelation),
       Lazy.force apply_subrelation)
      env
    in
    let evars, morph = new_cstr_evar evars env' app in
      evars, morph, morph, sigargs, appm, morphobjs, morphobjs'
  in
  let projargs, subst, evars, respars, typeargs =
    Array.fold_left2
      (fun (acc, subst, evars, sigargs, typeargs') x y ->
	let (carrier, relation), sigargs = split_head sigargs in
	  match relation with
	  | Some relation ->
	      let carrier = substl subst carrier
	      and relation = substl subst relation in
	      (match y with
	      | None ->
		  let evars, proof = proper_proof env evars carrier relation x in
		    [ proof ; x ; x ] @ acc, subst, evars, sigargs, x :: typeargs'
	      | Some r ->
		  [ snd (get_rew_prf r); r.rew_to; x ] @ acc, subst, evars,
	      sigargs, r.rew_to :: typeargs')
	  | None ->
	      if not (Option.is_empty y) then
		error "Cannot rewrite the argument of a dependent function";
	      x :: acc, x :: subst, evars, sigargs, x :: typeargs')
      ([], [], evars, sigargs, []) args args'
  in
  let proof = applistc proj (List.rev projargs) in
  let newt = applistc m' (List.rev typeargs) in
    match respars with
	[ a, Some r ] -> evars, proof, a, r, oldt, fnewt newt
      | _ -> assert(false)

let apply_constraint env avoid car rel prf cstr res =
  match cstr with
  | None -> res
  | Some r -> resolve_subrelation env avoid car rel prf r res

let apply_rule l2r flags by loccs : (hypinfo * int) pure_strategy =
  let (nowhere_except_in,occs) = convert_occs loccs in
  let is_occ occ =
    if nowhere_except_in
    then Int.List.mem occ occs
    else not (Int.List.mem occ occs)
  in
  fun (hypinfo, occ) env avoid t ty cstr evars ->
    let unif = unify_eqn l2r flags env evars hypinfo by t in
    match unif with
    | None -> ((hypinfo, occ), Fail)
    | Some (hypinfo, evd', (prf, (car, rel, c1, c2))) ->
      let occ = succ occ in
      let res =
        if not (is_occ occ) then Fail
        else if eq_constr t c2 then Same
        else
          let res = { rew_car = ty; rew_from = c1;
                      rew_to = c2; rew_prf = RewPrf (rel, prf);
                      rew_evars = evd', cstrevars evars }
          in Info (apply_constraint env avoid car rel prf cstr res)
      in
      ((hypinfo, occ), res)

let apply_lemma l2r flags c by loccs : strategy =
  fun () env avoid t ty cstr evars ->
    let hypinfo =
      decompose_applied_relation env (goalevars evars) None c
    in
    let _, res = apply_rule l2r flags by loccs (hypinfo, 0) env avoid t ty cstr evars in
    (), res

let make_leibniz_proof c ty r =
  let prf =
    match r.rew_prf with
    | RewPrf (rel, prf) ->
	let rel = mkApp (Lazy.force coq_eq, [| ty |]) in
	let prf =
	  mkApp (Lazy.force coq_f_equal,
		[| r.rew_car; ty;
		   mkLambda (Anonymous, r.rew_car, c);
		   r.rew_from; r.rew_to; prf |])
	in RewPrf (rel, prf)
    | RewCast k -> r.rew_prf
  in
    { r with rew_car = ty;
      rew_from = subst1 r.rew_from c; rew_to = subst1 r.rew_to c; rew_prf = prf }

let reset_env env =
  let env' = Global.env_of_context (Environ.named_context_val env) in
    Environ.push_rel_context (Environ.rel_context env) env'

let fold_match ?(force=false) env sigma c =
  let (ci, p, c, brs) = destCase c in
  let cty = Retyping.get_type_of env sigma c in
  let dep, pred, exists, (sk, eff) =
    let env', ctx, body =
      let ctx, pred = decompose_lam_assum p in
      let env' = Environ.push_rel_context ctx env in
	env', ctx, pred
    in
    let sortp = Retyping.get_sort_family_of env' sigma body in
    let sortc = Retyping.get_sort_family_of env sigma cty in
    let dep = not (noccurn 1 body) in
    let pred = if dep then p else
	it_mkProd_or_LetIn (subst1 mkProp body) (List.tl ctx)
    in
    let sk =
      if sortp == InProp then
	if sortc == InProp then
	  if dep then case_dep_scheme_kind_from_prop
	  else case_scheme_kind_from_prop
	else (
	  if dep
	  then case_dep_scheme_kind_from_type_in_prop
	  else case_scheme_kind_from_type)
      else ((* sortc <> InProp by typing *)
	if dep
	then case_dep_scheme_kind_from_type
	else case_scheme_kind_from_type)
    in
    let exists = Ind_tables.check_scheme sk ci.ci_ind in
      if exists || force then
	dep, pred, exists, Ind_tables.find_scheme sk ci.ci_ind
      else raise Not_found
  in
  let app =
    let ind, args = Inductive.find_rectype env cty in
    let pars, args = List.chop ci.ci_npar args in
    let meths = List.map (fun br -> br) (Array.to_list brs) in
      applist (mkConst sk, pars @ [pred] @ meths @ args @ [c])
  in
    sk, (if exists then env else reset_env env), app, eff

let unfold_match env sigma sk app =
  match kind_of_term app with
  | App (f', args) when eq_constr f' (mkConst sk) ->
      let v = Environ.constant_value (Global.env ()) sk in
	Reductionops.whd_beta sigma (mkApp (v, args))
  | _ -> app

let is_rew_cast = function RewCast _ -> true | _ -> false

let coerce env avoid cstr res =
  let rel, prf = get_rew_prf res in
    apply_constraint env avoid res.rew_car rel prf cstr res

let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
  let rec aux state env avoid t ty cstr evars =
    let cstr' = Option.map (fun c -> (ty, Some c)) cstr in
      match kind_of_term t with
      | App (m, args) ->
	  let rewrite_args state success =
	    let state, args', evars', progress =
	      Array.fold_left
		(fun (state, acc, evars, progress) arg ->
		  if not (Option.is_empty progress) && not all then (state, None :: acc, evars, progress)
		  else
		    let state, res = s state env avoid arg (Typing.type_of env (goalevars evars) arg) None evars in
		      match res with
		      | Same -> (state, None :: acc, evars, if Option.is_empty progress then Some false else progress)
		      | Info r -> (state, Some r :: acc, r.rew_evars, Some true)
		      | Fail -> (state, None :: acc, evars, progress))
		(state, [], evars, success) args
	    in
	      state, match progress with
	      | None -> Fail
	      | Some false -> Same
	      | Some true ->
		  let args' = Array.of_list (List.rev args') in
		    if Array.exists
		      (function
			 | None -> false
			 | Some r -> not (is_rew_cast r.rew_prf)) args'
		    then
		      let evars', prf, car, rel, c1, c2 = resolve_morphism env avoid t m args args' cstr' evars' in
		      let res = { rew_car = ty; rew_from = c1;
				  rew_to = c2; rew_prf = RewPrf (rel, prf);
				  rew_evars = evars' }
		      in Info res
		    else
		      let args' = Array.map2
			(fun aorig anew ->
			   match anew with None -> aorig
			   | Some r -> r.rew_to) args args'
		      in
		      let res = { rew_car = ty; rew_from = t;
				  rew_to = mkApp (m, args'); rew_prf = RewCast DEFAULTcast;
				  rew_evars = evars' }
		      in Info res

	  in
	    if flags.on_morphisms then
	      let mty = Typing.type_of env (goalevars evars) m in
	      let evars, cstr', m, mty, argsl, args =
		let argsl = Array.to_list args in
		  match lift_cstr env evars argsl m mty None with
		  | Some (evars, cstr', m, mty, args) ->
		    evars, Some cstr', m, mty, args, Array.of_list args
		  | None -> evars, None, m, mty, argsl, args
	      in
	      let state, m' = s state env avoid m mty cstr' evars in
		match m' with
		| Fail -> rewrite_args state None (* Standard path, try rewrite on arguments *)
		| Same -> rewrite_args state (Some false)
		| Info r ->
		    (* We rewrote the function and get a proof of pointwise rel for the arguments.
		       We just apply it. *)
		    let prf = match r.rew_prf with
		      | RewPrf (rel, prf) ->
			  RewPrf (apply_pointwise rel argsl, mkApp (prf, args))
		      | x -> x
		    in
		    let res =
		      { rew_car = prod_appvect r.rew_car args;
			rew_from = mkApp(r.rew_from, args); rew_to = mkApp(r.rew_to, args);
			rew_prf = prf;
			rew_evars = r.rew_evars }
		    in
		      state, match prf with
		      | RewPrf (rel, prf) ->
			Info (apply_constraint env avoid res.rew_car rel prf cstr res)
		      | RewCast _ -> Info res
	    else rewrite_args state None

      | Prod (n, x, b) when noccurn 1 b ->
	  let b = subst1 mkProp b in
	  let tx = Typing.type_of env (goalevars evars) x and tb = Typing.type_of env (goalevars evars) b in
	  let mor, unfold = arrow_morphism tx tb x b in
	  let state, res = aux state env avoid mor ty cstr evars in
	    state, (match res with
	    | Info r -> Info { r with rew_to = unfold r.rew_to }
	    | Fail | Same -> res)

      (* 		if x' = None && flags.under_lambdas then *)
      (* 		  let lam = mkLambda (n, x, b) in *)
      (* 		  let lam', occ = aux env lam occ None in *)
      (* 		  let res =  *)
      (* 		    match lam' with *)
      (* 		    | None -> None *)
      (* 		    | Some (prf, (car, rel, c1, c2)) -> *)
      (* 			Some (resolve_morphism env sigma t *)
      (* 				 ~fnewt:unfold_all *)
      (* 				 (Lazy.force coq_all) [| x ; lam |] [| None; lam' |] *)
      (* 				 cstr evars) *)
      (* 		  in res, occ *)
      (* 		else *)

      | Prod (n, dom, codom) ->
	  let lam = mkLambda (n, dom, codom) in
	  let app, unfold =
	    if eq_constr ty mkProp then
	      mkApp (Lazy.force coq_all, [| dom; lam |]), unfold_all
	    else mkApp (Lazy.force coq_forall, [| dom; lam |]), unfold_forall
	  in
	  let state, res = aux state env avoid app ty cstr evars in
	    state, (match res with
	     | Info r -> Info { r with rew_to = unfold r.rew_to }
	     | Fail | Same -> res)

      | Lambda (n, t, b) when flags.under_lambdas ->
	  let n' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n in
	  let env' = Environ.push_rel (n', None, t) env in
	  let state, b' = s state env' avoid b (Typing.type_of env' (goalevars evars) b) (unlift_cstr env (goalevars evars) cstr) evars in
	    state, (match b' with
	    | Info r ->
		let prf = match r.rew_prf with
		  | RewPrf (rel, prf) ->
		      let rel = pointwise_or_dep_relation n' t r.rew_car rel in
		      let prf = mkLambda (n', t, prf) in
			RewPrf (rel, prf)
		  | x -> x
		in
		  Info { r with
		    rew_prf = prf;
		    rew_car = mkProd (n, t, r.rew_car);
		    rew_from = mkLambda(n, t, r.rew_from);
		    rew_to = mkLambda (n, t, r.rew_to) }
	    | Fail | Same -> b')

      | Case (ci, p, c, brs) ->
	  let cty = Typing.type_of env (goalevars evars) c in
	  let cstr' = Some (mkApp (Lazy.force coq_eq, [| cty |])) in
	  let state, c' = s state env avoid c cty cstr' evars in
	  let state, res =
	    match c' with
	    | Info r ->
		let res = make_leibniz_proof (mkCase (ci, lift 1 p, mkRel 1, Array.map (lift 1) brs)) ty r in
		  state, Info (coerce env avoid cstr res)
	    | Same | Fail ->
	      if Array.for_all (Int.equal 0) ci.ci_cstr_ndecls then
		let cstr = Some (mkApp (Lazy.force coq_eq, [| ty |])) in
		let state, found, brs' = Array.fold_left
		  (fun (state, found, acc) br ->
		   if not (Option.is_empty found) then (state, found, fun x -> lift 1 br :: acc x)
		   else
                     let state, res = s state env avoid br ty cstr evars in
		     match res with
		     | Info r -> (state, Some r, fun x -> mkRel 1 :: acc x)
		     | Fail | Same -> (state, None, fun x -> lift 1 br :: acc x))
		  (state, None, fun x -> []) brs
		in
		  state, match found with
		  | Some r ->
		    let ctxc = mkCase (ci, lift 1 p, lift 1 c, Array.of_list (List.rev (brs' c'))) in
		      Info (make_leibniz_proof ctxc ty r)
		  | None -> c'
	      else
		match try Some (fold_match env (goalevars evars) t) with Not_found -> None with
		| None -> state, c'
		| Some (cst, _, t',_) -> (* eff XXX *)
                  let state, res = aux state env avoid t' ty cstr evars in
		  state, match res with
		  | Info prf ->
		    Info { prf with
				 rew_from = t; rew_to = unfold_match env (goalevars evars) cst prf.rew_to }
		  | x' -> c'
	  in
	    state, (match res with
	     | Info r ->
	       let rel, prf = get_rew_prf r in
		 Info (apply_constraint env avoid r.rew_car rel prf cstr r)
	     | x -> x)
      | _ -> state, Fail
  in aux

let all_subterms = subterm true default_flags
let one_subterm = subterm false default_flags

(** Requires transitivity of the rewrite step, if not a reduction.
    Not tail-recursive. *)

let transitivity state env avoid (res : rewrite_result_info) (next : 'a pure_strategy) : 'a * rewrite_result_info rewrite_result =
  let state, res' = next state env avoid res.rew_to res.rew_car (get_opt_rew_rel res.rew_prf) res.rew_evars in
  state, match res' with
  | Fail -> Fail
  | Same -> Info res
  | Info res' ->
      match res.rew_prf with
      | RewCast c -> Info { res' with rew_from = res.rew_from }
      | RewPrf (rew_rel, rew_prf) ->
	  match res'.rew_prf with
	  | RewCast _ -> Info { res with rew_to = res'.rew_to }
	  | RewPrf (res'_rel, res'_prf) ->
	      let prfty = mkApp (Lazy.force transitive_type, [| res.rew_car; rew_rel |]) in
	      let evars, prf = new_cstr_evar res'.rew_evars env prfty in
	      let prf = mkApp (prf, [|res.rew_from; res'.rew_from; res'.rew_to;
				      rew_prf; res'_prf |])
	      in Info { res' with rew_from = res.rew_from;
		rew_evars = evars; rew_prf = RewPrf (res'_rel, prf) }

(** Rewriting strategies.

    Inspired by ELAN's rewriting strategies:
    http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.21.4049
*)

module Strategies =
  struct

    let fail : 'a pure_strategy =
      fun s env avoid t ty cstr evars -> (s, Fail)

    let id : 'a pure_strategy =
      fun s env avoid t ty cstr evars -> (s, Same)

    let refl : 'a pure_strategy =
      fun s env avoid t ty cstr evars ->
	let evars, rel = match cstr with
	  | None -> new_cstr_evar evars env (mk_relation ty)
	  | Some r -> evars, r
	in
	let evars, proof =
	  let mty = mkApp (Lazy.force proper_proxy_type, [| ty ; rel; t |]) in
	    new_cstr_evar evars env mty
	in
	  s, Info { rew_car = ty; rew_from = t; rew_to = t;
		       rew_prf = RewPrf (rel, proof); rew_evars = evars }

    let progress (s : 'a pure_strategy) : 'a pure_strategy =
      fun state env avoid t ty cstr evars ->
        let state, res = s state env avoid t ty cstr evars in
	state, match res with
	| Fail -> Fail
	| Same -> Fail
	| Info _ -> res

    let seq (fst : 'a pure_strategy) (snd : 'a pure_strategy) : 'a pure_strategy =
      fun state env avoid t ty cstr evars ->
        let state, res = fst state env avoid t ty cstr evars in
	match res with
	| Fail -> state, Fail
	| Same -> snd state env avoid t ty cstr evars
	| Info res -> transitivity state env avoid res snd

    let choice fst snd : 'a pure_strategy =
      fun state env avoid t ty cstr evars ->
        let state, res = fst state env avoid t ty cstr evars in
	match res with
	| Fail -> snd state env avoid t ty cstr evars
	| Same | Info _ -> state, res

    let try_ str : 'a pure_strategy = choice str id

    let fix (f : 'a pure_strategy -> 'a pure_strategy) : 'a pure_strategy =
      let rec aux state env avoid t ty cstr evars =
        f aux state env avoid t ty cstr evars
      in aux

    let any (s : 'a pure_strategy) : 'a pure_strategy =
      fix (fun any -> try_ (seq s any))

    let repeat (s : 'a pure_strategy) : 'a pure_strategy =
      seq s (any s)

    let bu (s : 'a pure_strategy) : 'a pure_strategy =
      fix (fun s' -> seq (choice (progress (all_subterms s')) s) (try_ s'))

    let td (s : 'a pure_strategy) : 'a pure_strategy =
      fix (fun s' -> seq (choice s (progress (all_subterms s'))) (try_ s'))

    let innermost (s : 'a pure_strategy) : 'a pure_strategy =
      fix (fun ins -> choice (one_subterm ins) s)

    let outermost (s : 'a pure_strategy) : 'a pure_strategy =
      fix (fun out -> choice s (one_subterm out))

    let lemmas flags cs : 'a pure_strategy =
      List.fold_left (fun tac (l,l2r,by) ->
	choice tac (apply_lemma l2r flags l by AllOccurrences))
	fail cs

    let old_hints (db : string) : 'a pure_strategy =
      let rules = Autorewrite.find_rewrites db in
	lemmas rewrite_unif_flags
	  (List.map (fun hint -> ((hint.Autorewrite.rew_lemma, NoBindings), hint.Autorewrite.rew_l2r, hint.Autorewrite.rew_tac)) rules)

    let hints (db : string) : 'a pure_strategy =
      fun state env avoid t ty cstr evars ->
      let rules = Autorewrite.find_matches db t in
      let lemma hint = ((hint.Autorewrite.rew_lemma, NoBindings), hint.Autorewrite.rew_l2r,
			hint.Autorewrite.rew_tac) in
      let lems = List.map lemma rules in
	lemmas rewrite_unif_flags lems state env avoid t ty cstr evars

    let reduce (r : Redexpr.red_expr) : 'a pure_strategy =
      fun state env avoid t ty cstr evars ->
        let rfn, ckind = Redexpr.reduction_of_red_expr env r in
	  let t' = rfn env (goalevars evars) t in
	    if eq_constr t' t then
	      state, Same
	    else
	      state, Info { rew_car = ty; rew_from = t; rew_to = t';
			   rew_prf = RewCast ckind; rew_evars = evars }

    let fold_glob c : 'a pure_strategy =
      fun state env avoid t ty cstr evars ->
(* 	let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
	let sigma, c = Pretyping.understand_tcc (goalevars evars) env c in
	let unfolded =
	  try Tacred.try_red_product env sigma c
	  with e when Errors.noncritical e ->
            error "fold: the term is not unfoldable !"
	in
	  try
	    let sigma = Unification.w_unify env sigma CONV ~flags:Unification.elim_flags unfolded t in
	    let c' = Evarutil.nf_evar sigma c in
	      state, Info { rew_car = ty; rew_from = t; rew_to = c';
			   rew_prf = RewCast DEFAULTcast;
			   rew_evars = sigma, cstrevars evars }
	  with e when Errors.noncritical e -> state, Fail


end

(** The strategy for a single rewrite, dealing with occurences. *)

let rewrite_with l2r flags c occs : strategy =
  fun () env avoid t ty cstr evars ->
    let gevars = goalevars evars in
    let hypinfo = decompose_applied_relation_expr env gevars c in
    let (is, _) = c in
    let avoid = match TacStore.get is.extra f_avoid_ids with
    | None -> avoid
    | Some l -> l @ avoid
    in
    let avoid = Id.Map.fold (fun id _ accu -> id :: accu) is.lfun avoid in
    let app = apply_rule l2r flags None occs in
    let strat = Strategies.fix (fun aux -> Strategies.choice app (subterm true default_flags aux)) in
    let _, res = strat (hypinfo, 0) env avoid t ty cstr (gevars, cstrevars evars) in
    ((), res)

let apply_strategy (s : strategy) env avoid concl cstr evars =
  let _, res =
    s () env avoid concl (Typing.type_of env (goalevars evars) concl)
      (Option.map snd cstr) evars
  in
    match res with
    | Fail -> Fail
    | Same -> Same
    | Info res ->
	Info (res.rew_prf, res.rew_evars, res.rew_car, res.rew_from, res.rew_to)

let solve_constraints env evars =
  Typeclasses.resolve_typeclasses env ~split:false ~fail:true evars

let nf_zeta =
  Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])

exception RewriteFailure of std_ppcmds

type result = (evar_map * constr option * types) rewrite_result

let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : result =
  let cstr =
    let sort = mkProp in
    let impl = Lazy.force impl in
      match is_hyp with
      | None -> (sort, inverse sort impl)
      | Some _ -> (sort, impl)
  in
  let evars = (sigma, Evar.Set.empty) in
  let eq = apply_strategy strat env avoid concl (Some cstr) evars in
    match eq with
    | Fail -> Fail
    | Same -> Same
    | Info (p, (evars, cstrs), car, oldt, newt) ->
	let evars' = solve_constraints env evars in
	let newt = Evarutil.nf_evar evars' newt in
	let evars = (* Keep only original evars (potentially instantiated) and goal evars,
		       the rest has been defined and substituted already. *)
	  Evd.fold (fun ev evi acc ->
	    if Evar.Set.mem ev cstrs then Evd.remove acc ev
	    else acc) evars' evars'
	in
        match p with
        | RewCast c -> Info (evars, None, newt)
        | RewPrf (_, p) ->
          let p = nf_zeta env evars' (Evarutil.nf_evar evars' p) in
          let term = match abs with
          | None -> p
          | Some (t, ty) ->
            let t = Evarutil.nf_evar evars' t in
            let ty = Evarutil.nf_evar evars' ty in
            mkApp (mkLambda (Name (Id.of_string "lemma"), ty, p), [| t |])
          in
          let proof = match is_hyp with
          | None -> term
          | Some id -> mkApp (term, [| mkVar id |])
          in
          Info (evars, Some proof, newt)

(** ppedrot: this is a workaround. The current implementation of rewrite leaks
    evar maps. We know that we should not produce effects in here, so we reput
    them after computing... *)
let tclEFFECT (tac : tactic) : tactic = fun gl ->
  let eff = Evd.eval_side_effects gl.sigma in
  let gls = tac gl in
  let sigma = Evd.emit_side_effects eff (Evd.drop_side_effects gls.sigma) in
  { gls with sigma; }

let cl_rewrite_clause_tac ?abs strat clause gl =
  let evartac evd = Refiner.tclEVARS evd in
  let treat res =
    match res with
    | Fail -> tclFAIL 0 (str "Nothing to rewrite")
    | Same ->
	tclFAIL 0 (str"No progress made")
    | Info (undef, p, newt) ->
	let tac =
	  match clause, p with
	  | Some id, Some p ->
	      cut_replacing id newt (Tacmach.refine p)
	  | Some id, None ->
	      change_in_hyp None newt (id, InHypTypeOnly)
	  | None, Some p ->
	      let name = next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in
		tclTHENLAST
		  (Tacmach.internal_cut_no_check false name newt)
		  (tclTHEN (Tactics.revert [name]) (Tacmach.refine p))
	  | None, None -> change_in_concl None newt
	in tclTHEN (evartac undef) tac
  in
  let tac =
    try
      let concl, is_hyp =
	match clause with
	| Some id -> pf_get_hyp_typ gl id, Some id
	| None -> pf_concl gl, None
      in
      let sigma = project gl in
      let concl = Evarutil.nf_evar sigma concl in
      let res = cl_rewrite_clause_aux ?abs strat (pf_env gl) [] sigma concl is_hyp in
	treat res
    with
    | TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
	Refiner.tclFAIL 0
	  (str"Unable to satisfy the rewriting constraints."
	   ++ fnl () ++ Himsg.explain_typeclass_error env e)
  in tclEFFECT tac gl


let bind_gl_info f =
  bind concl (fun c -> bind env (fun v -> bind defs (fun ev -> f c v ev)))

let new_refine c : Goal.subgoals Goal.sensitive =
  let refable = Goal.Refinable.make
    (fun handle -> Goal.Refinable.constr_of_open_constr handle true c)
  in Goal.bind refable Goal.refine

let assert_replacing id newt tac =
  let sens = bind_gl_info
    (fun concl env sigma ->
       let nc' =
	 Environ.fold_named_context
	   (fun _ (n, b, t as decl) nc' ->
	      if Id.equal n id then (n, b, newt) :: nc'
	      else decl :: nc')
	   env ~init:[]
       in
       let reft = Refinable.make
	 (fun h ->
	    Goal.bind (Refinable.mkEvar h
			 (Environ.reset_with_named_context (val_of_named_context nc') env) concl)
	      (fun ev ->
		 Goal.bind (Refinable.mkEvar h env newt)
		   (fun ev' ->
		      let inst =
			fold_named_context
			  (fun _ (n, b, t) inst ->
			     if Id.equal n id then ev' :: inst
			     else if Option.is_empty b then mkVar n :: inst else inst)
			  env ~init:[]
		      in
		      let (e, args) = destEvar ev in
			Goal.return
                         (mkEvar (e, Array.of_list inst)))))
       in Goal.bind reft Goal.refine)
  in Tacticals.New.tclTHEN (Proofview.tclSENSITIVE sens)
       (Proofview.tclFOCUS 2 2 tac)

let newfail n s =
  Proofview.tclZERO (Refiner.FailError (n, lazy s))

let cl_rewrite_clause_newtac ?abs strat clause =
  let treat (res, is_hyp) =
    match res with
    | Fail -> newfail 0 (str "Nothing to rewrite")
    | Same ->
	newfail 0 (str"No progress made")
    | Info res ->
	match is_hyp, res with
	| Some id, (undef, Some p, newt) ->
	    assert_replacing id newt (Proofview.tclSENSITIVE (new_refine (undef, p)))
	| Some id, (undef, None, newt) ->
	    Proofview.tclSENSITIVE (Goal.convert_hyp false (id, None, newt))
	| None, (undef, Some p, newt) ->
	    let refable = Goal.Refinable.make
	      (fun handle ->
		 Goal.bind env
		   (fun env -> Goal.bind (Refinable.mkEvar handle env newt)
		      (fun ev ->
			 Goal.Refinable.constr_of_open_constr handle true
			   (undef, mkApp (p, [| ev |])))))
	    in
	      Proofview.tclSENSITIVE (Goal.bind refable Goal.refine)
	| None, (undef, None, newt) ->
	    Proofview.tclSENSITIVE (Goal.convert_concl false newt)
  in
  let info =
    bind_gl_info
      (fun concl env sigma ->
	 let ty, is_hyp =
	   match clause with
	   | Some id -> Environ.named_type id env, Some id
	   | None -> concl, None
	 in
	   try
	     let res =
	       cl_rewrite_clause_aux ?abs strat env [] sigma ty is_hyp
	     in return (res, is_hyp)
	   with
	   | TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
	     raise (RewriteFailure (str"Unable to satisfy the rewriting constraints."
			++ fnl () ++ Himsg.explain_typeclass_error env e)))
  in Proofview.Goal.lift info (fun i -> treat i)

let newtactic_init_setoid () =
  try init_setoid (); Proofview.tclUNIT ()
  with e when Errors.noncritical e -> Proofview.tclZERO e

let tactic_init_setoid () =
  init_setoid (); tclIDTAC

let cl_rewrite_clause_new_strat ?abs strat clause =
  Tacticals.New.tclTHEN (newtactic_init_setoid ())
  (try cl_rewrite_clause_newtac ?abs strat clause
   with RewriteFailure s ->
   newfail 0 (str"setoid rewrite failed: " ++ s))

let cl_rewrite_clause_newtac' l left2right occs clause =
  Proofview.tclFOCUS 1 1
       (cl_rewrite_clause_new_strat (rewrite_with left2right rewrite_unif_flags l occs) clause)

let cl_rewrite_clause_strat strat clause =
  tclTHEN (tactic_init_setoid ())
  (fun gl ->
     (*     let gl = { gl with sigma = Typeclasses.mark_unresolvables gl.sigma } in *)
     try cl_rewrite_clause_tac strat clause gl
     with RewriteFailure e ->
       tclFAIL 0 (str"setoid rewrite failed: " ++ e) gl
     | Refiner.FailError (n, pp) ->
       tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp) gl)

let cl_rewrite_clause l left2right occs clause gl =
  cl_rewrite_clause_strat (rewrite_with left2right (general_rewrite_unif_flags ()) l occs) clause gl

let apply_glob_constr c l2r occs = fun () env avoid t ty cstr evars ->
  let evd, c = (Pretyping.understand_tcc (goalevars evars) env c) in
    apply_lemma l2r (general_rewrite_unif_flags ()) (c, NoBindings)
      None occs () env avoid t ty cstr (evd, cstrevars evars)

let interp_glob_constr_list env sigma cl =
  let understand sigma (c, _) =
    let sigma, c = Pretyping.understand_tcc sigma env c in
    (sigma, ((c, NoBindings), true, None))
  in
  List.fold_map understand sigma cl

type ('constr,'redexpr) strategy_ast =
  | StratId | StratFail | StratRefl
  | StratUnary of string * ('constr,'redexpr) strategy_ast
  | StratBinary of string * ('constr,'redexpr) strategy_ast * ('constr,'redexpr) strategy_ast
  | StratConstr of 'constr * bool
  | StratTerms of 'constr list
  | StratHints of bool * string
  | StratEval of 'redexpr
  | StratFold of 'constr

let rec map_strategy (f : 'a -> 'a2) (g : 'b -> 'b2) : ('a,'b) strategy_ast -> ('a2,'b2) strategy_ast = function
  | StratId | StratFail | StratRefl as s -> s
  | StratUnary (s, str) -> StratUnary (s, map_strategy f g str)
  | StratBinary (s, str, str') -> StratBinary (s, map_strategy f g str, map_strategy f g str')
  | StratConstr (c, b) -> StratConstr (f c, b)
  | StratTerms l -> StratTerms (List.map f l)
  | StratHints (b, id) -> StratHints (b, id)
  | StratEval r -> StratEval (g r)
  | StratFold c -> StratFold (f c)

let rec strategy_of_ast = function
  | StratId -> Strategies.id
  | StratFail -> Strategies.fail
  | StratRefl -> Strategies.refl
  | StratUnary (f, s) ->
    let s' = strategy_of_ast s in
    let f' = match f with
      | "subterms" -> all_subterms
      | "subterm" -> one_subterm
      | "innermost" -> Strategies.innermost
      | "outermost" -> Strategies.outermost
      | "bottomup" -> Strategies.bu
      | "topdown" -> Strategies.td
      | "progress" -> Strategies.progress
      | "try" -> Strategies.try_
      | "any" -> Strategies.any
      | "repeat" -> Strategies.repeat
      | _ -> anomaly ~label:"strategy_of_ast" (str"Unkwnon strategy: " ++ str f)
    in f' s'
  | StratBinary (f, s, t) ->
    let s' = strategy_of_ast s in
    let t' = strategy_of_ast t in
    let f' = match f with
      | "compose" -> Strategies.seq
      | "choice" -> Strategies.choice
      | _ -> anomaly ~label:"strategy_of_ast" (str"Unkwnon strategy: " ++ str f)
    in f' s' t'
  | StratConstr (c, b) -> apply_glob_constr (fst c) b AllOccurrences
  | StratHints (old, id) -> if old then Strategies.old_hints id else Strategies.hints id
  | StratTerms l ->
    (fun () env avoid t ty cstr (evars, cstrs) ->
     let evars, cl = interp_glob_constr_list env evars l in
       Strategies.lemmas rewrite_unif_flags cl () env avoid t ty cstr (evars, cstrs))
  | StratEval r ->
    (fun () env avoid t ty cstr evars ->
     let (sigma,r_interp) = Tacinterp.interp_redexp env (goalevars evars) r in
       Strategies.reduce r_interp () env avoid t ty cstr (sigma,cstrevars evars))
  | StratFold c -> Strategies.fold_glob (fst c)


let mkappc s l = CAppExpl (Loc.ghost,(None,(Libnames.Ident (Loc.ghost,Id.of_string s))),l)

let declare_an_instance n s args =
  ((Loc.ghost,Name n), Explicit,
  CAppExpl (Loc.ghost, (None, Qualid (Loc.ghost, qualid_of_string s)),
	   args))

let declare_instance a aeq n s = declare_an_instance n s [a;aeq]

let anew_instance global binders instance fields =
  new_instance binders instance (Some (CRecord (Loc.ghost,None,fields)))
    ~global ~generalize:false None

let declare_instance_refl global binders a aeq n lemma =
  let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
  in anew_instance global binders instance
       [(Ident (Loc.ghost,Id.of_string "reflexivity"),lemma)]

let declare_instance_sym global binders a aeq n lemma =
  let instance = declare_instance a aeq (add_suffix n "_Symmetric") "Coq.Classes.RelationClasses.Symmetric"
  in anew_instance global binders instance
       [(Ident (Loc.ghost,Id.of_string "symmetry"),lemma)]

let declare_instance_trans global binders a aeq n lemma =
  let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive"
  in anew_instance global binders instance
       [(Ident (Loc.ghost,Id.of_string "transitivity"),lemma)]

let declare_relation ?(binders=[]) a aeq n refl symm trans =
  init_setoid ();
  let global = not (Locality.make_section_locality (Locality.LocalityFixme.consume ())) in
  let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation"
  in ignore(anew_instance global binders instance []);
  match (refl,symm,trans) with
      (None, None, None) -> ()
    | (Some lemma1, None, None) ->
	ignore (declare_instance_refl global binders a aeq n lemma1)
    | (None, Some lemma2, None) ->
	ignore (declare_instance_sym global binders a aeq n lemma2)
    | (None, None, Some lemma3) ->
	ignore (declare_instance_trans global binders a aeq n lemma3)
    | (Some lemma1, Some lemma2, None) ->
	ignore (declare_instance_refl global binders a aeq n lemma1);
	ignore (declare_instance_sym global binders a aeq n lemma2)
    | (Some lemma1, None, Some lemma3) ->
	let _lemma_refl = declare_instance_refl global binders a aeq n lemma1 in
	let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in
	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder"
	in ignore(
	    anew_instance global binders instance
	      [(Ident (Loc.ghost,Id.of_string "PreOrder_Reflexive"), lemma1);
	       (Ident (Loc.ghost,Id.of_string "PreOrder_Transitive"),lemma3)])
    | (None, Some lemma2, Some lemma3) ->
	let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in
	let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in
	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER"
	in ignore(
	    anew_instance global binders instance
	      [(Ident (Loc.ghost,Id.of_string "PER_Symmetric"), lemma2);
	       (Ident (Loc.ghost,Id.of_string "PER_Transitive"),lemma3)])
     | (Some lemma1, Some lemma2, Some lemma3) ->
	let _lemma_refl = declare_instance_refl global binders a aeq n lemma1 in
	let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in
	let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in
	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
	in ignore(
	  anew_instance global binders instance
	    [(Ident (Loc.ghost,Id.of_string "Equivalence_Reflexive"), lemma1);
	     (Ident (Loc.ghost,Id.of_string "Equivalence_Symmetric"), lemma2);
	     (Ident (Loc.ghost,Id.of_string "Equivalence_Transitive"), lemma3)])

let cHole = CHole (Loc.ghost, None, None)

let proper_projection r ty =
  let ctx, inst = decompose_prod_assum ty in
  let mor, args = destApp inst in
  let instarg = mkApp (r, rel_vect 0 (List.length ctx)) in
  let app = mkApp (Lazy.force proper_proj,
		  Array.append args [| instarg |]) in
    it_mkLambda_or_LetIn app ctx

let declare_projection n instance_id r =
  let ty = Global.type_of_global r in
  let c = constr_of_global r in
  let term = proper_projection c ty in
  let env = Global.env() in
  let typ = Typing.type_of env Evd.empty term in
  let ctx, typ = decompose_prod_assum typ in
  let typ =
    let n =
      let rec aux t =
	match kind_of_term t with
	    App (f, [| a ; a' ; rel; rel' |]) when eq_constr f (Lazy.force respectful) ->
	      succ (aux rel')
	  | _ -> 0
      in
      let init =
	match kind_of_term typ with
	    App (f, args) when eq_constr f (Lazy.force respectful) ->
	      mkApp (f, fst (Array.chop (Array.length args - 2) args))
	  | _ -> typ
      in aux init
    in
    let ctx,ccl = Reductionops.splay_prod_n env Evd.empty (3 * n) typ
    in it_mkProd_or_LetIn ccl ctx
  in
  let typ = it_mkProd_or_LetIn typ ctx in
  let cst =
    { const_entry_body = Future.from_val (term,Declareops.no_seff);
      const_entry_secctx = None;
      const_entry_type = Some typ;
      const_entry_opaque = false;
      const_entry_inline_code = false;
      const_entry_feedback = None;
  } in
    ignore(Declare.declare_constant n (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition))

let build_morphism_signature m =
  let env = Global.env () in
  let m = Constrintern.interp_constr Evd.empty env m in
  let t = Typing.type_of env Evd.empty m in
  let evdref = ref (Evd.empty, Evar.Set.empty) in
  let cstrs =
    let rec aux t =
      match kind_of_term t with
	| Prod (na, a, b) ->
	    None :: aux b
	| _ -> []
    in aux t
  in
  let evars, t', sig_, cstrs = build_signature !evdref env t cstrs None in
  let _ = evdref := evars in
  let _ = List.iter
    (fun (ty, rel) ->
      Option.iter (fun rel ->
	let default = mkApp (Lazy.force default_relation, [| ty; rel |]) in
	let evars,c = new_cstr_evar !evdref env default in
	  evdref := evars)
	rel)
    cstrs
  in
  let morph =
    mkApp (Lazy.force proper_type, [| t; sig_; m |])
  in
  let evd = solve_constraints env (goalevars !evdref) in
  let m = Evarutil.nf_evar evd morph in
    Evarutil.check_evars env Evd.empty evd m; m

let default_morphism sign m =
  let env = Global.env () in
  let t = Typing.type_of env Evd.empty m in
  let evars, _, sign, cstrs =
    build_signature (Evd.empty, Evar.Set.empty) env t (fst sign) (snd sign)
  in
  let morph =
    mkApp (Lazy.force proper_type, [| t; sign; m |])
  in
  let evars, mor = resolve_one_typeclass env (fst evars) morph in
    mor, proper_projection mor morph

let add_setoid global binders a aeq t n =
  init_setoid ();
  let _lemma_refl = declare_instance_refl global binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in
  let _lemma_sym = declare_instance_sym global binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
  let _lemma_trans = declare_instance_trans global binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in
  let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
  in ignore(
    anew_instance global binders instance
      [(Ident (Loc.ghost,Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
       (Ident (Loc.ghost,Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
       (Ident (Loc.ghost,Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])])

let make_tactic name =
  let open Tacexpr in
  let loc = Loc.ghost in
  let tacpath = Libnames.qualid_of_string name in
  let tacname = Qualid (loc, tacpath) in
  TacArg (loc, TacCall (loc, tacname, []))

let add_morphism_infer glob m n =
  init_setoid ();
  let instance_id = add_suffix n "_Proper" in
  let instance = build_morphism_signature m in
    if Lib.is_modtype () then
      let cst = Declare.declare_constant ~internal:Declare.KernelSilent instance_id
				(Entries.ParameterEntry (None,instance,None), Decl_kinds.IsAssumption Decl_kinds.Logical)
      in
	add_instance (Typeclasses.new_instance (Lazy.force proper_class) None glob (ConstRef cst));
	declare_projection n instance_id (ConstRef cst)
    else
      let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
      let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
	Flags.silently
	  (fun () ->
	    Lemmas.start_proof instance_id kind instance
	      (fun _ -> function
		Globnames.ConstRef cst ->
		  add_instance (Typeclasses.new_instance (Lazy.force proper_class) None
				   glob (ConstRef cst));
		  declare_projection n instance_id (ConstRef cst)
		| _ -> assert false);
	    ignore (Pfedit.by (Tacinterp.interp tac))) ()

let add_morphism glob binders m s n =
  init_setoid ();
  let instance_id = add_suffix n "_Proper" in
  let instance =
    ((Loc.ghost,Name instance_id), Explicit,
    CAppExpl (Loc.ghost,
	     (None, Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper")),
	     [cHole; s; m]))
  in
  let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
    ignore(new_instance ~global:glob binders instance (Some (CRecord (Loc.ghost,None,[])))
	      ~generalize:false ~tac ~hook:(declare_projection n instance_id) None)

(** Bind to "rewrite" too *)

(** Taken from original setoid_replace, to emulate the old rewrite semantics where
    lemmas are first instantiated and then rewrite proceeds. *)

let check_evar_map_of_evars_defs evd =
 let metas = Evd.meta_list evd in
 let check_freemetas_is_empty rebus =
  Evd.Metaset.iter
   (fun m ->
     if Evd.meta_defined evd m then () else
      raise
	(Logic.RefinerError (Logic.UnresolvedBindings [Evd.meta_name evd m])))
 in
  List.iter
   (fun (_,binding) ->
     match binding with
        Evd.Cltyp (_,{Evd.rebus=rebus; Evd.freemetas=freemetas}) ->
         check_freemetas_is_empty rebus freemetas
      | Evd.Clval (_,({Evd.rebus=rebus1; Evd.freemetas=freemetas1},_),
                 {Evd.rebus=rebus2; Evd.freemetas=freemetas2}) ->
         check_freemetas_is_empty rebus1 freemetas1 ;
         check_freemetas_is_empty rebus2 freemetas2
   ) metas

let unification_rewrite l2r c1 c2 cl car rel but env =
  let (evd',c') =
    try
      (* ~flags:(false,true) to allow to mark occurrences that must not be
         rewritten simply by replacing them with let-defined definitions
         in the context *)
      Unification.w_unify_to_subterm
       ~flags:{ rewrite_unif_flags with Unification.resolve_evars = true } env
        cl.evd ((if l2r then c1 else c2),but)
    with
	Pretype_errors.PretypeError _ ->
	  (* ~flags:(true,true) to make Ring work (since it really
             exploits conversion) *)
	  Unification.w_unify_to_subterm
	  ~flags:{ rewrite2_unif_flags with Unification.resolve_evars = true }
	    env cl.evd ((if l2r then c1 else c2),but)
  in
  let cl' = {cl with evd = evd'} in
  let cl' = Clenvtac.clenv_pose_dependent_evars true cl' in
  let nf c = Evarutil.nf_evar cl'.evd (Clenv.clenv_nf_meta cl' c) in
  let c1 = if l2r then nf c' else nf c1
  and c2 = if l2r then nf c2 else nf c'
  and car = nf car and rel = nf rel in
  check_evar_map_of_evars_defs cl'.evd;
  let prf = nf (Clenv.clenv_value cl') and prfty = nf (Clenv.clenv_type cl') in
  let cl' = { cl' with templval = mk_freelisted prf ; templtyp = mk_freelisted prfty } in
  let abs = (prf, prfty) in
  abs, {cl=cl'; ext=Evar.Set.empty; prf=(mkRel 1); car=car; rel=rel;
     c1=c1; c2=c2; c=None; abs=true; }

let get_hyp gl evars (c,l) clause l2r =
  let env = pf_env gl in
  let hi = decompose_applied_relation env evars None (c,l) in
  let but = match clause with
    | Some id -> pf_get_hyp_typ gl id
    | None -> Evarutil.nf_evar evars (pf_concl gl)
  in
  unification_rewrite l2r hi.c1 hi.c2 hi.cl hi.car hi.rel but env

let general_rewrite_flags = { under_lambdas = false; on_morphisms = true }

let general_s_rewrite cl l2r occs (c,l) ~new_goals gl =
  let app = apply_rule l2r rewrite_unif_flags None occs in
  let recstrat aux = Strategies.choice app (subterm true general_rewrite_flags aux) in
  let substrat = Strategies.fix recstrat in
  let abs, hypinfo = get_hyp gl (project gl) (c,l) cl l2r in
  let strat () env avoid t ty cstr evars =
    let _, res = substrat (hypinfo, 0) env avoid t ty cstr evars in
    (), res
  in
    try
      (tclWEAK_PROGRESS
	(tclTHEN
           (Refiner.tclEVARS hypinfo.cl.evd)
	   (cl_rewrite_clause_tac ~abs:(Some abs) strat cl))) gl
    with RewriteFailure e ->
      let {c1=x; c2=y} = hypinfo in
	raise (Pretype_errors.PretypeError
		  (pf_env gl,project gl,
		  Pretype_errors.NoOccurrenceFound ((if l2r then x else y), cl)))

open Proofview.Notations

let general_s_rewrite_clause x =
  match x with
    | None -> general_s_rewrite None
    | Some id -> general_s_rewrite (Some id)
let general_s_rewrite_clause x y z w ~new_goals =
  newtactic_init_setoid () <*>
  Proofview.V82.tactic (general_s_rewrite_clause x y z w ~new_goals)

let _ = Hook.set Equality.general_rewrite_clause general_s_rewrite_clause

(** [setoid_]{reflexivity,symmetry,transitivity} tactics *)

let not_declared env ty rel =
  Tacticals.New.tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared " ++
		str ty ++ str" relation. Maybe you need to require the Setoid library")

let setoid_proof ty fn fallback =
  Proofview.Goal.enter begin fun gl ->
    let sigma = Proofview.Goal.sigma gl in
    let env = Proofview.Goal.env gl in
    let concl = Proofview.Goal.concl gl in
    Proofview.tclORELSE
      begin
        try
          let rel, args = decompose_app_rel env sigma concl in
          let evm = sigma in
          let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env evm rel)))) in
          fn env evm car rel
        with e -> Proofview.tclZERO e
      end
      begin function
        | e ->
            Proofview.tclORELSE
              fallback
              begin function
                | Hipattern.NoEquationFound ->
                (* spiwack: [Errors.push] here is unlikely to do what
                   it's intended to, or anything meaningful for that
                   matter. *)
                    let e = Errors.push e in
	            begin match e with
	            | Not_found ->
	                let rel, args = decompose_app_rel env sigma concl in
		        not_declared env ty rel
	            | _ -> Proofview.tclZERO e
                    end
                | e' -> Proofview.tclZERO e'
              end
      end
  end

let setoid_reflexivity =
  setoid_proof "reflexive"
    (fun env evm car rel -> Proofview.V82.tactic (apply (get_reflexive_proof env evm car rel)))
    (reflexivity_red true)

let setoid_symmetry =
  setoid_proof "symmetric"
    (fun env evm car rel -> Proofview.V82.tactic (apply (get_symmetric_proof env evm car rel)))
    (symmetry_red true)

let setoid_transitivity c =
  setoid_proof "transitive"
    (fun env evm car rel ->
      Proofview.V82.tactic begin
        let proof = get_transitive_proof env evm car rel in
        match c with
        | None -> eapply proof
        | Some c -> apply_with_bindings (proof,ImplicitBindings [ c ])
      end)
    (transitivity_red true c)

let setoid_symmetry_in id =
  Proofview.Goal.enter begin fun gl ->
  let ctype = Tacmach.New.of_old (fun gl -> pf_type_of gl (mkVar id)) gl in
  let binders,concl = decompose_prod_assum ctype in
  let (equiv, args) = decompose_app concl 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 equivalence."
  in
  let others,(c1,c2) = split_last_two args in
  let he,c1,c2 =  mkApp (equiv, Array.of_list others),c1,c2 in
  let new_hyp' =  mkApp (he, [| c2 ; c1 |]) in
  let new_hyp = it_mkProd_or_LetIn new_hyp'  binders in
    Tacticals.New.tclTHENS (Tactics.cut new_hyp)
      [ Proofview.V82.tactic (intro_replacing id);
	Tacticals.New.tclTHENLIST [ intros; setoid_symmetry; Proofview.V82.tactic (apply (mkVar id)); Tactics.assumption ] ]
  end

let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity
let _ = Hook.set Tactics.setoid_symmetry setoid_symmetry
let _ = Hook.set Tactics.setoid_symmetry_in setoid_symmetry_in
let _ = Hook.set Tactics.setoid_transitivity setoid_transitivity