Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

1 files changed, 448 insertions, 262 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b02e84e7..5af5c0d5 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tactics.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: tactics.ml 11745 2009-01-04 18:43:08Z herbelin $ *)
 
 open Pp
 open Util
@@ -85,15 +85,6 @@ let dloc = dummy_loc
 (* General functions                    *)
 (****************************************)
 
-(*
-let get_pairs_from_bindings = 
-  let pair_from_binding = function  
-    | [(Bindings binds)] -> binds
-    | _                  -> error "not a binding list!"
-  in 
-  List.map pair_from_binding
-*)
-
 let string_of_inductive c = 
   try match kind_of_term c with
   | Ind ind_sp -> 
@@ -102,26 +93,16 @@ let string_of_inductive c =
   | _ -> raise Bound
   with Bound -> error "Bound head variable."
 
-let rec head_constr_bound t l =
-  let t = strip_outer_cast(collapse_appl t) in
-  match kind_of_term t with
-    | Prod (_,_,c2)  -> head_constr_bound c2 l 
-    | LetIn (_,_,_,c2) -> head_constr_bound c2 l 
-    | App (f,args)  -> 
-	head_constr_bound f (Array.fold_right (fun a l -> a::l) args l)
-    | Const _        -> t::l
-    | Ind _       -> t::l
-    | Construct _ -> t::l
-    | Var _          -> t::l
-    | _                -> raise Bound
+let rec head_constr_bound t =
+  let t = strip_outer_cast t in
+  let _,ccl = decompose_prod_assum t in
+  let hd,args = decompose_app ccl in
+  match kind_of_term hd with
+    | Const _ | Ind _ | Construct _ | Var _ -> (hd,args)
+    | _ -> raise Bound
 
 let head_constr c = 
-  try head_constr_bound c [] with Bound -> error "Bound head variable."
-
-(*
-let bad_tactic_args s l =
-  raise (RefinerError (BadTacticArgs (s,l)))
-*)
+  try head_constr_bound c with Bound -> error "Bound head variable."
 
 (******************************************)
 (*           Primitive tactics            *)
@@ -169,6 +150,8 @@ let internal_cut_rev_replace = internal_cut_rev_gen true
 (* Moving hypotheses *)
 let move_hyp        = Tacmach.move_hyp 
 
+let order_hyps      = Tacmach.order_hyps
+
 (* Renaming hypotheses *)
 let rename_hyp      = Tacmach.rename_hyp
 
@@ -192,25 +175,28 @@ let cofix = function
 
 type tactic_reduction = env -> evar_map -> constr -> constr
 
-(* The following two tactics apply an arbitrary
-   reduction function either to the conclusion or to a 
-   certain hypothesis *)
-
-let reduct_in_concl (redfun,sty) gl = 
-  convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) sty gl
-
-let reduct_in_hyp redfun ((_,id),where) gl =
-  let (_,c, ty) = pf_get_hyp gl id in
+let pf_reduce_decl redfun where (id,c,ty) gl =
   let redfun' = pf_reduce redfun gl in
   match c with
   | None -> 
       if where = InHypValueOnly then
 	errorlabstrm "" (pr_id id ++ str "has no value.");
