Finish fix for the treatment of [inverse] in [setoid_rewrite], making a

variant of the [unify] tactic that takes a hint db as argument and does
unification modulo its [transparent_state]. Add test-file for bug #1939
and another [AdvancedTypeClasses.v] that mimicks
[AdvancedCanonicalStructure.v].


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

4 files changed, 18 insertions, 9 deletions

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index ea50107ceb..5610f7518e 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -458,3 +458,9 @@ TACTIC EXTEND autosimpl
 | [ "autosimpl" hintbases(db) ] ->
     [ autosimpl (match db with None -> ["core"] | Some x -> "core"::x) None ]
 END
+
+TACTIC EXTEND unify
+| ["unify" constr(x) constr(y) ] -> [ unify x y ]
+| ["unify" constr(x) constr(y) "with" preident(base)  ] -> [ 
+    unify ~state:(Hint_db.transparent_state (searchtable_map base)) x y ]
+END
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 62ac0d4d72..285aec91ca 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -499,10 +499,6 @@ TACTIC EXTEND dependent_pattern
 | ["dependent_pattern" constr(c) ] -> [ dependent_pattern c ]
 END
 
-TACTIC EXTEND conv
-| ["conv" constr(x) constr(y) ] -> [ conv x y ]
-END
-
 TACTIC EXTEND resolve_classes
 | ["resolve_classes" ] -> [ resolve_classes ]
 END
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7cfea18b8d..ab65c4888a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3149,7 +3149,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
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 050473bfec..01d517c163 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -358,7 +358,7 @@ val generalize      : constr list -> tactic
 val generalize_gen  : ((occurrences * constr) * name) list -> tactic
 val generalize_dep  : constr  -> tactic
 
-val conv            : constr -> constr -> tactic
+val unify           : ?state:Names.transparent_state -> constr -> constr -> tactic
 val resolve_classes : tactic
 
 val tclABSTRACT : identifier option -> tactic -> tactic