From c9931180560b7b343427811be0f14281bc791bda Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 13 Mar 2011 14:41:09 +0000
Subject: - 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
---
 plugins/subtac/subtac_classes.ml  | 5 +++--
 plugins/subtac/subtac_classes.mli | 2 +-
 2 files changed, 4 insertions(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 419205a198..05e634c58b 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 c7687abf36..5b5c02037a 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
-- 
cgit v1.2.3