-      convert_hyp_no_check (id,None,redfun' ty) gl
+      (id,None,redfun' ty)
   | Some b ->
       let b' = if where <> InHypTypeOnly then redfun' b else b in
       let ty' =	if where <> InHypValueOnly then redfun' ty else ty in
-      convert_hyp_no_check (id,Some b',ty') gl
+      (id,Some b',ty')
+
+(* The following two tactics apply an arbitrary
+   reduction function either to the conclusion or to a 
+   certain hypothesis *)
+
+let reduct_in_concl (redfun,sty) gl = 
+  convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) sty gl
+
+let reduct_in_hyp redfun ((_,id),where) gl =
+  convert_hyp_no_check
+    (pf_reduce_decl redfun where (pf_get_hyp gl id) gl) gl 
 
 let reduct_option redfun = function
   | Some id -> reduct_in_hyp (fst redfun) id 
@@ -238,8 +224,8 @@ let change_on_subterm cv_pb t = function
 let change_in_concl occl t =
   reduct_in_concl ((change_on_subterm Reduction.CUMUL t occl),DEFAULTcast)
 
-let change_in_hyp occl t   =
-  reduct_in_hyp (change_on_subterm Reduction.CONV t occl)
+let change_in_hyp occl t id  =
+  with_check (reduct_in_hyp (change_on_subterm Reduction.CONV t occl) id)
 
 let change_option occl t = function
     Some id -> change_in_hyp occl t id
@@ -276,16 +262,18 @@ let pattern_option l = reduct_option (pattern_occs l,DEFAULTcast)
 (* A function which reduces accordingly to a reduction expression,
    as the command Eval does. *)
 
-let needs_check = function
+let checking_fun = function
   (* Expansion is not necessarily well-typed: e.g. expansion of t into x is
      not well-typed in [H:(P t); x:=t |- G] because x is defined after H *)
-  | Fold _ -> true
-  | _ -> false
+  | Fold _ -> with_check
+  | Pattern _ -> with_check
+  | _ -> (fun x -> x)
 
 let reduce redexp cl goal =
-  (if needs_check redexp then with_check else (fun x -> x))
-    (redin_combinator (Redexpr.reduction_of_red_expr redexp) cl)
-    goal
+  let red = Redexpr.reduction_of_red_expr redexp in
+  match redexp with
+      (Fold _|Pattern _) -> with_check (redin_combinator red cl) goal
+    | _ -> redin_combinator red cl goal
 
 (* Unfolding occurrences of a constant *)
 
@@ -402,9 +390,26 @@ let rec get_next_hyp_position id = function
       else
 	get_next_hyp_position id right
 
+let thin_for_replacing l gl =
+  try Tacmach.thin l gl
+  with Evarutil.ClearDependencyError (id,err) -> match err with
+  | Evarutil.OccurHypInSimpleClause None ->
+      errorlabstrm ""
+      (str "Cannot change " ++ pr_id id ++ str ", it is used in conclusion.")
+  | Evarutil.OccurHypInSimpleClause (Some id') -> 
+      errorlabstrm ""
+        (str "Cannot change " ++ pr_id id ++ 
+	 strbrk ", it is used in hypothesis " ++ pr_id id' ++ str".")
+  | Evarutil.EvarTypingBreak ev ->
+      errorlabstrm ""
+        (str "Cannot change " ++ pr_id id ++ 
+	 strbrk " without breaking the typing of " ++ 
+	 Printer.pr_existential (pf_env gl) ev ++ str".")
+
 let intro_replacing id gl =
   let next_hyp = get_next_hyp_position id (pf_hyps gl) in
-  tclTHENLIST [thin [id]; introduction id; move_hyp true id next_hyp] gl
+  tclTHENLIST
+    [thin_for_replacing [id]; introduction id; move_hyp true id next_hyp] gl
 
 let intros_replacing ids gl = 
   let rec introrec = function
@@ -518,6 +523,13 @@ let bring_hyps hyps =
       let f = mkCast (Evarutil.mk_new_meta(),DEFAULTcast, newcl) in
       refine_no_check (mkApp (f, instance_from_named_context hyps)) gl)
 
+let resolve_classes gl =
+  let env = pf_env gl and evd = project gl in
+    if evd = Evd.empty then tclIDTAC gl
+    else
+      let evd' = Typeclasses.resolve_typeclasses env (Evd.create_evar_defs evd) in
+	(tclTHEN (tclEVARS (Evd.evars_of evd')) tclNORMEVAR) gl
+
 (**************************)
 (*     Cut tactics        *)
 (**************************)
@@ -535,17 +547,11 @@ let cut c gl =
 
 let cut_intro t = tclTHENFIRST (cut t) intro
 
-(* let cut_replacing id t tac = 
-  tclTHENS (cut t)
-    [tclORELSE
-	(intro_replacing id) 
-	(tclORELSE (intro_erasing id) (intro_using id));
-     tac (refine_no_check (mkVar id)) ] *)
-
 (* cut_replacing échoue si l'hypothèse à remplacer apparaît dans le
    but, ou dans une autre hypothèse *)
 let cut_replacing id t tac = 
-  tclTHENS (cut t) [ intro_replacing id; tac (refine_no_check (mkVar id)) ]
+  tclTHENLAST (internal_cut_rev_replace id t)
+    (tac (refine_no_check (mkVar id)))
 
 let cut_in_parallel l = 
   let rec prec = function
@@ -704,72 +710,88 @@ let general_case_analysis with_evars (c,lbindc as cx) =
 
 let simplest_case c = general_case_analysis false (c,NoBindings)
 
+(* Apply a tactic below the products of the conclusion of a lemma *) 
+
+let descend_in_conjunctions with_evars tac exit c gl =
+  try
+    let (mind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
+    match match_with_record (snd (decompose_prod t)) with
+    | Some _ ->
+	let n = (mis_constr_nargs mind).(0) in
+	let sort = elimination_sort_of_goal gl in
+	let elim = pf_apply make_case_gen gl mind sort in
+	tclTHENLAST
+	  (general_elim with_evars (c,NoBindings) (elim,NoBindings))
+	  (tclTHENLIST [
+	    tclDO n intro;
+	    tclLAST_NHYPS n (fun l ->
+	      tclFIRST
+		(List.map (fun id -> tclTHEN (tac (mkVar id)) (thin l)) l))])
+          gl
+    | None ->
+	raise Exit
+  with RefinerError _|UserError _|Exit -> exit ()
+
 (****************************************************)
 (*            Resolution tactics                    *)
 (****************************************************)
 
-let resolve_classes gl =
-  let env = pf_env gl and evd = project gl in
-    if evd = Evd.empty then tclIDTAC gl
-    else
-      let evd' = Typeclasses.resolve_typeclasses env (Evd.create_evar_defs evd) in
-	(tclTHEN (tclEVARS (Evd.evars_of evd')) tclNORMEVAR) gl
-
 (* Resolution with missing arguments *)
 
-let general_apply with_delta with_destruct with_evars (c,lbind) gl =
+let check_evars sigma evm gl =
+  let origsigma = gl.sigma in
+  let rest = 
+    Evd.fold (fun ev evi acc -> 
+      if not (Evd.mem origsigma ev) && not (Evd.is_defined sigma ev) 
+      then Evd.add acc ev evi else acc)
+      evm Evd.empty
+  in 
+  if rest <> Evd.empty then
+    errorlabstrm "apply" (str"Uninstantiated existential variables: " ++ 
+      fnl () ++ pr_evar_map rest)
+
+let general_apply with_delta with_destruct with_evars (c,lbind) gl0 =
   let flags = 
     if with_delta then default_unify_flags else default_no_delta_unify_flags in
   (* The actual type of the theorem. It will be matched against the
   goal. If this fails, then the head constant will be unfolded step by
   step. *)
-  let concl_nprod = nb_prod (pf_concl gl) in
+  let concl_nprod = nb_prod (pf_concl gl0) in
+  let evm, c = c in
   let rec try_main_apply c gl =
-  let thm_ty0 = nf_betaiota (pf_type_of gl c) in
-  let try_apply thm_ty nprod =
-    let n = nb_prod thm_ty - nprod in
-    if n<0 then error "Applied theorem has not enough premisses.";
-    let clause = make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in
-    Clenvtac.res_pf clause ~with_evars:with_evars ~flags:flags gl in
-  try try_apply thm_ty0 concl_nprod
-  with PretypeError _|RefinerError _|UserError _|Failure _ as exn ->
-    let rec try_red_apply thm_ty =
-      try 
-        (* Try to head-reduce the conclusion of the theorem *)
-        let red_thm = try_red_product (pf_env gl) (project gl) thm_ty in
-        try try_apply red_thm concl_nprod
-        with PretypeError _|RefinerError _|UserError _|Failure _ ->
-          try_red_apply red_thm
-      with Redelimination -> 
-        (* Last chance: if the head is a variable, apply may try
-	   second order unification *)
-	try if concl_nprod <> 0 then try_apply thm_ty 0 else raise Exit
-	with PretypeError _|RefinerError _|UserError _|Failure _|Exit ->
-	  if with_destruct then
-	   try
-	    let (mind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
-	    match match_with_conjunction (snd (decompose_prod t)) with
-	    | Some _ ->
-	      let n = (mis_constr_nargs mind).(0) in
-	      let sort = elimination_sort_of_goal gl in
-	      let elim = pf_apply make_case_gen gl mind sort in
-	      tclTHENLAST
-		(general_elim with_evars (c,NoBindings) (elim,NoBindings))
-		(tclTHENLIST [
-		  tclDO n intro;
-		  tclLAST_NHYPS n (fun l ->
-		    tclFIRST
-		      (List.map (fun id ->
-			tclTHEN (try_main_apply (mkVar id)) (thin l)) l))
-		]) gl
-	    | None ->
-		raise Exit
-	   with RefinerError _|UserError _|Exit -> raise exn 
-	  else
-	    raise exn
- in
-    try_red_apply thm_ty0 in
-  try_main_apply c gl
+    let thm_ty0 = nf_betaiota (pf_type_of gl c) in
+    let try_apply thm_ty nprod =
+      let n = nb_prod thm_ty - nprod in
+	if n<0 then error "Applied theorem has not enough premisses.";
+	let clause = make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in
+	let res = Clenvtac.res_pf clause ~with_evars:with_evars ~flags:flags gl in
+	  if not with_evars then check_evars (fst res).sigma evm gl0;
+	  res
+    in
+      try try_apply thm_ty0 concl_nprod
+      with PretypeError _|RefinerError _|UserError _|Failure _ as exn ->
+	let rec try_red_apply thm_ty =
+	  try 
+            (* Try to head-reduce the conclusion of the theorem *)
+            let red_thm = try_red_product (pf_env gl) (project gl) thm_ty in
+              try try_apply red_thm concl_nprod
+              with PretypeError _|RefinerError _|UserError _|Failure _ ->
+		try_red_apply red_thm
+	  with Redelimination -> 
+            (* Last chance: if the head is a variable, apply may try
+	       second order unification *)
+	    try if concl_nprod <> 0 then try_apply thm_ty 0 else raise Exit
+	    with PretypeError _|RefinerError _|UserError _|Failure _|Exit ->
+	      if with_destruct then
+                descend_in_conjunctions with_evars
+                  try_main_apply (fun _ -> raise exn) c gl
+	      else
+		raise exn
+	in try_red_apply thm_ty0 
+  in
+    if evm = Evd.empty then try_main_apply c gl0
+    else
+      tclTHEN (tclEVARS (Evd.merge gl0.sigma evm)) (try_main_apply c) gl0
 
 let rec apply_with_ebindings_gen b e = function
   | [] ->
@@ -783,13 +805,13 @@ let apply_with_ebindings cb = apply_with_ebindings_gen false false [cb]
 let eapply_with_ebindings cb = apply_with_ebindings_gen false true [cb]
 
 let apply_with_bindings (c,bl) =
-  apply_with_ebindings (c,inj_ebindings bl)
+  apply_with_ebindings (inj_open c,inj_ebindings bl)
 
 let eapply_with_bindings (c,bl) =
-  apply_with_ebindings_gen false true [c,inj_ebindings bl]
+  apply_with_ebindings_gen false true [inj_open c,inj_ebindings bl]
 
 let apply c =
-  apply_with_ebindings (c,NoBindings)
+  apply_with_ebindings (inj_open c,NoBindings)
 
 let apply_list = function 
   | c::l -> apply_with_bindings (c,ImplicitBindings l)
@@ -819,27 +841,43 @@ let find_matching_clause unifier clause =
     with NotExtensibleClause -> failwith "Cannot apply"
   in find clause
 
-let progress_with_clause innerclause clause =
+let progress_with_clause flags innerclause clause =
   let ordered_metas = List.rev (clenv_independent clause) in
   if ordered_metas = [] then error "Statement without assumptions.";
-  let f mv = find_matching_clause (clenv_fchain mv clause) innerclause in
+  let f mv =
+    find_matching_clause (clenv_fchain mv ~flags clause) innerclause in
   try list_try_find f ordered_metas
   with Failure _ -> error "Unable to unify."
 
-let apply_in_once gl innerclause (d,lbind) =
+let apply_in_once_main flags innerclause (d,lbind) gl =
   let thm = nf_betaiota (pf_type_of gl d) in
   let rec aux clause =
-    try progress_with_clause innerclause clause
+    try progress_with_clause flags innerclause clause
     with err ->
     try aux (clenv_push_prod clause)
-    with NotExtensibleClause -> raise err
-  in aux (make_clenv_binding gl (d,thm) lbind)
+    with NotExtensibleClause -> raise err in 
+  aux (make_clenv_binding gl (d,thm) lbind)
+
+let apply_in_once with_delta with_destruct with_evars id ((sigma,d),lbind) gl0 =
+  let flags = 
+    if with_delta then default_unify_flags else default_no_delta_unify_flags in
+  let t' = pf_get_hyp_typ gl0 id in
+  let innerclause = mk_clenv_from_n gl0 (Some 0) (mkVar id,t') in
+  let rec aux c gl =
+    try
+      let clause = apply_in_once_main flags innerclause (c,lbind) gl in
+      let res = clenv_refine_in with_evars id clause gl in
+      if not with_evars then check_evars (fst res).sigma sigma gl0;
+      res
+    with exn when with_destruct ->
+      descend_in_conjunctions true aux (fun _ -> raise exn) c gl
+  in
+    if sigma = Evd.empty then aux d gl0
+    else
+      tclTHEN (tclEVARS (Evd.merge gl0.sigma sigma)) (aux d) gl0
+
+
 
-let apply_in with_evars id lemmas gl =
-  let t' = pf_get_hyp_typ gl id in
-  let innermostclause = mk_clenv_from_n gl (Some 0) (mkVar id,t') in
-  let clause = List.fold_left (apply_in_once gl) innermostclause lemmas in
-  clenv_refine_in with_evars id clause gl
 
 (* A useful resolution tactic which, if c:A->B, transforms |- C into
    |- B -> C and |- A
@@ -1013,7 +1051,7 @@ let constructor_tac with_evars expctdnumopt i lbind gl =
     Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
   check_number_of_constructors expctdnumopt i nconstr;
   let cons = mkConstruct (ith_constructor_of_inductive mind i) in
-  let apply_tac = general_apply true false with_evars (cons,lbind) in
+  let apply_tac = general_apply true false with_evars (inj_open cons,lbind) in
   (tclTHENLIST 
      [convert_concl_no_check redcl DEFAULTcast; intros; apply_tac]) gl
 
@@ -1062,11 +1100,6 @@ let register_general_multi_rewrite f =
 let clear_last = tclLAST_HYP (fun c -> (clear [destVar c]))
 let case_last  = tclLAST_HYP simplest_case
 
-let fix_empty_case nv l =
-  (* The syntax does not distinguish between "[ ]" for one clause with no names
-     and "[ ]" for no clause at all; so we are a bit liberal here *)
-  if Array.length nv = 0 & l = [[]] then [] else l
-
 let error_unexpected_extra_pattern loc nb pat =
   let s1,s2,s3 = match pat with
   | IntroIdentifier _ -> "name", (plural nb " introduction pattern"), "no"
@@ -1089,7 +1122,7 @@ let intro_or_and_pattern loc b ll l' tac =
 	  if bracketed then error_unexpected_extra_pattern loc' nb pat;
 	  l
       | ip :: l -> ip :: adjust_names_length nb (n-1) l in
-    let ll = fix_empty_case nv ll in
+    let ll = fix_empty_or_and_pattern (Array.length nv) ll in
     check_or_and_pattern_size loc ll (Array.length nv);
     tclTHENLASTn
       (tclTHEN case_last clear_last)
@@ -1097,12 +1130,29 @@ let intro_or_and_pattern loc b ll l' tac =
 	nv (Array.of_list ll))
       gl)
 
-let clear_if_atomic l2r id gl =
-  let eq = pf_type_of gl (mkVar id) in
-  let (_,lhs,rhs) = snd (find_eq_data_decompose eq) in
-  if l2r & isVar lhs then tclTRY (clear [destVar lhs;id]) gl
-  else if not l2r & isVar rhs then tclTRY (clear [destVar rhs;id]) gl
-  else tclIDTAC gl
+let rewrite_hyp l2r id gl =
+  let rew_on l2r =
+    !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) in
+  let clear_var_and_eq c =
+    tclTRY (tclTHEN (clear [id]) (tclTRY (clear [destVar c]))) in
+  let t = pf_whd_betadeltaiota gl (pf_type_of gl (mkVar id)) in
+  (* TODO: detect setoid equality? better detect the different equalities *)
+  match match_with_equality_type t with
+  | Some (hdcncl,[_;lhs;rhs]) ->
+      if l2r & isVar lhs & not (occur_var (pf_env gl) (destVar lhs) rhs) then
+	tclTHEN (rew_on l2r allClauses) (clear_var_and_eq lhs) gl
+      else if not l2r & isVar rhs & not (occur_var (pf_env gl) (destVar rhs) lhs) then
+	tclTHEN (rew_on l2r allClauses) (clear_var_and_eq rhs) gl
+      else
+	tclTHEN (rew_on l2r onConcl) (tclTRY (clear [id])) gl
+  | Some (hdcncl,[c]) ->
+      let l2r = not l2r in (* equality of the form eq_true *)
+      if isVar c then
+	tclTHEN (rew_on l2r allClauses) (clear_var_and_eq c) gl
+      else
+	tclTHEN (rew_on l2r onConcl) (tclTRY (clear [id])) gl
+  | _ ->
+      error "Cannot find a known equation."
 
 let rec explicit_intro_names = function
 | (_, IntroIdentifier id) :: l ->
@@ -1149,11 +1199,9 @@ let rec intros_patterns b avoid thin destopt = function
       tclTHEN 
         (intro_gen loc (IntroAvoid(avoid@explicit_intro_names l)) no_move true)
         (onLastHyp (fun id ->
-	  tclTHENLIST [
-	    !forward_general_multi_rewrite l2r false (mkVar id,NoBindings) 
-	      allClauses;
-	    clear_if_atomic l2r id;
-	    intros_patterns b avoid thin destopt l ]))
+	  tclTHEN
+	    (rewrite_hyp l2r id)
+	    (intros_patterns b avoid thin destopt l)))
   | [] -> clear_wildcards thin
 
 let intros_pattern = intros_patterns false [] []
@@ -1170,23 +1218,25 @@ let intro_patterns = function
 
 let make_id s = fresh_id [] (default_id_of_sort s)
 
-let prepare_intros s (loc,ipat) gl = match ipat with
+let prepare_intros s ipat gl = match ipat with
+  | None -> make_id s gl, tclIDTAC
+  | Some (loc,ipat) -> match ipat with
   | IntroIdentifier id -> id, tclIDTAC
   | IntroAnonymous -> make_id s gl, tclIDTAC
   | IntroFresh id -> fresh_id [] id gl, tclIDTAC
   | IntroWildcard -> let id = make_id s gl in id, clear_wildcards [dloc,id]
   | IntroRewrite l2r -> 
       let id = make_id s gl in
-      id, !forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allClauses
+      id, !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) allClauses
   | IntroOrAndPattern ll -> make_id s gl, 
       intro_or_and_pattern loc true ll [] (intros_patterns true [] [] no_move)
 
 let ipat_of_name = function
-  | Anonymous -> IntroAnonymous
-  | Name id -> IntroIdentifier id
+  | Anonymous -> None
+  | Name id -> Some (dloc, IntroIdentifier id)
 
 let allow_replace c gl = function (* A rather arbitrary condition... *)
-  | _, IntroIdentifier id ->
+  | Some (_, IntroIdentifier id) ->
       fst (decompose_app (snd (decompose_lam_assum c))) = mkVar id
   | _ ->
       false
@@ -1201,15 +1251,37 @@ let assert_as first ipat c gl =
 	(if first then [tclIDTAC; tac] else [tac; tclIDTAC]) gl
   | _  -> error "Not a proposition or a type."
 
-let assert_tac first na = assert_as first (dloc,ipat_of_name na)
-let true_cut = assert_tac true 
+let assert_tac na = assert_as true (ipat_of_name na)
+
+(* apply in as *)
+
+let as_tac id ipat = match ipat with
+  | Some (loc,IntroRewrite l2r) -> 
+      !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) allClauses
+  | Some (loc,IntroOrAndPattern ll) ->
+      intro_or_and_pattern loc true ll [] (intros_patterns true [] [] no_move)
+  | Some (loc,
+      (IntroIdentifier _ | IntroAnonymous | IntroFresh _ | IntroWildcard)) ->
+      user_err_loc (loc,"", str "Disjunctive/conjunctive pattern expected")
+  | None -> tclIDTAC
+
+let general_apply_in with_delta with_destruct with_evars id lemmas ipat gl =
+  tclTHEN
+    (tclMAP (apply_in_once with_delta with_destruct with_evars id) lemmas)
+    (as_tac id ipat)
+    gl
+
+let apply_in simple with_evars = general_apply_in simple simple with_evars
 
 (**************************)
 (*   Generalize tactics   *)
 (**************************)
 
-let generalized_name c t cl = function
-  | Name id as na -> na
+let generalized_name c t ids cl = function
+  | Name id as na ->
+      if List.mem id ids then
+	errorlabstrm "" (pr_id id ++ str " is already used"); 
+      na
   | Anonymous -> 
       match kind_of_term c with
       | Var id ->
@@ -1228,7 +1300,7 @@ let generalize_goal gl i ((occs,c),na) cl =
   let dummy_prod = it_mkProd_or_LetIn mkProp decls in
   let newdecls,_ = decompose_prod_n_assum i (subst_term c dummy_prod) in
   let cl' = subst_term_occ occs c (it_mkProd_or_LetIn cl newdecls) in
-  let na = generalized_name c t cl' na in
+  let na = generalized_name c t (pf_ids_of_hyps gl) cl' na in
   mkProd (na,t,cl')
 
 let generalize_dep c gl =
@@ -1313,10 +1385,10 @@ let out_arg = function
 let occurrences_of_hyp id cls =
   let rec hyp_occ = function
       [] -> None
-    | (((b,occs),id'),hl)::_ when id=id' -> Some (b,List.map out_arg occs)
+    | (((b,occs),id'),hl)::_ when id=id' -> Some ((b,List.map out_arg occs),hl)
     | _::l -> hyp_occ l in
   match cls.onhyps with
-      None -> Some (all_occurrences)
+      None -> Some (all_occurrences,InHyp)
     | Some l -> hyp_occ l
 
 let occurrences_of_goal cls =
@@ -1383,15 +1455,15 @@ let letin_tac with_eq name c occs gl =
 (* Implementation without generalisation: abbrev will be lost in hyps in *)
 (* in the extracted proof *)
 
-let letin_abstract id c occs gl =
+let letin_abstract id c (occs,check_occs) gl =
   let env = pf_env gl in
   let compute_dependency _ (hyp,_,_ as d) depdecls =
     match occurrences_of_hyp hyp occs with
       | None -> depdecls
       | Some occ ->
           let newdecl = subst_term_occ_decl occ c d in
-          if occ = all_occurrences & d = newdecl then
-	    if not (in_every_hyp occs)
+          if occ = (all_occurrences,InHyp) & d = newdecl then
+	    if check_occs & not (in_every_hyp occs) 
 	    then raise (RefinerError (DoesNotOccurIn (c,hyp)))
 	    else depdecls
           else 
@@ -1404,14 +1476,14 @@ let letin_abstract id c occs gl =
     if depdecls = [] then no_move else MoveAfter(pi1(list_last depdecls)) in
   (depdecls,lastlhyp,ccl)
 
-let letin_tac with_eq name c occs gl =
+let letin_tac_gen with_eq name c ty occs gl =
   let id =
     let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) name in
     if name = Anonymous then fresh_id [] x gl else
       if not (mem_named_context x (pf_hyps gl)) then x else
 	error ("The variable "^(string_of_id x)^" is already declared.") in
   let (depdecls,lastlhyp,ccl)= letin_abstract id c occs gl in 
-  let t = pf_type_of gl c in
+  let t = match ty with Some t -> t | None -> pf_type_of gl c in
   let newcl,eq_tac = match with_eq with
     | Some (lr,(loc,ido)) ->
       let heq = match ido with
@@ -1434,7 +1506,10 @@ let letin_tac with_eq name c occs gl =
       intro_gen dloc (IntroMustBe id) lastlhyp true;
       eq_tac;
       tclMAP convert_hyp_no_check depdecls ] gl
-  
+
+let letin_tac with_eq name c ty occs =
+  letin_tac_gen with_eq name c ty (occs,true)
+
 (* Tactics "pose proof" (usetac=None) and "assert" (otherwise) *)
 let forward usetac ipat c gl =
   match usetac with
@@ -1444,6 +1519,9 @@ let forward usetac ipat c gl =
   | Some tac -> 
       tclTHENFIRST (assert_as true ipat c) tac gl
 
+let pose_proof na c = forward None (ipat_of_name na) c
+let assert_by na t tac = forward (Some tac) (ipat_of_name na) t
+
 (*****************************)
 (* Ad hoc unfold             *)
 (*****************************)
@@ -1523,7 +1601,7 @@ let rec first_name_buggy avoid gl (loc,pat) = match pat with
   | IntroWildcard -> no_move
   | IntroRewrite _ -> no_move
   | IntroIdentifier id -> MoveAfter id
-  | IntroAnonymous | IntroFresh _ -> assert false
+  | IntroAnonymous | IntroFresh _ -> (* buggy *) no_move
 
 let consume_pattern avoid id gl = function
   | [] -> ((dloc, IntroIdentifier (fresh_id avoid id gl)), [])
@@ -1618,14 +1696,14 @@ let atomize_param_of_ind (indref,nparams) hyp0 gl =
 	| Var id ->
 	    let x = fresh_id [] id gl in
 	    tclTHEN
-	      (letin_tac None (Name x) (mkVar id) allClauses)
+	      (letin_tac None (Name x) (mkVar id) None allClauses)
 	      (atomize_one (i-1) ((mkVar x)::avoid)) gl
 	| _ ->
 	    let id = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c)
 		       Anonymous in
 	    let x = fresh_id [] id gl in
 	    tclTHEN
-	      (letin_tac None (Name x) c allClauses)
+	      (letin_tac None (Name x) c None allClauses)
 	      (atomize_one (i-1) ((mkVar x)::avoid)) gl
     else 
       tclIDTAC gl
@@ -1712,11 +1790,11 @@ let find_atomic_param_of_ind nparams indtyp =
 
 exception Shunt of identifier move_location
 
-let cook_sign hyp0_opt indvars_init env =
-  let hyp0,indvars = 
-    match hyp0_opt with
-      | None -> List.hd (List.rev indvars_init) , indvars_init
-      | Some h -> h,indvars_init in
+let cook_sign hyp0_opt indvars env =
+  let hyp0,inhyps =
+  match hyp0_opt with
+  | None -> List.hd (List.rev indvars), []
+  | Some (hyp0,at_least_in_hyps) -> hyp0, at_least_in_hyps in
   (* First phase from L to R: get [indhyps], [decldep] and [statuslist]
      for the hypotheses before (= more ancient than) hyp0 (see above) *)
   let allindhyps = hyp0::indvars in
@@ -1739,9 +1817,9 @@ let cook_sign hyp0_opt indvars_init env =
       indhyps := hyp::!indhyps; 
       rhyp
     end else
-      if (List.exists (fun id -> occur_var_in_decl env id decl) allindhyps
-	  or List.exists (fun (id,_,_) -> occur_var_in_decl env id decl)
-        !decldeps)
+      if inhyps <> [] && List.mem hyp inhyps || inhyps = [] &&
+	(List.exists (fun id -> occur_var_in_decl env id decl) allindhyps ||
+         List.exists (fun (id,_,_) -> occur_var_in_decl env id decl) !decldeps)
       then begin
 	decldeps := decl::!decldeps;
 	if !before then 
@@ -1909,14 +1987,26 @@ let mkEq t x y =
 let mkRefl t x = 
   mkApp ((build_coq_eq_data ()).refl, [| t; x |])
 
-let mkHEq t x u y = 
+let mkHEq t x u y =
   mkApp (coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq",
 	[| t; x; u; y |])
     
-let mkHRefl t x = 
+let mkHRefl t x =
   mkApp (coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq_refl",
 	[| t; x |])
 
+(* let id = lazy (coq_constant "mkHEq" ["Init";"Datatypes"] "id") *)
+
+(* let mkHEq t x u y =  *)
+(*   let ty = new_Type () in *)
+(*   mkApp (coq_constant "mkHEq" ["Logic";"EqdepFacts"] "eq_dep", *)
+(* 	[| ty; mkApp (Lazy.force id, [|ty|]); t; x; u; y |]) *)
+    
+(* let mkHRefl t x =  *)
+(*   let ty = new_Type () in *)
+(*   mkApp (coq_constant "mkHEq" ["Logic";"EqdepFacts"] "eq_dep_intro", *)
+(* 	[| ty; mkApp (Lazy.force id, [|ty|]); t; x |]) *)
+
 let mkCoe a x p px y eq = 
   mkApp (Option.get (build_coq_eq_data ()).rect, [| a; x; p; px; y; eq |])
 
@@ -1936,40 +2026,46 @@ let ids_of_constr vars c =
   let rec aux vars c = 
     match kind_of_term c with
     | Var id -> if List.mem id vars then vars else id :: vars
+    | App (f, args) -> 
+	(match kind_of_term f with
+	| Construct (ind,_) 
+	| Ind ind ->
+            let (mib,mip) = Global.lookup_inductive ind in
+	      array_fold_left_from mib.Declarations.mind_nparams 
+		aux vars args
+	| _ -> fold_constr aux vars c)
     | _ -> fold_constr aux vars c
   in aux vars c
 
 let make_abstract_generalize gl id concl dep ctx c eqs args refls = 
   let meta = Evarutil.new_meta() in
-  let cstr =
+  let term, typ = mkVar id, pf_get_hyp_typ gl id in
+  let eqslen = List.length eqs in
+    (* Abstract by the "generalized" hypothesis equality proof if necessary. *)
+  let abshypeq = 
+    if dep then 
+      mkProd (Anonymous, mkHEq (lift 1 c) (mkRel 1) typ term, lift 1 concl)
+    else concl
+  in
     (* Abstract by equalitites *)
-    let eqs = lift_togethern 1 eqs in
-    let abseqs = it_mkProd_or_LetIn ~init:concl (List.map (fun x -> (Anonymous, None, x)) eqs) in
-      (* Abstract by the "generalized" hypothesis and its equality proof *)
-    let term, typ = mkVar id, pf_get_hyp_typ gl id in
-    let abshyp = 
-      let abshypeq = 
-	if dep then 
-	  mkProd (Anonymous, mkHEq (lift 1 c) (mkRel 1) typ term, lift 1 abseqs)
-	else abseqs
-      in
-	mkProd (Name id, c, abshypeq)
-    in
-      (* Abstract by the extension of the context *)
-    let genctyp = it_mkProd_or_LetIn ~init:abshyp ctx in
-      (* The goal will become this product. *)
-    let genc = mkCast (mkMeta meta, DEFAULTcast, genctyp) in      
-      (* Apply the old arguments giving the proper instantiation of the hyp *)
-    let instc = mkApp (genc, Array.of_list args) in
-      (* Then apply to the original instanciated hyp. *)
-    let newc = mkApp (instc, [| mkVar id |]) in
-      (* Apply the reflexivity proof for the original hyp. *)
-    let newc = if dep then mkApp (newc, [| mkHRefl typ term |]) else newc in
-      (* Finaly, apply the remaining reflexivity proofs on the index, to get a term of type gl again *)
-    let appeqs = mkApp (newc, Array.of_list refls) in
-      appeqs
-  in cstr
-    
+  let eqs = lift_togethern 1 eqs in (* lift together and past genarg *)
+  let abseqs = it_mkProd_or_LetIn ~init:(lift eqslen abshypeq) (List.map (fun x -> (Anonymous, None, x)) eqs) in
+    (* Abstract by the "generalized" hypothesis. *)
+  let genarg = mkProd (Name id, c, abseqs) in
+    (* Abstract by the extension of the context *)
+  let genctyp = it_mkProd_or_LetIn ~init:genarg ctx in
+    (* The goal will become this product. *)
+  let genc = mkCast (mkMeta meta, DEFAULTcast, genctyp) in      
+    (* Apply the old arguments giving the proper instantiation of the hyp *)
+  let instc = mkApp (genc, Array.of_list args) in
+    (* Then apply to the original instanciated hyp. *)
+  let instc = mkApp (instc, [| mkVar id |]) in
+    (* Apply the reflexivity proofs on the indices. *)
+  let appeqs = mkApp (instc, Array.of_list refls) in
+    (* Finaly, apply the reflexivity proof for the original hyp, to get a term of type gl again. *)
+  let newc = if dep then mkApp (appeqs, [| mkHRefl typ term |]) else appeqs in
+    newc
+      
 let abstract_args gl id = 
   let c = pf_get_hyp_typ gl id in
   let sigma = project gl in
@@ -1998,26 +2094,36 @@ let abstract_args gl id =
 	  let liftargty = lift (List.length ctx) argty in
 	  let convertible = Reductionops.is_conv_leq ctxenv sigma liftargty ty in
 	    match kind_of_term arg with
-	      | Var _ | Rel _ | Ind _ when convertible -> 
-		  (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, vars, env)
-	      | _ ->
-		  let name = get_id name in
-		  let decl = (Name name, None, ty) in
-		  let ctx = decl :: ctx in
-		  let c' = mkApp (lift 1 c, [|mkRel 1|]) in
-		  let args = arg :: args in
-		  let liftarg = lift (List.length ctx) arg in
-		  let eq, refl = 
-		    if convertible then
-		      mkEq (lift 1 ty) (mkRel 1) liftarg, mkRefl argty arg
-		    else
-		      mkHEq (lift 1 ty) (mkRel 1) liftargty liftarg, mkHRefl argty arg
-		  in
-		  let eqs = eq :: lift_list eqs in
-		  let refls = refl :: refls in
-		  let vars = ids_of_constr vars arg in
-		    (arity, ctx, push_rel decl ctxenv, c', args, eqs, refls, vars, env)
+	    | Var _ | Rel _ | Ind _ when convertible -> 
+		(subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, vars, env)
+	    | _ ->
+		let name = get_id name in
+		let decl = (Name name, None, ty) in
+		let ctx = decl :: ctx in
+		let c' = mkApp (lift 1 c, [|mkRel 1|]) in
+		let args = arg :: args in
+		let liftarg = lift (List.length ctx) arg in
+		let eq, refl = 
+		  if convertible then
+		    mkEq (lift 1 ty) (mkRel 1) liftarg, mkRefl argty arg
+		  else
+		    mkHEq (lift 1 ty) (mkRel 1) liftargty liftarg, mkHRefl argty arg
+		in
+		let eqs = eq :: lift_list eqs in
+		let refls = refl :: refls in
+		let vars = ids_of_constr vars arg in
+		  (arity, ctx, push_rel decl ctxenv, c', args, eqs, refls, vars, env)
 	in 
+	let f, args =
+	  match kind_of_term f with
+	  | Construct (ind,_) 
+	  | Ind ind ->
+              let (mib,mip) = Global.lookup_inductive ind in
+	      let first = mib.Declarations.mind_nparams in
+	      let pars, args = array_chop first args in
+		mkApp (f, pars), args
+	  | _ -> f, args
+	in
 	let arity, ctx, ctxenv, c', args, eqs, refls, vars, env = 
 	  Array.fold_left aux (pf_type_of gl f,[],env,f,[],[],[],[],env) args
 	in
@@ -2040,10 +2146,31 @@ let abstract_generalize id ?(generalize_vars=true) gl =
 	    else
 	      tclTHENLIST [refine newc; clear [id]; tclDO n intro]
 	  in 
-	    if generalize_vars then
-	      tclTHEN tac (tclMAP (fun id -> tclTRY (generalize_dep (mkVar id))) vars) gl
+	    if generalize_vars then tclTHEN tac 
+	      (tclFIRST [revert (List.rev vars) ;
+			 tclMAP (fun id -> tclTRY (generalize_dep (mkVar id))) vars]) gl
 	    else tac gl
-
+	      
+let dependent_pattern c gl =
+  let cty = pf_type_of gl c in
+  let deps = 
+    match kind_of_term cty with
+    | App (f, args) -> Array.to_list args
+    | _ -> []
+  in
+  let varname c = match kind_of_term c with
+    | Var id -> id
+    | _ -> id_of_string (hdchar (pf_env gl) c)
+  in
+  let mklambda ty (c, id, cty) =
+    let conclvar = subst_term_occ all_occurrences c ty in
+      mkNamedLambda id cty conclvar
+  in
+  let subst = (c, varname c, cty) :: List.map (fun c -> (c, varname c, pf_type_of gl c)) deps in
+  let concllda = List.fold_left mklambda (pf_concl gl) subst in 
+  let conclapp = applistc concllda (List.rev_map pi1 subst) in
+    convert_concl_no_check conclapp DEFAULTcast gl
+      
 let occur_rel n c = 
   let res = not (noccurn n c) in
   res
@@ -2466,7 +2593,8 @@ let induction_from_context_l isrec with_evars elim_info lid names gl =
   apply_induction_in_context isrec
     None indsign (hyp0::indvars) names induct_tac gl
 
-let induction_from_context isrec with_evars elim_info (hyp0,lbind) names gl =
+let induction_from_context isrec with_evars elim_info (hyp0,lbind) names
+  inhyps gl =
   let indsign,scheme = elim_info in
   let indref = match scheme.indref with | None -> assert false | Some x -> x in
   let tmptyp0 =	pf_get_hyp_typ gl hyp0 in
@@ -2479,12 +2607,11 @@ let induction_from_context isrec with_evars elim_info (hyp0,lbind) names gl =
     thin [hyp0]
   ] in
   apply_induction_in_context isrec
-    (Some hyp0) indsign indvars names induct_tac gl
-
+    (Some (hyp0,inhyps)) indsign indvars names induct_tac gl
 
 exception TryNewInduct of exn
 
-let induction_with_atomization_of_ind_arg isrec with_evars elim names (hyp0,lbind) gl =
+let induction_with_atomization_of_ind_arg isrec with_evars elim names (hyp0,lbind) inhyps gl =
   let (indsign,scheme as elim_info) = find_elim_signature isrec elim hyp0 gl in
   if scheme.indarg = None then (* This is not a standard induction scheme (the
 				  argument is probably a parameter) So try the
@@ -2494,7 +2621,8 @@ let induction_with_atomization_of_ind_arg isrec with_evars elim names (hyp0,lbin
     let indref = match scheme.indref with | None -> assert false | Some x -> x in
     tclTHEN
       (atomize_param_of_ind (indref,scheme.nparams) hyp0)
-      (induction_from_context isrec with_evars elim_info (hyp0,lbind) names) gl
+      (induction_from_context isrec with_evars elim_info 
+	(hyp0,lbind) names inhyps) gl
 
 (* Induction on a list of induction arguments. Analyse the elim
    scheme (which is mandatory for multiple ind args), check that all
@@ -2512,26 +2640,66 @@ let induction_without_atomization isrec with_evars elim names lid gl =
   then error "Not the right number of induction arguments."
   else induction_from_context_l isrec with_evars elim_info lid names gl
 
+let enforce_eq_name id gl = function
+  | (b,(loc,IntroAnonymous)) ->
+      (b,(loc,IntroIdentifier (fresh_id [id] (add_prefix "Heq" id) gl)))
+  | (b,(loc,IntroFresh heq_base)) ->
+      (b,(loc,IntroIdentifier (fresh_id [id] heq_base gl)))
+  | x ->
+      x
+
+let has_selected_occurrences = function
+  | None -> false
+  | Some cls ->
+      cls.concl_occs <> all_occurrences_expr ||
+	cls.onhyps <> None && List.exists (fun ((occs,_),hl) ->
+          occs <> all_occurrences_expr || hl <> InHyp) (Option.get cls.onhyps)
+
+(* assume that no occurrences are selected *)
+let clear_unselected_context id inhyps cls gl =
+  match cls with
+  | None -> tclIDTAC gl
+  | Some cls ->
+      if occur_var (pf_env gl) id (pf_concl gl) &&
+	 cls.concl_occs = no_occurrences_expr 
+      then errorlabstrm ""
+	    (str "Conclusion must be mentioned: it depends on " ++ pr_id id
+	     ++ str ".");
+      match cls.onhyps with
+      | Some hyps ->
+	  let to_erase (id',_,_ as d) =
+	    if List.mem id' inhyps then (* if selected, do not erase *) None
+	    else
+	      (* erase if not selected and dependent on id or selected hyps *)
+	      let test id = occur_var_in_decl (pf_env gl) id d in
+	      if List.exists test (id::inhyps) then Some id' else None in
+	  let ids = list_map_filter to_erase (pf_hyps gl) in
+	  thin ids gl
+      | None -> tclIDTAC gl
+
 let new_induct_gen isrec with_evars elim (eqname,names) (c,lbind) cls gl =
+  let inhyps = match cls with
+  | Some {onhyps=Some hyps} -> List.map (fun ((_,id),_) -> id) hyps
+  | _ -> [] in
   match kind_of_term c with
     | Var id when not (mem_named_context id (Global.named_context()))
-	        & lbind = NoBindings & not with_evars & cls = None
-	        & eqname = None ->
-	induction_with_atomization_of_ind_arg
-	  isrec with_evars elim names (id,lbind) gl
+	        & lbind = NoBindings & not with_evars & eqname = None 
+                & not (has_selected_occurrences cls) ->
+	tclTHEN
+          (clear_unselected_context id inhyps cls)
+	  (induction_with_atomization_of_ind_arg
+	    isrec with_evars elim names (id,lbind) inhyps) gl
     | _        ->
 	let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) 
 		  Anonymous in
 	let id = fresh_id [] x gl in
-	let with_eq = 
-	  match eqname with
-	  | Some eq -> Some (false,eq)
-	  | _ ->
-	    if cls <> None then Some (false,(dloc,IntroAnonymous)) else None in
+	(* We need the equality name now *)
+	let with_eq = Option.map (fun eq -> (false,eq)) eqname in
+	(* TODO: if ind has predicate parameters, use JMeq instead of eq *)
 	tclTHEN
-	  (letin_tac with_eq (Name id) c (Option.default allClauses cls))
+	  (letin_tac_gen with_eq (Name id) c None (Option.default allClauses cls,false))
 	  (induction_with_atomization_of_ind_arg
-	     isrec with_evars elim names (id,lbind)) gl
+	     isrec with_evars elim names (id,lbind) inhyps) gl
 
 (* Induction on a list of arguments. First make induction arguments
    atomic (using letins), then do induction. The specificity here is
@@ -2563,7 +2731,7 @@ let new_induct_gen_l isrec with_evars elim (eqname,names) lc gl =
 		let _ = newlc:=id::!newlc in
 		let _ = letids:=id::!letids in
 		tclTHEN 
-		  (letin_tac None (Name id) c allClauses)
+		  (letin_tac None (Name id) c None allClauses)
 		  (atomize_list newl') gl in
   tclTHENLIST 
     [
@@ -2763,12 +2931,15 @@ let reflexivity_red allowred gl =
   let concl = if not allowred then pf_concl gl
   else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl) 
   in 
-  match match_with_equation concl with
-    | None -> !setoid_reflexivity gl
-    | Some _ -> one_constructor 1 NoBindings gl
-
-let reflexivity gl = reflexivity_red false gl
-
+    match match_with_equality_type concl with
+    | None -> None
+    | Some _ -> Some (one_constructor 1 NoBindings)
+
+let reflexivity gl = 
+  match reflexivity_red false gl with
+  | None -> !setoid_reflexivity gl
+  | Some tac -> tac gl
+      
 let intros_reflexivity  = (tclTHEN intros reflexivity)
 
 (* Symmetry tactics *)
@@ -2788,13 +2959,15 @@ let symmetry_red allowred gl =
   let concl = if not allowred then pf_concl gl
   else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl) 
   in 
-  match match_with_equation concl with
-    | None -> !setoid_symmetry gl
-    | Some (hdcncl,args) ->
+    match match_with_equation concl with
+    | None -> None
+    | Some (hdcncl,args) -> Some (fun gl ->
         let hdcncls = string_of_inductive hdcncl in
         begin 
 	  try 
-	    (apply (pf_parse_const gl ("sym_"^hdcncls)) gl)
+            tclTHEN
+              (convert_concl_no_check concl DEFAULTcast)
+	      (apply (pf_parse_const gl ("sym_"^hdcncls))) gl
           with  _ ->
             let symc = match args with 
 	      | [t1; c1; t2; c2] -> mkApp (hdcncl, [| t2; c2; t1; c1 |])
@@ -2808,9 +2981,12 @@ let symmetry_red allowred gl =
 		  tclLAST_HYP simplest_case;
 		  one_constructor 1 NoBindings ])
 	      gl
-	end
+	end)
 
-let symmetry gl = symmetry_red false gl
+let symmetry gl = 
+  match symmetry_red false gl with
+  | None -> !setoid_symmetry gl
+  | Some tac -> tac gl
 
 let setoid_symmetry_in = ref (fun _ _ -> assert false)
 let register_setoid_symmetry_in f = setoid_symmetry_in := f
@@ -2860,8 +3036,8 @@ let transitivity_red allowred t gl =
   else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl) 
   in 
   match match_with_equation concl with
-    | None -> !setoid_transitivity t gl
-    | Some (hdcncl,args) -> 
+    | None -> None
+    | Some (hdcncl,args) -> Some (fun gl ->
         let hdcncls = string_of_inductive hdcncl in
         begin
 	  try 
@@ -2885,10 +3061,13 @@ let transitivity_red allowred t gl =
 		  [ tclDO 2 intro;
 		    tclLAST_HYP simplest_case;
 		    assumption ])) gl
-        end 
-
-let transitivity t gl = transitivity_red false t gl
+        end)
 
+let transitivity t gl =
+  match transitivity_red false t gl with
+  | None -> !setoid_transitivity t gl
+  | Some tac -> tac gl
+      
 let intros_transitivity  n  = tclTHEN intros (transitivity n)
 
 (* tactical to save as name a subproof such that the generalisation of 
@@ -2917,7 +3096,7 @@ let abstract_subproof name tac gl =
       error "\"abstract\" cannot handle existentials.";
     let lemme =
       start_proof na (Global, Proof Lemma) secsign concl (fun _ _ -> ());
-      let _,(const,kind,_) =
+      let _,(const,_,kind,_) =
 	try
 	  by (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)); 
 	  let r = cook_proof ignore in 
@@ -2968,7 +3147,14 @@ let admit_as_an_axiom gl =
               List.rev (Array.to_list (instance_from_named_context sign))))
     gl
 
-let conv x y gl =
-  try let evd = Evarconv.the_conv_x_leq (pf_env gl) x y (Evd.create_evar_defs (project gl)) in
-	tclEVARS (Evd.evars_of evd) gl
-  with _ -> tclFAIL 0 (str"Not convertible") gl
+let unify ?(state=full_transparent_state) x y gl =
+  try 
+    let flags = 
+      {default_unify_flags with 
+	modulo_delta = state;
+	modulo_conv_on_closed_terms = Some state}
+    in
+    let evd = w_unify false (pf_env gl) Reduction.CONV 
+      ~flags x y (Evd.create_evar_defs (project gl))
+    in tclEVARS (Evd.evars_of evd) gl
+  with _ -> tclFAIL 0 (str"Not unifiable") gl