Various fixes on typeclasses:

- Better interface in constrintern w.r.t. evars used during typechecking
- Add "unsatisfiable_constraints" exception which gives back the raw
evar_map that was not satisfied during typeclass search (presentation
could be improved).
- Correctly infer the minimal sort for typeclasses declared as
definitions (everything was in type before).
- Really handle priorities in typeclass eauto: goals produced with higher
priority (lowest number) instances are tried before other of lower
priority goals, regardless of the number of subgoals.
- Change inverse to a notation for flip, now that universe polymorphic
definitions are handled correctly. 
- Add EquivalenceDec class similar to SetoidDec, declaring decision
procedures for equivalences.


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

4 files changed, 17 insertions, 4 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 9a0a0981e..eda8760a9 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -253,6 +253,10 @@ let new_class id par ar sup props =
 
   (* Interpret the arity *)
   let arity_imps, fullarity = 
+    let ar = 
+      match ar with
+	Some ar -> ar | None -> (dummy_loc, Rawterm.RType None)
+    in
     let arity = CSort (fst ar, snd ar) in
     let term = prod_constr_expr (prod_constr_expr arity par) sup in
       interp_type_evars isevars env0 term      
@@ -278,11 +282,15 @@ let new_class id par ar sup props =
       List.iter (fun (_,c,t) -> ce t; match c with Some c -> ce c | None -> ()) (params @ fields);
       match fields with
 	  [(Name proj_name, _, field)] ->
-	    let class_type = it_mkProd_or_LetIn arity params in
 	    let class_body = it_mkLambda_or_LetIn field params in
+	    let class_type = 
+	      match ar with
+		  Some _ -> Some (it_mkProd_or_LetIn arity params)
+		| None -> None
+	    in
 	    let class_entry = 
 	      { const_entry_body = class_body;
-		const_entry_type = Some class_type;
+		const_entry_type = class_type;
 		const_entry_opaque = false;
 		const_entry_boxed = false }
 	    in
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 973845d9c..da00044d9 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -35,7 +35,7 @@ val infer_super_instances : env -> constr list ->
 *)
 val new_class : identifier located ->
   local_binder list ->
-  Vernacexpr.sort_expr located ->
+  Vernacexpr.sort_expr located option ->
   local_binder list ->
   binder_list -> unit
 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 70441e50d..4adfaf6aa 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -488,6 +488,10 @@ let explain_no_instance env (_,id) l =
   str "applied to arguments" ++ spc () ++ 
     prlist_with_sep pr_spc (pr_lconstr_env env) l
 
+let explain_unsatisfiable_constraints env evm =
+  str"Unable to satisfy the following typeclass constraints:" ++ fnl() ++
+    Evd.pr_evar_map evm
+
 let explain_mismatched_contexts env c i j = 
   str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++
     hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_named_context env j) ++ fnl () ++ brk (1,1) ++ 
@@ -498,6 +502,7 @@ let explain_typeclass_error env err =
     | NotAClass c -> explain_not_a_class env c
     | UnboundMethod (cid, id) -> explain_unbound_method env cid id
     | NoInstance (id, l) -> explain_no_instance env id l
+    | UnsatisfiableConstraints evm -> explain_unsatisfiable_constraints env evm
     | MismatchedContextInstance (c, i, j) -> explain_mismatched_contexts env c i j
 	
 (* Refiner errors *)
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index ee0c42aa2..4579d43a6 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -228,7 +228,7 @@ type vernac_expr =
   | VernacClass of
       lident * (* name *)
 	local_binder list * (* params *)
-	sort_expr located * (* arity *)
+	sort_expr located option * (* arity *)
 	local_binder list * (* constraints *)
 	(lident * bool * constr_expr) list (* props, with substructure hints *)