Imported Upstream version 8.5~beta1+dfsg

1 files changed, 0 insertions, 2121 deletions

diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
deleted file mode 100644
index 41944125..00000000
--- a/tactics/rewrite.ml4
+++ /dev/null
@@ -1,2121 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i camlp4deps: "parsing/grammar.cma" i*)
-
-open Pp
-open Util
-open Names
-open Nameops
-open Namegen
-open Term
-open Termops
-open Sign
-open Reduction
-open Proof_type
-open Declarations
-open Tacticals
-open Tacmach
-open Evar_refiner
-open Tactics
-open Pattern
-open Clenv
-open Auto
-open Glob_term
-open Hiddentac
-open Typeclasses
-open Typeclasses_errors
-open Classes
-open Topconstr
-open Pfedit
-open Command
-open Libnames
-open Evd
-open Compat
-
-(** Typeclass-based generalized rewriting. *)
-
-let classes_dirpath =
-  make_dirpath (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 proper_class =
-  lazy (class_info (Nametab.global (Qualid (dummy_loc, qualid_of_string "Coq.Classes.Morphisms.Proper"))))
-
-let proper_proxy_class =
-  lazy (class_info (Nametab.global (Qualid (dummy_loc, qualid_of_string "Coq.Classes.Morphisms.ProperProxy"))))
-
-let proper_proj = lazy (mkConst (Option.get (pi3 (List.hd (Lazy.force proper_class).cl_projs))))
-
-let make_dir l = make_dirpath (List.map id_of_string (List.rev 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 (* ["Classes"; "RelationClasses"] "inverse" *)
-			   ["Program"; "Basics"] "flip")
-
-let inverse car rel = mkApp (Lazy.force coq_inverse, [| car ; car; mkProp; rel |])
-(* let inverse car rel = mkApp (Lazy.force coq_inverse, [| car ; car; new_Type (); 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 mk_relation a = mkProd (Anonymous, a, mkProd (Anonymous, a, new_Type ())) *)
-
-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)
-
-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 _ =
-  Equality.register_is_applied_rewrite_relation is_applied_rewrite_relation
-
-let split_head = function
-    hd :: tl -> hd, tl
-  | [] -> assert(false)
-
-let new_cstr_evar (goal,cstr) env t =
-  let cstr', t = Evarutil.new_evar cstr env t in
-    (goal, cstr'), t
-
-let new_goal_evar (goal,cstr) env t =
-  let goal', t = Evarutil.new_evar goal env t in
-    (goal', cstr), t
-
-let build_signature evars env m (cstrs : (types * types option) option list)
-    (finalcstr : (types * types option) option) =
-  let new_evar evars env t =
-    new_cstr_evar evars env
-      (* ~src:(dummy_loc, ImplicitArg (ConstRef (Lazy.force respectful), (n, Some na))) *) t
-  in
-  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_evar evars env' relty
-	    else new_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 obj = None then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs
-	      else error "build_signature: no constraint can apply on a dependent argument"
-      | _, obj :: _ -> anomaly "build_signature: 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
-
-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
-
-exception FoundInt of int
-
-let array_find (arr: 'a array) (pred: int -> 'a -> bool): int =
-  try
-    for i=0 to Array.length arr - 1 do if pred i (arr.(i)) then raise (FoundInt i) done;
-    raise Not_found
-  with FoundInt i -> i
-
-type hypinfo = {
-  cl : clausenv;
-  prf : constr;
-  car : constr;
-  rel : constr;
-  l2r : bool;
-  c1 : constr;
-  c2 : constr;
-  c  : (Tacinterp.interp_sign * Genarg.glob_constr_and_expr with_bindings) option;
-  abs : (constr * types) option;
-  flags : Unification.unify_flags;
-}
-
-let goalevars evars = fst evars
-let cstrevars evars = snd evars
-
-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 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 nc, c', cl = push_rel_context_to_named_context env c in *)
-(*   let env' = reset_with_named_context nc env in *)
-
-let decompose_applied_relation env sigma flags orig (c,l) left2right =
-  let c' = c in
-  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
-	Some { cl=eqclause; prf=(Clenv.clenv_value eqclause);
-	       car=ty1; rel = equiv;
-	       l2r=left2right; c1=c1; c2=c2; c=orig; abs=None;
-	       flags = flags }
-  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."
-
-open Tacinterp
-let decompose_applied_relation_expr env sigma flags (is, (c,l)) left2right =
-  let sigma, cbl = Tacinterp.interp_open_constr_with_bindings false is env sigma (c,l) in
-    decompose_applied_relation env sigma flags (Some (is, (c,l))) cbl left2right
-
-let rewrite_db = "rewrite"
-
-let conv_transparent_state = (Idpred.empty, Cpred.full)
-
-let _ = 
-  Auto.add_auto_init
-    (fun () ->
-       Auto.create_hint_db false rewrite_db conv_transparent_state true)
-
-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 = true;
-  Unification.use_pattern_unification = true;
-  Unification.use_meta_bound_pattern_unification = true;
-  Unification.frozen_evars = ExistentialSet.empty;
-  Unification.restrict_conv_on_strict_subterms = false;
-  Unification.modulo_betaiota = false;
-  Unification.modulo_eta = true;
-  Unification.allow_K_in_toplevel_higher_order_unification = true
-}
-
-let rewrite2_unif_flags =
-  {  Unification.modulo_conv_on_closed_terms = Some conv_transparent_state;
-     Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
-     Unification.modulo_delta = empty_transparent_state;
-     Unification.modulo_delta_types = conv_transparent_state;
-     Unification.modulo_delta_in_merge = None;
-     Unification.check_applied_meta_types = true;
-     Unification.resolve_evars = true;
-     Unification.use_pattern_unification = true;
-     Unification.use_meta_bound_pattern_unification = true;
-     Unification.frozen_evars = ExistentialSet.empty;
-     Unification.restrict_conv_on_strict_subterms = false;
-     Unification.modulo_betaiota = 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 = true;
-       Unification.use_pattern_unification = true;
-       Unification.use_meta_bound_pattern_unification = true;
-       Unification.frozen_evars = ExistentialSet.empty;
-       Unification.restrict_conv_on_strict_subterms = false;
-       Unification.modulo_betaiota = true;
-       Unification.modulo_eta = true;
-       Unification.allow_K_in_toplevel_higher_order_unification = true }
-
-let convertible env evd x y =
-  Reductionops.is_conv env evd x y
-
-let refresh_hypinfo env sigma hypinfo =
-  if hypinfo.abs = None then
-    let {l2r=l2r; c=c;cl=cl;flags=flags} = 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 flags c l2r;
-	| _ -> hypinfo
-  else hypinfo
-
-let unify_eqn env sigma hypinfo t =
-  if isEvar t then None
-  else try
-    let {cl=cl; prf=prf; car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=c; abs=abs} = !hypinfo in
-    let left = if l2r then c1 else c2 in
-    let env', prf, c1, c2, car, rel =
-      match abs with
-      | Some (absprf, absprfty) ->
-	  let env' = clenv_unify ~flags:rewrite_unif_flags CONV left t cl in
-	    env', prf, c1, c2, car, rel
-      | None ->
-	  let env' = clenv_unify ~flags:!hypinfo.flags CONV left t cl
-	  in
-	  let env' = Clenvtac.clenv_pose_dependent_evars true env' in
-(* 	  let env' = Clenv.clenv_pose_metas_as_evars env' (Evd.undefined_metas env'.evd) in *)
-	  let evd' = Typeclasses.resolve_typeclasses ~fail:true env'.env env'.evd in
-	  let env' = { env' with evd = evd' } in
-	  let nf c = Evarutil.nf_evar 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 (Clenv.clenv_value env') 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
-		hypinfo := refresh_hypinfo env env'.evd !hypinfo;
-	      env', 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 env'.evd car rel,
-		   [| c1 ; c2 ; prf |]),
-	    (car, rel, c2, c1))
-	with Not_found ->
-	  (prf, (car, inverse car rel, c2, c1))
-    in Some (env'.evd, res)
-  with e when Class_tactics.catchable e -> None
-
-(* let unify_eqn env sigma hypinfo t = *)
-(*   if isEvar t then None *)
-(*   else try *)
-(*     let {cl=cl; prf=prf; car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=c; abs=abs} = !hypinfo in *)
-(*     let left = if l2r then c1 else c2 in *)
-(*     let evd', prf, c1, c2, car, rel = *)
-(*       match abs with *)
-(*       | Some (absprf, absprfty) -> *)
-(* 	  let env' = clenv_unify allowK ~flags:rewrite_unif_flags CONV left t cl in *)
-(* 	    env'.evd, prf, c1, c2, car, rel *)
-(*       | None -> *)
-(* 	  let cl' = Clenv.clenv_pose_metas_as_evars cl (Evd.undefined_metas cl.evd) in *)
-(* 	  let sigma = cl'.evd in *)
-(* 	  let c1 = Clenv.clenv_nf_meta cl' c1 *)
-(* 	  and c2 = Clenv.clenv_nf_meta cl' c2 *)
-(* 	  and prf = Clenv.clenv_nf_meta cl' prf *)
-(* 	  and car = Clenv.clenv_nf_meta cl' car *)
-(* 	  and rel = Clenv.clenv_nf_meta cl' rel *)
-(* 	  in *)
-(* 	  let sigma' = *)
-(* 	    try Evarconv.the_conv_x ~ts:empty_transparent_state env t c1 sigma *)
-(* 	    with Reduction.NotConvertible _ ->  *)
-(* 	      Evarconv.the_conv_x ~ts:conv_transparent_state env t c1 sigma *)
-(* 	  in *)
-(* 	  let sigma' = Evarconv.consider_remaining_unif_problems ~ts:conv_transparent_state env sigma' in *)
-(* 	  let evd' = Typeclasses.resolve_typeclasses ~fail:true env sigma' in *)
-(* 	  let nf c = Evarutil.nf_evar evd' c in *)
-(* 	  let c1 = nf c1 and c2 = nf c2 *)
-(* 	  and car = nf car and rel = nf rel *)
-(* 	  and prf' = nf prf in *)
-(* 	    if occur_meta_or_existential prf then *)
-(* 	      hypinfo := refresh_hypinfo env evd' !hypinfo; *)
-(* 	    evd', prf', c1, c2, car, rel *)
-(*     in *)
-(*     let res = *)
-(*       if l2r then (prf, (car, rel, c1, c2)) *)
-(*       else *)
-(* 	try (mkApp (get_symmetric_proof env Evd.empty car rel, *)
-(* 		   [| c1 ; c2 ; prf |]), *)
-(* 	    (car, rel, c2, c1)) *)
-(* 	with Not_found -> *)
-(* 	  (prf, (car, inverse car rel, c2, c1)) *)
-(*     in Some (evd', res) *)
-(*   with Reduction.NotConvertible -> None *)
-(*   | 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 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]))
-    | _ -> raise (Invalid_argument "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
-      | _ -> raise (Invalid_argument "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 sigma evars (args : constr list) c ty cstr =
-  let start env car =
-    match cstr with
-    | None | Some (_, None) ->
-	Evarutil.e_new_evar evars env (mk_relation car)
-    | Some (ty, Some rel) -> rel
-  in
-  let rec aux env prod n = 
-    if n = 0 then start 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 rb = aux env b' (pred n) in
-	      mkApp (Lazy.force pointwise_relation, [| ty; b'; rb |])
-	  else
-	    let rb = aux (Environ.push_rel (na, None, ty) env) b (pred n) in
-	      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 Some (aux env ty (succ (List.length args)), 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_map (* 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 rewrite_result = rewrite_result_info option
-
-type strategy = Environ.env -> identifier list -> constr -> types ->
-  constr option -> evars -> rewrite_result option
-
-let get_rew_rel r = match r.rew_prf with
-  | RewPrf (rel, prf) -> rel
-  | RewCast c -> mkApp (Coqlib.build_coq_eq (), [| r.rew_car; r.rew_from; r.rew_to |])
-
-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
-(*   try let evd' = Evarconv.the_conv_x env rel rel' res.rew_evars in *)
-(* 	{ res with rew_evars = evd' } *)
-(*   with NotConvertible -> *)
-    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 = try (array_find args' (fun i b -> b <> None)) 
-      with Not_found -> raise (Invalid_argument "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 y <> None 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 eq_env x y = x == y
-
-let apply_rule hypinfo loccs : strategy =
-  let (nowhere_except_in,occs) = loccs in
-  let is_occ occ =
-    if nowhere_except_in then List.mem occ occs else not (List.mem occ occs) in
-  let occ = ref 0 in
-    fun env avoid t ty cstr evars ->
-      if not (eq_env !hypinfo.cl.env env) then
-	hypinfo := refresh_hypinfo env (goalevars evars) !hypinfo;
-      let unif = unify_eqn env (goalevars evars) hypinfo t in
-	if unif <> None then incr occ;
-	match unif with
-	| Some (evd', (prf, (car, rel, c1, c2))) when is_occ !occ ->
-	    begin
-	      if eq_constr t c2 then Some None
-	      else
-		let res = { rew_car = ty; rew_from = c1;
-			    rew_to = c2; rew_prf = RewPrf (rel, prf); 
-			    rew_evars = evd', cstrevars evars }
-		in Some (Some (apply_constraint env avoid car rel prf cstr res))
-	    end
-	| _ -> None
-
-let apply_lemma flags (evm,c) left2right loccs : strategy =
-  fun env avoid t ty cstr evars ->
-    let hypinfo = ref (decompose_applied_relation env (goalevars evars) flags None c left2right) in
-      apply_rule hypinfo loccs env avoid t ty cstr evars
-
-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 }
-
-open Elimschemes
-
-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 = 
-    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
-      
-let unfold_match env sigma sk app =
-  match kind_of_term app with
-  | App (f', args) when 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 : strategy) : strategy =
-  let rec aux 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 success =
-	    let args', evars', progress =
-	      Array.fold_left
-		(fun (acc, evars, progress) arg ->
-		  if progress <> None && not all then (None :: acc, evars, progress)
-		  else
-		    let res = s env avoid arg (Typing.type_of env (goalevars evars) arg) None evars in
-		      match res with
-		      | Some None -> (None :: acc, evars, if progress = None then Some false else progress)
-		      | Some (Some r) -> (Some r :: acc, r.rew_evars, Some true)
-		      | None -> (None :: acc, evars, progress))
-		([], evars, success) args
-	    in
-	      match progress with
-	      | None -> None
-	      | Some false -> Some None
-	      | 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 Some (Some 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 Some (Some res)
-
-	  in
-	    if flags.on_morphisms then
-	      let evarsref = ref (snd evars) in
-	      let mty = Typing.type_of env (goalevars evars) m in
-	      let cstr', m, mty, argsl, args = 
-		let argsl = Array.to_list args in
-		  match lift_cstr env (goalevars evars) evarsref argsl m mty None with
-		  | Some (cstr', m, mty, args) -> Some cstr', m, mty, args, Array.of_list args
-		  | None -> None, m, mty, argsl, args
-	      in
-	      let m' = s env avoid m mty cstr' (fst evars, !evarsref) in
-		match m' with
-		| None -> rewrite_args None (* Standard path, try rewrite on arguments *)
-		| Some None -> rewrite_args (Some false)
-		| Some (Some 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 
-		      match prf with
-		      | RewPrf (rel, prf) ->
-			Some (Some (apply_constraint env avoid res.rew_car rel prf cstr res))
-		      | _ -> Some (Some res)
-	    else rewrite_args 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 res = aux env avoid mor ty cstr evars in
-	    (match res with
-	    | Some (Some r) -> Some (Some { r with rew_to = unfold r.rew_to })
-	    | _ -> 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 res = aux env avoid app ty cstr evars in
-	    (match res with
-	     | Some (Some r) -> Some (Some { r with rew_to = unfold r.rew_to })
-	     | _ -> 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 b' = s env' avoid b (Typing.type_of env' (goalevars evars) b) (unlift_cstr env (goalevars evars) cstr) evars in
-	    (match b' with
-	    | Some (Some 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
-		  Some (Some { 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) })
-	    | _ -> 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 c' = s env avoid c cty cstr' evars in
-	  let res = 
-	    match c' with
-	    | Some (Some r) ->
-		let res = make_leibniz_proof (mkCase (ci, lift 1 p, mkRel 1, Array.map (lift 1) brs)) ty r in
-		  Some (Some (coerce env avoid cstr res))
-	    | x ->
-	      if array_for_all ((=) 0) ci.ci_cstr_ndecls then
-		let cstr = Some (mkApp (Lazy.force coq_eq, [| ty |])) in
-		let found, brs' = Array.fold_left 
-		  (fun (found, acc) br ->
-		   if found <> None then (found, fun x -> lift 1 br :: acc x)
-		   else
-		     match s env avoid br ty cstr evars with
-		     | Some (Some r) -> (Some r, fun x -> mkRel 1 :: acc x)
-		     | _ -> (None, fun x -> lift 1 br :: acc x))
-		  (None, fun x -> []) brs
-		in
-		  match found with
-		  | Some r ->
-		    let ctxc = mkCase (ci, lift 1 p, lift 1 c, Array.of_list (List.rev (brs' x))) in
-		      Some (Some (make_leibniz_proof ctxc ty r))
-		  | None -> x
-	      else
-		match try Some (fold_match env (goalevars evars) t) with Not_found -> None with
-		| None -> x
-		| Some (cst, _, t') ->
-		  match aux env avoid t' ty cstr evars with
-		  | Some (Some prf) -> 
-		    Some (Some { prf with
-				 rew_from = t; rew_to = unfold_match env (goalevars evars) cst prf.rew_to })
-		  | x' -> x
-	  in 
-	    (match res with
-	     | Some (Some r) ->  
-	       let rel, prf = get_rew_prf r in
-		 Some (Some (apply_constraint env avoid r.rew_car rel prf cstr r))
-	     | x -> x)
-      | _ -> None
-  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 env avoid (res : rewrite_result_info) (next : strategy) : rewrite_result option =
-  match next env avoid res.rew_to res.rew_car (get_opt_rew_rel res.rew_prf) res.rew_evars with
-  | None -> None
-  | Some None -> Some (Some res)
-  | Some (Some res') ->
-      match res.rew_prf with
-      | RewCast c -> Some (Some { res' with rew_from = res.rew_from })
-      | RewPrf (rew_rel, rew_prf) ->
-	  match res'.rew_prf with
-	  | RewCast _ -> Some (Some ({ 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 Some (Some { 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 : strategy =
-      fun env avoid t ty cstr evars -> None
-
-    let id : strategy =
-      fun env avoid t ty cstr evars -> Some None
-
-    let refl : strategy =
-      fun 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
-	  Some (Some { rew_car = ty; rew_from = t; rew_to = t;
-		       rew_prf = RewPrf (rel, proof); rew_evars = evars })
-
-    let progress (s : strategy) : strategy =
-      fun env avoid t ty cstr evars ->
-	match s env avoid t ty cstr evars with
-	| None -> None
-	| Some None -> None
-	| r -> r
-
-    let seq fst snd : strategy =
-      fun env avoid t ty cstr evars ->
-	match fst env avoid t ty cstr evars with
-	| None -> None
-	| Some None -> snd env avoid t ty cstr evars
-	| Some (Some res) -> transitivity env avoid res snd
-
-    let choice fst snd : strategy =
-      fun env avoid t ty cstr evars ->
-	match fst env avoid t ty cstr evars with
-	| None -> snd env avoid t ty cstr evars
-	| res -> res
-
-    let try_ str : strategy = choice str id
-
-    let fix (f : strategy -> strategy) : strategy =
-      let rec aux env = f (fun env -> aux env) env in aux
-
-    let any (s : strategy) : strategy =
-      fix (fun any -> try_ (seq s any))
-
-    let repeat (s : strategy) : strategy =
-      seq s (any s)
-
-    let bu (s : strategy) : strategy =
-      fix (fun s' -> seq (choice (progress (all_subterms s')) s) (try_ s'))
-
-    let td (s : strategy) : strategy =
-      fix (fun s' -> seq (choice s (progress (all_subterms s'))) (try_ s'))
-
-    let innermost (s : strategy) : strategy =
-      fix (fun ins -> choice (one_subterm ins) s)
-
-    let outermost (s : strategy) : strategy =
-      fix (fun out -> choice s (one_subterm out))
-
-    let lemmas flags cs : strategy =
-      List.fold_left (fun tac (l,l2r) ->
-	choice tac (apply_lemma flags l l2r (false,[])))
-	fail cs
-
-    let inj_open c = (Evd.empty,c)
-
-    let old_hints (db : string) : strategy =
-      let rules = Autorewrite.find_rewrites db in
-	lemmas rewrite_unif_flags
-	  (List.map (fun hint -> (inj_open (hint.Autorewrite.rew_lemma, NoBindings), hint.Autorewrite.rew_l2r)) rules)
-
-    let hints (db : string) : strategy =
-      fun env avoid t ty cstr evars ->
-      let rules = Autorewrite.find_matches db t in
-      let lemma hint = (inj_open (hint.Autorewrite.rew_lemma, NoBindings), hint.Autorewrite.rew_l2r) in
-      let lems = List.map lemma rules in
-	lemmas rewrite_unif_flags lems env avoid t ty cstr evars
-
-    let reduce (r : Redexpr.red_expr) : strategy =
-      let rfn, ckind = Redexpr.reduction_of_red_expr r in
-	fun env avoid t ty cstr evars ->
-	  let t' = rfn env (goalevars evars) t in
-	    if eq_constr t' t then
-	      Some None
-	    else
-	      Some (Some { rew_car = ty; rew_from = t; rew_to = t';
-			   rew_prf = RewCast ckind; rew_evars = evars })
-	
-    let fold c : strategy =
-      fun env avoid t ty cstr evars ->
-(* 	let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
-	let sigma, c = Constrintern.interp_open_constr (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
-	      Some (Some { rew_car = ty; rew_from = t; rew_to = c';
-			   rew_prf = RewCast DEFAULTcast; 
-			   rew_evars = sigma, cstrevars evars })
-	  with e when Errors.noncritical e -> None
-
-    let fold_glob c : strategy =
-      fun 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.Default.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
-	      Some (Some { rew_car = ty; rew_from = t; rew_to = c';
-			   rew_prf = RewCast DEFAULTcast; 
-			   rew_evars = sigma, cstrevars evars })
-	  with e when Errors.noncritical e -> None
-  
-
-end
-
-(** The strategy for a single rewrite, dealing with occurences. *)
-
-let rewrite_strat flags occs hyp =
-  let app = apply_rule hyp occs in
-  let rec aux () =
-    Strategies.choice app (subterm true flags (fun env -> aux () env))
-  in aux ()
-
-let get_hypinfo_ids {c = opt} =
-  match opt with
-  | None -> []
-  | Some (is, gc) -> List.map fst is.lfun @ is.avoid_ids
-
-let rewrite_with flags c left2right loccs : strategy =
-  fun env avoid t ty cstr evars ->
-    let gevars = goalevars evars in
-    let hypinfo = ref (decompose_applied_relation_expr env gevars flags c left2right) in
-    let avoid = get_hypinfo_ids !hypinfo @ avoid in
-      rewrite_strat default_flags loccs hypinfo env avoid t ty cstr (gevars, cstrevars evars)
-
-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
-    | None -> None
-    | Some None -> Some None
-    | Some (Some res) ->
-	Some (Some (res.rew_prf, res.rew_evars, res.rew_car, res.rew_from, res.rew_to))
-
-let merge_evars (goal,cstr) = Evd.merge goal cstr
-let solve_constraints env evars =
-  Typeclasses.resolve_typeclasses env ~split:false ~fail:true
-    (merge_evars evars)
-
-let nf_zeta =
-  Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
-
-let map_rewprf f = function
-  | RewPrf (rel, prf) -> RewPrf (f rel, f prf)
-  | RewCast c -> RewCast c
-
-type result = (evar_map * constr option * types) option option
-
-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, Evd.empty) in
-  let eq = apply_strategy strat env avoid concl (Some cstr) evars in
-    match eq with
-    | Some (Some (p, evars, car, oldt, newt)) ->
-	let evars' = solve_constraints env evars in
-	let p = map_rewprf (fun p -> nf_zeta env evars' (Evarutil.nf_evar evars' p)) p in
-	let newt = Evarutil.nf_evar evars' newt in
-	let abs = Option.map (fun (x, y) ->
-				Evarutil.nf_evar evars' x, Evarutil.nf_evar evars' y) abs in
-	let evars = (* Keep only original evars (potentially instantiated) and goal evars,
-		       the rest has been defined and substituted already. *)
-(* 	  let cstrs = cstrevars evars in *)
-	    (* cstrs is small *)
-	  let gevars = goalevars evars in
-	    Evd.fold (fun ev evi acc -> 
-			if Evd.mem gevars ev then Evd.add acc ev evi
-			else acc) evars' Evd.empty
-(* 	    Evd.fold (fun ev evi acc -> Evd.remove acc ev) cstrs evars' *)
-	in
-	let res =
-	  match is_hyp with
-	  | Some id ->
-	      (match p with
-	       | RewPrf (rel, p) ->
-		   let term =
-		     match abs with
-		     | None -> p
-		     | Some (t, ty) ->
-			 mkApp (mkLambda (Name (id_of_string "lemma"), ty, p), [| t |])
-		   in
-		     Some (evars, Some (mkApp (term, [| mkVar id |])), newt)
-	       | RewCast c ->
-		   Some (evars, None, newt))
-		
-	  | None ->
-	      (match p with
-	       | RewPrf (rel, p) ->
-		   (match abs with
-		    | None -> Some (evars, Some p, newt)
-		    | Some (t, ty) ->
-			let proof = mkApp (mkLambda (Name (id_of_string "lemma"), ty, p), [| t |]) in
-			  Some (evars, Some proof, newt))
-	       | RewCast c -> Some (evars, None, newt))
-	in Some res
-    | Some None -> Some None
-    | None -> None
-		   
-let rewrite_refine (evd,c) = 
-  Tacmach.refine c
-
-let cl_rewrite_clause_tac ?abs strat meta clause gl =
-  let evartac evd = Refiner.tclEVARS evd in
-  let treat res =
-    match res with
-    | None -> tclFAIL 0 (str "Nothing to rewrite")
-    | Some None ->
-	tclFAIL 0 (str"No progress made")
-    | Some (Some (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
-    | Loc.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
-    | TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
-	Refiner.tclFAIL_lazy 0
-	  (lazy (str"Unable to satisfy the rewriting constraints."
-		 ++ fnl () ++ Himsg.explain_typeclass_error env e))
-  in tac gl
-
-open Goal
-open Environ
-
-let bind_gl_info f =
-  bind concl (fun c -> bind env (fun v -> bind defs (fun ev -> f c v ev))) 
-
-let fail l s =
-  raise (Refiner.FailError (l, lazy s))
-
-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 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 n = id then ev' :: inst
-			     else if b = None 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 Proofview.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
-    | None -> newfail 0 (str "Nothing to rewrite")
-    | Some None ->
-	newfail 0 (str"No progress made")
-    | Some (Some 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
-	 let res = 
-	   try cl_rewrite_clause_aux ?abs strat env [] sigma ty is_hyp 
-	   with
-	   | Loc.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
-	   | TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
-	       fail 0 (str"setoid rewrite failed: unable to satisfy the rewriting constraints."
-		       ++ fnl () ++ Himsg.explain_typeclass_error env e)
-	 in return (res, is_hyp))
-  in Proofview.tclGOALBINDU info (fun i -> treat i)
-  
-let cl_rewrite_clause_new_strat ?abs strat clause =
-  init_setoid ();
-  cl_rewrite_clause_newtac ?abs strat clause
-
-let cl_rewrite_clause_newtac' l left2right occs clause =
-  Proof_global.run_tactic 
-    (Proofview.tclFOCUS 1 1 
-       (cl_rewrite_clause_new_strat (rewrite_with rewrite_unif_flags l left2right occs) clause))
-
-
-let tactic_init_setoid () = 
-  init_setoid (); tclIDTAC
-
-let cl_rewrite_clause_strat strat clause =
-  tclTHEN (tactic_init_setoid ())
-  (fun gl ->
-   let meta = Evarutil.new_meta() in
-     try cl_rewrite_clause_tac strat (mkMeta meta) clause gl
-     with
-     | 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 (general_rewrite_unif_flags ()) l left2right occs) clause gl
-
-open Pp
-open Pcoq
-open Names
-open Tacexpr
-open Tacinterp
-open Termops
-open Genarg
-open Extraargs
-
-let occurrences_of = function
-  | n::_ as nl when n < 0 -> (false,List.map abs nl)
-  | nl ->
-      if List.exists (fun n -> n < 0) nl then
-	error "Illegal negative occurrence number.";
-      (true,nl)
-
-let apply_constr_expr c l2r occs = fun env avoid t ty cstr evars ->
-  let evd, c = Constrintern.interp_open_constr (goalevars evars) env c in
-    apply_lemma (general_rewrite_unif_flags ()) (evd, (c, NoBindings)) 
-      l2r occs env avoid t ty cstr (evd, cstrevars evars)
-
-let apply_glob_constr c l2r occs = fun env avoid t ty cstr evars ->
-  let evd, c = (Pretyping.Default.understand_tcc (goalevars evars) env c) in
-    apply_lemma (general_rewrite_unif_flags ()) (evd, (c, NoBindings)) 
-      l2r occs env avoid t ty cstr (evd, cstrevars evars)
-
-let interp_constr_list env sigma =
-  List.map (fun c -> 
-	      let evd, c = Constrintern.interp_open_constr sigma env c in
-		(evd, (c, NoBindings)), true)
-
-let interp_glob_constr_list env sigma =
-  List.map (fun c -> 
-	      let evd, c = Pretyping.Default.understand_tcc sigma env c in
-		(evd, (c, NoBindings)), true)
-
-open Pcoq
-
-(* Syntax for rewriting with strategies *)
-
-type constr_expr_with_bindings = constr_expr with_bindings
-type glob_constr_with_bindings = glob_constr_and_expr with_bindings
-type glob_constr_with_bindings_sign = interp_sign * glob_constr_and_expr with_bindings
-
-let pr_glob_constr_with_bindings_sign _ _ _ (ge : glob_constr_with_bindings_sign) = Printer.pr_glob_constr (fst (fst (snd ge)))
-let pr_glob_constr_with_bindings _ _ _ (ge : glob_constr_with_bindings) = Printer.pr_glob_constr (fst (fst ge))
-let pr_constr_expr_with_bindings prc _ _ (ge : constr_expr_with_bindings) = prc (fst ge)
-let interp_glob_constr_with_bindings ist gl c = Tacmach.project gl , (ist, c)
-let glob_glob_constr_with_bindings ist l = Tacinterp.intern_constr_with_bindings ist l
-let subst_glob_constr_with_bindings s c = subst_glob_with_bindings s c
-
-
-ARGUMENT EXTEND glob_constr_with_bindings 
-    PRINTED BY pr_glob_constr_with_bindings_sign
-
-    INTERPRETED BY interp_glob_constr_with_bindings
-    GLOBALIZED BY glob_glob_constr_with_bindings
-    SUBSTITUTED BY subst_glob_constr_with_bindings
-
-    RAW_TYPED AS constr_expr_with_bindings
-    RAW_PRINTED BY pr_constr_expr_with_bindings
-
-    GLOB_TYPED AS glob_constr_with_bindings
-    GLOB_PRINTED BY pr_glob_constr_with_bindings
-   
-   [ constr_with_bindings(bl) ] -> [ bl ]
-END
-
-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
-      | _ -> anomalylabstrm "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
-      | _ -> anomalylabstrm "strategy_of_ast" (str"Unkwnon strategy: " ++ str f)
-    in f' s' t'
-  | StratConstr (c, b) -> apply_glob_constr (fst c) b all_occurrences
-  | StratHints (old, id) -> if old then Strategies.old_hints id else Strategies.hints id
-  | StratTerms l -> 
-    (fun env avoid t ty cstr evars ->
-     let l' = interp_glob_constr_list env (goalevars evars) (List.map fst l) in
-       Strategies.lemmas rewrite_unif_flags l' env avoid t ty cstr evars)
-  | 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)
-
-
-type raw_strategy = (constr_expr, Tacexpr.raw_red_expr) strategy_ast
-type glob_strategy = (glob_constr_and_expr, Tacexpr.raw_red_expr) strategy_ast
-
-let interp_strategy ist gl s = 
-  let sigma = project gl in
-    sigma, strategy_of_ast s
-let glob_strategy ist s = map_strategy (Tacinterp.intern_constr ist) (fun c -> c) s
-let subst_strategy s str = str
-
-let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>"
-let pr_raw_strategy _ _ _ (s : raw_strategy) = Pp.str "<strategy>"
-let pr_glob_strategy _ _ _ (s : glob_strategy) = Pp.str "<strategy>"
-
-ARGUMENT EXTEND rewstrategy
-    PRINTED BY pr_strategy
-
-    INTERPRETED BY interp_strategy
-    GLOBALIZED BY glob_strategy
-    SUBSTITUTED BY subst_strategy
-
-    RAW_TYPED AS raw_strategy
-    RAW_PRINTED BY pr_raw_strategy
-
-    GLOB_TYPED AS glob_strategy
-    GLOB_PRINTED BY pr_glob_strategy
-
-    [ glob(c) ] -> [ StratConstr (c, true) ]
-  | [ "<-" constr(c) ] -> [ StratConstr (c, false) ]
-  | [ "subterms" rewstrategy(h) ] -> [ StratUnary ("all_subterms", h) ]
-  | [ "subterm" rewstrategy(h) ] -> [ StratUnary ("one_subterm", h) ]
-  | [ "innermost" rewstrategy(h) ] -> [ StratUnary("innermost", h) ]
-  | [ "outermost" rewstrategy(h) ] -> [ StratUnary("outermost", h) ]
-  | [ "bottomup" rewstrategy(h) ] -> [ StratUnary("bottomup", h) ]
-  | [ "topdown" rewstrategy(h) ] -> [ StratUnary("topdown", h) ]
-  | [ "id" ] -> [ StratId ]
-  | [ "fail" ] -> [ StratFail ]
-  | [ "refl" ] -> [ StratRefl ]
-  | [ "progress" rewstrategy(h) ] -> [ StratUnary ("progress", h) ]
-  | [ "try" rewstrategy(h) ] -> [ StratUnary ("try", h) ]
-  | [ "any" rewstrategy(h) ] -> [ StratUnary ("any", h) ]
-  | [ "repeat" rewstrategy(h) ] -> [ StratUnary ("repeat", h) ]
-  | [ rewstrategy(h) ";" rewstrategy(h') ] -> [ StratBinary ("compose", h, h') ]
-  | [ "(" rewstrategy(h) ")" ] -> [ h ]
-  | [ "choice" rewstrategy(h) rewstrategy(h') ] -> [ StratBinary ("choice", h, h') ]
-  | [ "old_hints" preident(h) ] -> [ StratHints (true, h) ]
-  | [ "hints" preident(h) ] -> [ StratHints (false, h) ]
-  | [ "terms" constr_list(h) ] -> [ StratTerms h ]
-  | [ "eval" red_expr(r) ] -> [ StratEval r ]
-  | [ "fold" constr(c) ] -> [ StratFold c ]
-END
-
-(* By default the strategy for "rewrite_db" is top-down *)
-
-let db_strat db = Strategies.td (Strategies.hints db)
-let cl_rewrite_clause_db db cl = cl_rewrite_clause_strat (db_strat db) cl
-
-TACTIC EXTEND rewrite_strat
-| [ "rewrite_strat" rewstrategy(s) "in" hyp(id) ] -> [ cl_rewrite_clause_strat s (Some id) ]
-| [ "rewrite_strat" rewstrategy(s) ] -> [ cl_rewrite_clause_strat s None ]
-| [ "rewrite_db" preident(db) "in" hyp(id) ] -> [ cl_rewrite_clause_db db (Some id) ]
-| [ "rewrite_db" preident(db) ] -> [ cl_rewrite_clause_db db None ]
-END
-
-let clsubstitute o c =
-  let is_tac id = match fst (fst (snd c)) with GVar (_, id') when id' = id -> true | _ -> false in
-    Tacticals.onAllHypsAndConcl
-      (fun cl ->
-	match cl with
-	  | Some id when is_tac id -> tclIDTAC
-	  | _ -> cl_rewrite_clause c o all_occurrences cl)
-
-open Extraargs
-
-TACTIC EXTEND substitute
-| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ clsubstitute o c ]
-END
-
-
-(* Compatibility with old Setoids *)
-
-TACTIC EXTEND setoid_rewrite
-   [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) ]
-   -> [ cl_rewrite_clause c o all_occurrences None ]
- | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "in" hyp(id) ] ->
-      [ cl_rewrite_clause c o all_occurrences (Some id)]
- | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) ] ->
-      [ cl_rewrite_clause c o (occurrences_of occ) None]
- | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id)] ->
-      [ cl_rewrite_clause c o (occurrences_of occ) (Some id)]
- | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "in" hyp(id) "at" occurrences(occ)] ->
-      [ cl_rewrite_clause c o (occurrences_of occ) (Some id)]
-END
-
-let cl_rewrite_clause_newtac_tac c o occ cl gl =
-  cl_rewrite_clause_newtac' c o occ cl;
-  tclIDTAC gl
-  
-TACTIC EXTEND GenRew
-| [ "rew" orient(o) glob_constr_with_bindings(c) "in" hyp(id) "at" occurrences(occ) ] ->
-    [ cl_rewrite_clause_newtac_tac c o (occurrences_of occ) (Some id) ]
-| [ "rew" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id) ] ->
-    [ cl_rewrite_clause_newtac_tac c o (occurrences_of occ) (Some id) ]
-| [ "rew" orient(o) glob_constr_with_bindings(c) "in" hyp(id) ] ->
-    [ cl_rewrite_clause_newtac_tac c o all_occurrences (Some id) ]
-| [ "rew" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) ] ->
-    [ cl_rewrite_clause_newtac_tac c o (occurrences_of occ) None ]
-| [ "rew" orient(o) glob_constr_with_bindings(c) ] ->
-    [ cl_rewrite_clause_newtac_tac c o all_occurrences None ]
-END
-
-let mkappc s l = CAppExpl (dummy_loc,(None,(Libnames.Ident (dummy_loc,id_of_string s))),l)
-
-let declare_an_instance n s args =
-  ((dummy_loc,Name n), Explicit,
-  CAppExpl (dummy_loc, (None, Qualid (dummy_loc, 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 (dummy_loc,None,fields)))
-    ~global:(not (Vernacexpr.use_section_locality ())) ~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 (dummy_loc,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 (dummy_loc,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 (dummy_loc,id_of_string "transitivity"),lemma)]
-
-let declare_relation ?(binders=[]) a aeq n refl symm trans =
-  init_setoid ();
-  let global = not (Vernacexpr.use_section_locality ()) 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 (dummy_loc,id_of_string "PreOrder_Reflexive"), lemma1);
-	       (Ident (dummy_loc,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 (dummy_loc,id_of_string "PER_Symmetric"), lemma2);
-	       (Ident (dummy_loc,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 (dummy_loc,id_of_string "Equivalence_Reflexive"), lemma1);
-	     (Ident (dummy_loc,id_of_string "Equivalence_Symmetric"), lemma2);
-	     (Ident (dummy_loc,id_of_string "Equivalence_Transitive"), lemma3)])
-
-type 'a binders_argtype = (local_binder list, 'a) Genarg.abstract_argument_type
-
-let _, _, rawwit_binders =
- (Genarg.create_arg None "binders" :
-    Genarg.tlevel binders_argtype *
-    Genarg.glevel binders_argtype *
-    Genarg.rlevel binders_argtype)
-
-open Pcoq.Constr
-
-VERNAC COMMAND EXTEND AddRelation
-  | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
-	"symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
-      [ declare_relation a aeq n (Some lemma1) (Some lemma2) None ]
-
-  | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
-	"as" ident(n) ] ->
-      [ declare_relation a aeq n (Some lemma1) None None ]
-  | [ "Add" "Relation" constr(a) constr(aeq)  "as" ident(n) ] ->
-      [ declare_relation a aeq n None None None ]
-END
-
-VERNAC COMMAND EXTEND AddRelation2
-    [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
-      "as" ident(n) ] ->
-      [ declare_relation a aeq n None (Some lemma2) None ]
-  | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
-      [ declare_relation a aeq n None (Some lemma2) (Some lemma3) ]
-END
-
-VERNAC COMMAND EXTEND AddRelation3
-    [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
-      "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
-      [ declare_relation a aeq n (Some lemma1) None (Some lemma3) ]
-  | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
-      "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
-      "as" ident(n) ] ->
-      [ declare_relation a aeq n (Some lemma1) (Some lemma2) (Some lemma3) ]
-  | [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
-	"as" ident(n) ] ->
-      [ declare_relation a aeq n None None (Some lemma3) ]
-END
-
-VERNAC COMMAND EXTEND AddParametricRelation
-  | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
-	"reflexivity" "proved" "by" constr(lemma1)
-	"symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
-      [ declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) None ]
-  | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
-	"reflexivity" "proved" "by" constr(lemma1)
-	"as" ident(n) ] ->
-      [ declare_relation ~binders:b a aeq n (Some lemma1) None None ]
-  | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)  "as" ident(n) ] ->
-      [ declare_relation ~binders:b a aeq n None None None ]
-END
-
-VERNAC COMMAND EXTEND AddParametricRelation2
-    [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
-      "as" ident(n) ] ->
-      [ declare_relation ~binders:b a aeq n None (Some lemma2) None ]
-  | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
-      [ declare_relation ~binders:b a aeq n None (Some lemma2) (Some lemma3) ]
-END
-
-VERNAC COMMAND EXTEND AddParametricRelation3
-    [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
-      "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
-      [ declare_relation ~binders:b a aeq n (Some lemma1) None (Some lemma3) ]
-  | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
-      "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
-      "as" ident(n) ] ->
-      [ declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) ]
-  | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
-	"as" ident(n) ] ->
-      [ declare_relation ~binders:b a aeq n None None (Some lemma3) ]
-END
-
-let cHole = CHole (dummy_loc, None)
-
-open Entries
-open Libnames
-
-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 typ = Typing.type_of (Global.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 (Global.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 = term;
-      const_entry_secctx = None;
-      const_entry_type = Some typ;
-      const_entry_opaque = false }
-  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 isevars = ref (Evd.empty, Evd.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 !isevars env t cstrs None in
-  let _ = isevars := 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 !isevars env default in
-	  isevars := evars)
-	rel)
-    cstrs
-  in
-  let morph =
-    mkApp (Lazy.force proper_type, [| t; sig_; m |])
-  in
-  let evd = solve_constraints env !isevars 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,Evd.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 (merge_evars 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 (dummy_loc,id_of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
-       (Ident (dummy_loc,id_of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
-       (Ident (dummy_loc,id_of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])])
-
-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
-	Flags.silently
-	  (fun () ->
-	    Lemmas.start_proof instance_id kind instance
-	      (fun _ -> function
-		Libnames.ConstRef cst ->
-		  add_instance (Typeclasses.new_instance (Lazy.force proper_class) None
-				   glob (ConstRef cst));
-		  declare_projection n instance_id (ConstRef cst)
-		| _ -> assert false);
-	    Pfedit.by (Tacinterp.interp <:tactic< Coq.Classes.SetoidTactics.add_morphism_tactic>>)) ();
-	Flags.if_verbose (fun x -> msg (Printer.pr_open_subgoals x)) ()
-
-let add_morphism glob binders m s n =
-  init_setoid ();
-  let instance_id = add_suffix n "_Proper" in
-  let instance =
-    ((dummy_loc,Name instance_id), Explicit,
-    CAppExpl (dummy_loc,
-	     (None, Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper")),
-	     [cHole; s; m]))
-  in
-  let tac = Tacinterp.interp <:tactic<add_morphism_tactic>> in
-    ignore(new_instance ~global:glob binders instance (Some (CRecord (dummy_loc,None,[])))
-	      ~generalize:false ~tac ~hook:(declare_projection n instance_id) None)
-
-VERNAC COMMAND EXTEND AddSetoid1
-   [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
-     [ add_setoid (not (Vernacexpr.use_section_locality ())) [] a aeq t n ]
-  | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
-     [	add_setoid (not (Vernacexpr.use_section_locality ())) binders a aeq t n ]
-  | [ "Add" "Morphism" constr(m) ":" ident(n) ] ->
-      [ add_morphism_infer (not (Vernacexpr.use_section_locality ())) m n ]
-  | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] ->
-      [ add_morphism (not (Vernacexpr.use_section_locality ())) [] m s n ]
-  | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
-	"with" "signature" lconstr(s) "as" ident(n) ] ->
-      [ add_morphism (not (Vernacexpr.use_section_locality ())) binders m s n ]
-END
-
-(** 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 flags l2r c1 c2 cl car rel but gl =
-  let env = pf_env gl in
-  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 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:flags
-	    env cl.evd ((if l2r then c1 else c2),but)
-  in
-  let evd' = Typeclasses.resolve_typeclasses ~fail:false env evd' 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
-    {cl=cl'; prf=(mkRel 1); car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=None; abs=Some (prf, prfty);
-     flags = flags}
-
-let get_hyp gl evars (c,l) clause l2r =
-  let flags = rewrite2_unif_flags in
-  let hi = decompose_applied_relation (pf_env gl) evars flags None (c,l) l2r 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 flags hi.l2r hi.c1 hi.c2 hi.cl hi.car hi.rel but gl with
-	flags = rewrite_unif_flags }
-
-let general_rewrite_flags = { under_lambdas = false; on_morphisms = true }
-
-let apply_lemma gl (c,l) cl l2r occs =
-  let sigma = project gl in
-  let hypinfo = ref (get_hyp gl sigma (c,l) cl l2r) in
-  let app = apply_rule hypinfo occs in
-  let rec aux () =
-    Strategies.choice app (subterm true general_rewrite_flags (fun env -> aux () env))
-  in !hypinfo, aux ()
-
-let general_s_rewrite cl l2r occs (c,l) ~new_goals gl =
-  let meta = Evarutil.new_meta() in
-  let hypinfo, strat = apply_lemma gl (c,l) cl l2r occs in
-    tclWEAK_PROGRESS 
-      (tclTHEN
-       (Refiner.tclEVARS hypinfo.cl.evd)
-       (cl_rewrite_clause_tac ~abs:hypinfo.abs strat (mkMeta meta) cl)) gl
-
-let general_s_rewrite_clause x =
-  init_setoid ();
-  match x with
-    | None -> general_s_rewrite None
-    | Some id -> general_s_rewrite (Some id)
-
-let _ = Equality.register_general_rewrite_clause general_s_rewrite_clause
-
-(** [setoid_]{reflexivity,symmetry,transitivity} tactics *)
-
-let not_declared env ty rel =
-  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 gl ty fn fallback =
-  let env = pf_env gl in
-    try
-      let rel, args = decompose_app_rel env (project gl) (pf_concl gl) in
-      let evm = project gl in
-      let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env evm rel)))) in
-	fn env evm car rel gl
-    with e when Errors.noncritical e ->
-      try fallback gl
-      with Hipattern.NoEquationFound ->
-	  match e with
-	  | Not_found ->
-	      let rel, args = decompose_app_rel env (project gl) (pf_concl gl) in
-		not_declared env ty rel gl
-	  | _ -> raise e
-
-let setoid_reflexivity gl =
-  setoid_proof gl "reflexive"
-    (fun env evm car rel -> apply (get_reflexive_proof env evm car rel))
-    (reflexivity_red true)
-
-let setoid_symmetry gl =
-  setoid_proof gl "symmetric"
-    (fun env evm car rel -> apply (get_symmetric_proof env evm car rel))
-    (symmetry_red true)
-
-let setoid_transitivity c gl =
-  setoid_proof gl "transitive"
-    (fun env evm car rel ->
-      let proof = get_transitive_proof env evm car rel in
-      match c with
-      | None -> eapply proof
-      | Some c -> apply_with_bindings (proof,Glob_term.ImplicitBindings [ c ]))
-    (transitivity_red true c)
-
-let setoid_symmetry_in id gl =
-  let ctype = pf_type_of gl (mkVar id) 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
-    tclTHENS (Tactics.cut new_hyp)
-      [ intro_replacing id;
-	tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ] ]
-      gl
-
-let _ = Tactics.register_setoid_reflexivity setoid_reflexivity
-let _ = Tactics.register_setoid_symmetry setoid_symmetry
-let _ = Tactics.register_setoid_symmetry_in setoid_symmetry_in
-let _ = Tactics.register_setoid_transitivity setoid_transitivity
-
-TACTIC EXTEND setoid_symmetry
-   [ "setoid_symmetry" ] -> [ setoid_symmetry ]
- | [ "setoid_symmetry" "in" hyp(n) ] -> [ setoid_symmetry_in n ]
-END
-
-TACTIC EXTEND setoid_reflexivity
-[ "setoid_reflexivity" ] -> [ setoid_reflexivity ]
-END
-
-TACTIC EXTEND setoid_transitivity
-  [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity (Some t) ]
-| [ "setoid_etransitivity" ] -> [ setoid_transitivity None ]
-END
-
-let implify id gl =
-  let (_, b, ctype) = pf_get_hyp gl id in
-  let binders,concl = decompose_prod_assum ctype in
-  let ctype' =
-    match binders with
-    | (_, None, ty as hd) :: tl when noccurn 1 concl ->
-	let env = Environ.push_rel_context tl (pf_env gl) in
-	let sigma = project gl in
-	let tyhd = Typing.type_of env sigma ty
-	and tyconcl = Typing.type_of (Environ.push_rel hd env) sigma concl in
-	let app, unfold = arrow_morphism tyhd (subst1 mkProp tyconcl) ty (subst1 mkProp concl) in
-	  it_mkProd_or_LetIn app tl
-    | _ -> ctype
-  in convert_hyp_no_check (id, b, ctype') gl
-
-TACTIC EXTEND implify
-[ "implify" hyp(n) ] -> [ implify n ]
-END
-
-let rec fold_matches env sigma c =
-  map_constr_with_full_binders Environ.push_rel 
-    (fun env c ->
-      match kind_of_term c with
-      | Case _ ->
-          let cst, env, c' = fold_match ~force:true env sigma c in
-	    fold_matches env sigma c'
-      | _ -> fold_matches env sigma c)
-    env c
-
-TACTIC EXTEND fold_match
-[ "fold_match" constr(c) ] -> [ fun gl -> 
-  let _, _, c' = fold_match ~force:true (pf_env gl) (project gl) c in
-    change (Some (snd (pattern_of_constr (project gl) c))) c' onConcl gl ]
-END
-
-TACTIC EXTEND fold_matches
-| [ "fold_matches" constr(c) ] -> [ fun gl -> 
-  let c' = fold_matches (pf_env gl) (project gl) c in
-    change (Some (snd (pattern_of_constr (project gl) c))) c' onConcl gl ]
-END
-
-TACTIC EXTEND myapply
-| [ "myapply" global(id) constr_list(l) ] -> [ 
-    fun gl -> 
-      let gr = id in
-      let _, impls = List.hd (Impargs.implicits_of_global gr) in
-      let ty = Global.type_of_global gr in
-      let env = pf_env gl in
-      let evars = ref (project gl) in
-      let app =
-	let rec aux ty impls args args' =
-	  match impls, kind_of_term ty with
-	  | Some (_, _, (_, _)) :: impls, Prod (n, t, t') ->
-	      let arg = Evarutil.e_new_evar evars env t in
-		aux (subst1 arg t') impls args (arg :: args')
-	  | None :: impls, Prod (n, t, t') ->
-	      (match args with
-	       | [] ->
-		   if dependent (mkRel 1) t' then
-		     let arg = Evarutil.e_new_evar evars env t in
-		       aux (subst1 arg t') impls args (arg :: args')
-		   else
-		     let arg = Evarutil.mk_new_meta () in
-		       evars := meta_declare (destMeta arg) t !evars;
-		       aux (subst1 arg t') impls args (arg :: args')
-	       | arg :: args -> 
-		   aux (subst1 arg t') impls args (arg :: args'))
-	  | _, _ -> mkApp (constr_of_global gr, Array.of_list (List.rev args'))
-	in aux ty impls l []
-      in
-	tclTHEN (Refiner.tclEVARS !evars) (apply app) gl ]
-END