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

8 files changed, 114 insertions, 11 deletions

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index ea50107ce..5610f7518 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 62ac0d4d7..285aec91c 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 7cfea18b8..ab65c4888 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 050473bfe..01d517c16 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
diff --git a/test-suite/bugs/closed/shouldsucceed/1939.v b/test-suite/bugs/closed/shouldsucceed/1939.v
new file mode 100644
index 000000000..0399b1124
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1939.v
@@ -0,0 +1,19 @@
+Require Import Setoid.
+
+ Parameter P : nat -> Prop.
+ Parameter R : nat -> nat -> Prop.
+
+ Add Parametric Morphism : P
+   with signature R ++> impl as PM1.
+ Admitted.
+
+ Add Parametric Morphism : P
+   with signature R --> impl as PM2.
+ Admitted.
+
+ Goal forall x y, R x y -> P y -> P x.
+ Proof.
+   intros x y H1 H2.
+   rewrite H1. 
+   auto.
+ Qed.
\ No newline at end of file
diff --git a/test-suite/success/AdvancedTypeClasses.v b/test-suite/success/AdvancedTypeClasses.v
new file mode 100644
index 000000000..b4535b3ba
--- /dev/null
+++ b/test-suite/success/AdvancedTypeClasses.v
@@ -0,0 +1,75 @@
+Open Scope type_scope.
+
+Section type_reification.
+
+Inductive term :Type := 
+   Fun : term -> term -> term
+ | Prod : term -> term -> term
+ | Bool : term
+ | SET :term
+ | PROP :term
+ | TYPE :term
+ | Var : Type -> term.
+
+Fixpoint interp (t:term) := 
+  match t with 
+    Bool => bool
+  | SET => Set
+  | PROP => Prop
+  | TYPE => Type   
+  | Fun a b => interp a -> interp b
+  | Prod a b => interp a * interp b
+  | Var x => x
+end.
+
+Class interp_pair (abs : Type) :=
+ { repr : term; 
+  link: abs = interp repr }.
+
+Implicit Arguments repr [[interp_pair]].
+Implicit Arguments link [[interp_pair]].
+
+Lemma prod_interp `{interp_pair a, interp_pair b} : a * b = interp (Prod (repr a) (repr b)).
+  simpl. intros. rewrite <- link. rewrite <- (link b). reflexivity.
+Qed.
+
+Lemma fun_interp :forall `{interp_pair a, interp_pair b}, (a -> b) = interp (Fun (repr a) (repr b)).
+  simpl. intros. rewrite <- link. rewrite <- (link b). reflexivity.
+Qed.
+
+Coercion repr : interp_pair >-> term.
+
+Definition abs `{interp_pair a} : Type := a.
+Coercion abs : interp_pair >-> Sortclass.
+
+Lemma fun_interp' :forall `{ia : interp_pair, ib : interp_pair}, (ia -> ib) = interp (Fun ia ib).
+  simpl. intros a ia b ib. rewrite <- link. rewrite <- (link b). reflexivity.
+Qed.
+
+Instance ProdCan `(interp_pair a, interp_pair b) : interp_pair (a * b) :=
+  repr := Prod (repr a) (repr b) ; link := prod_interp.
+
+Instance FunCan `(interp_pair a, interp_pair b) : interp_pair (a -> b) :=
+  link := fun_interp.
+
+Instance BoolCan : interp_pair bool := repr := Bool ; link := refl_equal _.
+
+Instance VarCan : interp_pair x | 10 := repr := Var x ; link := refl_equal _.
+Instance SetCan : interp_pair Set := repr := SET ; link := refl_equal _.
+Instance PropCan : interp_pair Prop := repr := PROP ; link := refl_equal _.
+Instance TypeCan : interp_pair Type := repr := TYPE ; link := refl_equal _.
+
+(* Print Canonical Projections. *)
+
+Variable A:Type.
+
+Variable Inhabited: term -> Prop.
+
+Variable Inhabited_correct: forall `{interp_pair p}, Inhabited (repr p) -> p.
+
+Lemma L : Prop * A -> bool * (Type -> Set) .
+apply (Inhabited_correct _ _).
+change (Inhabited (Fun (Prod PROP (Var A)) (Prod Bool (Fun TYPE SET)))).
+Admitted.
+
+End type_reification.
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index 8b4cac5f4..7fb48aa43 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -33,7 +33,7 @@ Class Unconvertible (A : Type) (a b : A).
 
 Ltac unconvertible :=
   match goal with
-    | |- @Unconvertible _ ?x ?y => conv x y ; fail 1 "Convertible"
+    | |- @Unconvertible _ ?x ?y => unify x y with typeclass_instances ; fail 1 "Convertible"
     | |- _ => eapply Build_Unconvertible 
   end.
 
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index eb5c7cc11..fff78a85a 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -93,7 +93,7 @@ Ltac clear_dup :=
         | [ H' : ?Y |- _ ] =>
           match H with
             | H' => fail 2
-            | _ => conv X Y ; (clear H' || clear H)
+            | _ => unify X Y ; (clear H' || clear H)
           end
       end
   end.