New tactics [conv] to test convertibility (actually, unification) of two

terms and [head_of_constr id] to put the head of a constr in some new
hypothesis. Both are used in a new tactic to deal with partial
applications in setoid_rewrite. Also fix bug #1905 by using
[subrelation] to take care of [Morphism (R ==> R') id] constraints.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11244 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 34 insertions, 2 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 700ce5895a..5cd656e910 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -760,11 +760,11 @@ let allowK = true
 
 let refresh_hypinfo env sigma hypinfo = 
   if !hypinfo.abs = None then
-    let {l2r=l2r; c = c} = !hypinfo in
+    let {l2r=l2r; c = c;cl=cl} = !hypinfo in
       match c with 
 	| Some c ->
 	    (* Refresh the clausenv to not get the same meta twice in the goal. *)
-	    hypinfo := decompose_setoid_eqhyp env sigma c l2r;
+	    hypinfo := decompose_setoid_eqhyp cl.env (Evd.evars_of cl.evd) c l2r;
 	| _ -> ()
   else ()
 
@@ -1723,6 +1723,21 @@ TACTIC EXTEND apply_typeclasses
    ]
 END
 
+let rec head_of_constr t =
+  let t = strip_outer_cast(collapse_appl t) in
+    match kind_of_term t with
+    | Prod (_,_,c2)  -> head_of_constr c2 
+    | LetIn (_,_,_,c2) -> head_of_constr c2
+    | App (f,args)  -> head_of_constr f
+    | _      -> t
+      
+TACTIC EXTEND head_of_constr
+  [ "head_of_constr" ident(h) constr(c) ] -> [
+    let c = head_of_constr c in
+      letin_tac None (Name h) c allHyps
+  ]
+END
+
 (* TACTIC EXTEND solve_evar *)
 (*   [ "solve_evar" int_or_var(n) ] -> [ fun gl -> *)
 (*     let n = match n with ArgArg i -> pred i | _ -> assert false in *)
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 5d374215de..19ce087113 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -504,3 +504,6 @@ TACTIC EXTEND generalize_eqs
 | ["generalize_eqs" hyp(id) ] -> [ abstract_generalize id ]
 END
 
+TACTIC EXTEND conv
+| ["conv" constr(x) constr(y) ] -> [ conv x y ]
+END
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8c84b40d15..586283d5a3 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -689,6 +689,13 @@ let simplest_case c = general_case_analysis false (c,NoBindings)
 (*            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 =
@@ -2925,3 +2932,8 @@ let admit_as_an_axiom gl =
     (applist (axiom, 
               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
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 700c25f6e8..cbf27b0320 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -339,6 +339,8 @@ val generalize      : constr list -> tactic
 val generalize_gen  : ((occurrences * constr) * name) list -> tactic
 val generalize_dep  : constr  -> tactic
 
+val conv            : constr -> constr -> tactic
+
 val tclABSTRACT : identifier option -> tactic -> tactic
 
 val admit_as_an_axiom : tactic