Merge branch 'subclasses' into coq-trunk

Stop using hnf_constr in unify_type, which might unfold constants
that are marked opaque for unification.
Conflicts:
	pretyping/unification.ml

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

7 files changed, 69 insertions, 61 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index c50346a00f..c76055d4f7 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -630,9 +630,8 @@ let w_coerce env evd mv c =
 let unify_to_type env sigma flags c status u =
   let c = refresh_universes c in
   let t = get_type_of env sigma c in
-  let t = Tacred.hnf_constr env sigma (nf_betaiota sigma (nf_meta sigma t)) in
-  let u = Tacred.hnf_constr env sigma u in
-    unify_0 env sigma CUMUL flags t u
+  let t = nf_betaiota sigma (nf_meta sigma t) in
+    unify_0 env sigma Cumul flags t u
 
 let unify_type env sigma flags mv status c =
   let mvty = Typing.meta_type sigma mv in
diff --git a/tactics/auto.ml b/tactics/auto.ml
index fa1985d8c5..f4952cf0d2 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -356,7 +356,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri ?name (c,cty) =
    cty is the type of constr *)
 
 let make_resolves env sigma flags pri ?name c =
-  let cty = type_of env sigma c in
+  let cty = Retyping.get_type_of env sigma c in
   let ents =
     map_succeed
       (fun f -> f (c,cty))
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 41894ec511..16e38598b5 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -230,21 +230,39 @@ let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) =
 	       if not (eq_constr ty' ar) then iscl env' ty'
 	       else false
   in
-  let keep = not only_classes || iscl env cty in
-    if keep then let c = mkVar id in
-      map_succeed 
-	(fun f -> try f (c,cty) with UserError _ -> failwith "") 
+  let is_class = iscl env cty in
+  let keep = not only_classes || is_class in
+    if keep then 
+      let c = mkVar id in
+      let hints =
+	if is_class then
+	  let hints = build_subclasses env sigma (mkVar id) in
+	    list_map_append
+	      (make_resolves env sigma (true,false,Flags.is_verbose()) None) hints
+	else []
+      in
+	hints @ map_succeed 
+	  (fun f -> try f (c,cty) with UserError _ -> failwith "") 
 	[make_exact_entry sigma pri; make_apply_entry env sigma flags pri]
     else []
 
 let pf_filtered_hyps gls = 
-  Goal.V82.filtered_context gls.Evd.sigma (sig_it gls)
+  Goal.V82.hyps gls.Evd.sigma (sig_it gls)
 
-let make_autogoal_hints only_classes ?(st=full_transparent_state) g =
-  let sign = pf_filtered_hyps g in
-  let hintlist = list_map_append (pf_apply make_resolve_hyp g st (true,false,false) only_classes None) sign in
-    Hint_db.add_list hintlist (Hint_db.empty st true)
-  
+let make_hints g st only_classes sign =
+  let hintlist = list_map_append 
+    (pf_apply make_resolve_hyp g st (true,false,false) only_classes None) sign
+  in Hint_db.add_list hintlist (Hint_db.empty st true)
+    
+let make_autogoal_hints = 
+  let res = ref None in
+    fun only_classes ?(st=full_transparent_state) g ->
+    let sign = pf_filtered_hyps g in
+      match !res with
+      | Some (sign', hints) when sign = sign' -> hints
+      | _ -> let hints = make_hints g st only_classes (Environ.named_context_of_val sign) in
+	  res := Some (sign, hints); hints
+	  
 let lift_tactic tac (f : goal list sigma -> autoinfo -> autogoal list sigma) : 'a tac =
   { skft = fun sk fk {it = gl,hints; sigma=s} ->
     let res = try Some (tac {it=gl; sigma=s}) with e when catchable e -> None in
@@ -603,8 +621,10 @@ let initial_select_evars onlyargs =
     (fun evd ev evi -> Typeclasses.is_class_evar evd evi)
 
 let resolve_typeclass_evars debug m env evd onlyargs split fail =
-  let evd = Evarconv.consider_remaining_unif_problems
-    ~ts:(Typeclasses.classes_transparent_state ()) env evd 
+  let evd = 
+    try Evarconv.consider_remaining_unif_problems
+      ~ts:(Typeclasses.classes_transparent_state ()) env evd
+    with _ -> evd
   in
     resolve_all_evars debug m env (initial_select_evars onlyargs) evd split fail
 
diff --git a/test-suite/bugs/closed/shouldsucceed/2362.v b/test-suite/bugs/closed/shouldsucceed/2362.v
index 897f7c456f..febb9c7bb0 100644
--- a/test-suite/bugs/closed/shouldsucceed/2362.v
+++ b/test-suite/bugs/closed/shouldsucceed/2362.v
@@ -17,7 +17,6 @@ Notation "( x ,> y )" := (fpair x y) (at level 0).
 Instance Pointed_FPair B neutral:
  Pointed (fun A => FPair A B neutral) :=
  { creturn := fun A (a:A) => (a,> neutral) }.
-
 Definition blah_fail (x:bool) : FPair bool nat O :=
   creturn x.
 Set Printing All. Print blah_fail.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index f75c9274d3..9b8301a5d0 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -230,28 +230,34 @@ Hint Extern 4 (subrelation (inverse _) _) =>
 
 (** The complement of a relation conserves its proper elements. *)
 
-Program Instance complement_proper
+Program Definition complement_proper
   `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) :
-  Proper (RA ==> RA ==> iff) (complement R).
+  Proper (RA ==> RA ==> iff) (complement R) := _.
 
-  Next Obligation.
+ Next Obligation.
   Proof.
     unfold complement.
     pose (mR x y H x0 y0 H0).
     intuition.
   Qed.
+ 
+Hint Extern 1 (Proper (_ ==> _ ==> iff) (complement _)) => 
+  apply @complement_proper : typeclass_instances.
 
 (** The [inverse] too, actually the [flip] instance is a bit more general. *)
 
-Program Instance flip_proper
+Program Definition flip_proper
   `(mor : Proper (A -> B -> C) (RA ==> RB ==> RC) f) :
-  Proper (RB ==> RA ==> RC) (flip f).
+  Proper (RB ==> RA ==> RC) (flip f) := _.
 
   Next Obligation.
   Proof.
     apply mor ; auto.
   Qed.
 
+Hint Extern 1 (Proper (_ ==> _ ==> _) (flip _)) => 
+  apply @flip_proper : typeclass_instances.
+
 (** Every Transitive relation gives rise to a binary morphism on [impl],
    contravariant in the first argument, covariant in the second. *)
 
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index e70f65308d..6c26ce598b 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -283,40 +283,25 @@ let named_of_rel_context l =
 let string_of_global r =
  string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty r)
 
-let declare_subclasses gr cl =
-  let rec build_subclasses c (rels, (tc, args)) =
-    let projs = list_map_filter 
-      (fun (n, b, proj) ->
-	 if b then Option.map (fun p -> Nameops.out_name n, mkConst p) proj
-	 else None) tc.cl_projs 
-    in
-    let instapp = appvectc (constr_of_global gr)
-      (Termops.extended_rel_vect 0 rels)
-    in
-    let projargs = 
-      Array.of_list (args @ [instapp])
-    in
-    let declare_proj (n, p) =
-      let body = it_mkLambda_or_LetIn (mkApp (p, projargs)) rels in
-	(*     let ce = { *)
-	(*       const_entry_body   = ; *)
-(*       const_entry_type   = None; *)
-(*       const_entry_opaque = false } *)
-(*     in *)
-(*     let cst = Declare.declare_constant ~internal:Declare.KernelSilent  *)
-(*       (Nameops.add_suffix (Nameops.add_suffix (id_of_string (string_of_global gr)) "_")  *)
-(* 	 (string_of_id n)) *)
-(*       (DefinitionEntry ce, IsAssumption Logical) *)
-(*     in *)
-      let ty = Retyping.get_type_of (Global.env ()) Evd.empty body in
-	match class_of_constr ty with
-	| Some (rels, (tc, args) as cl) ->
-	    (* 	  add_instance (Typeclasses.new_instance tc None false (ConstRef cst)); *)
-	    body :: build_subclasses body cl
-	| None -> []
-    in list_map_append declare_proj projs
-  in
-  let hints = build_subclasses (constr_of_global gr) cl in
+let rec build_subclasses env sigma c =
+  let ty = Retyping.get_type_of env sigma c in
+    match class_of_constr ty with
+    | None -> []
+    | Some (rels, (tc, args)) ->
+	let projs = list_map_filter 
+	  (fun (n, b, proj) ->
+	     if b then Option.map (fun p -> Nameops.out_name n, mkConst p) proj
+	     else None) tc.cl_projs 
+	in
+	let instapp = appvectc c (Termops.extended_rel_vect 0 rels) in
+	let projargs = Array.of_list (args @ [instapp]) in
+	let declare_proj (n, p) =
+	  let body = it_mkLambda_or_LetIn (mkApp (p, projargs)) rels in
+	    body :: build_subclasses env sigma body
+	in list_map_append declare_proj projs
+	     
+let declare_subclasses constr =
+  let hints = build_subclasses (Global.env ()) Evd.empty constr in
   let entry = List.map (fun c -> (None, false, None, c)) hints in
     Auto.add_hints true (* local *) [typeclasses_db] (Auto.HintsResolveEntry entry)
 
@@ -346,9 +331,7 @@ let context l =
 	   match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls
       in
 	Command.declare_assumption false (Local (* global *), Definitional) t
-	  [] impl (* implicit *) None (* inline *) (dummy_loc, id))
-(* 	match class_of_constr t with *)
-(* 	| None -> () *)
-(* 	| Some tc -> declare_subclasses (VarRef id) tc) *)
+	  [] impl (* implicit *) None (* inline *) (dummy_loc, id);
+	declare_subclasses (mkVar id))
   in List.iter fn (List.rev ctx)
-	
+       
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index b57f1bea07..0f842ffe50 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -73,3 +73,4 @@ val context : local_binder list -> unit
 
 val refine_ref : (open_constr -> Proof_type.tactic) ref
 
+val build_subclasses : env -> evar_map -> constr -> constr list