- Add modulo_delta_types flag for unification to allow full

conversion when checking types of instanciations while having
restricted delta reduction for unification itself. This
makes auto/eauto... backward compatible.
- Change semantics of [Instance foo : C a.] to _not_ search
for an instance of [C a] automatically and potentially slow
down interaction, except for trivial classes with no fields.
Use [C a := _.] or [C a := {}] to search for an instance of
the class or for every field.
- Correct treatment of transparency information for classes 
declared in sections.


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

2 files changed, 4 insertions, 3 deletions

diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 419205a19..05e634c58 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -109,11 +109,12 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
   let subst = List.map (Evarutil.nf_evar sigma) subst in
   let props =
     match props with
-    | CRecord (loc, _, fs) ->
+    | Some (CRecord (loc, _, fs)) ->
 	if List.length fs > List.length k.cl_props then
 	  Classes.mismatched_props env' (List.map snd fs) k.cl_props;
 	Inl fs
-    | _ -> Inr props
+    | Some p -> Inr p
+    | None -> Inl []
   in
   let subst =
     match props with
diff --git a/plugins/subtac/subtac_classes.mli b/plugins/subtac/subtac_classes.mli
index c7687abf3..5b5c02037 100644
--- a/plugins/subtac/subtac_classes.mli
+++ b/plugins/subtac/subtac_classes.mli
@@ -33,7 +33,7 @@ val new_instance :
   ?global:bool ->
   local_binder list ->
   typeclass_constraint ->
-  constr_expr ->
+  constr_expr option ->
   ?generalize:bool ->
   int option ->
   identifier * Subtac_obligations.progress