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

2 files changed, 94 insertions, 0 deletions

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.