Specific syntax for Instances in Module Type: Declare Instance

NB: the grammar entry is placed in vernac:command on purpose
 even if it should have gone into vernac:gallina_ext. Camlp4
 isn't factorising rules starting by "Declare" in a correct way
 otherwise...

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

4 files changed, 11 insertions, 5 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 590f5c6f47..ca16e21313 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -128,7 +128,8 @@ let declare_instance_constant k pri global imps ?hook id term termtype =
     instance_hook k pri global imps ?hook (ConstRef kn);
     id
 
-let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
+let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
+    ?(generalize=true)
     ?(tac:Proof_type.tactic option) ?(hook:(global_reference -> unit) option) pri =
   let env = Global.env() in
   let evars = ref Evd.empty in
@@ -179,8 +180,10 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
   evars := resolve_typeclasses env !evars;
   let sigma =  !evars in
   let subst = List.map (Evarutil.nf_evar sigma) subst in
-    if Lib.is_modtype () then
+    if abstract then
       begin
+	if not (Lib.is_modtype ()) then
+	  error "Declare Instance while not in Module Type.";
 	let _, ty_constr = instance_constructor k (List.rev subst) in
 	let termtype =
 	  let t = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index c8439a1668..b8b104d47a 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -50,6 +50,7 @@ val declare_instance_constant :
   Names.identifier
 
 val new_instance :
+  ?abstract:bool -> (* Not abstract by default. *)
   ?global:bool -> (* Not global by default. *)
   local_binder list ->
   typeclass_constraint ->
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a90136d43e..7955d49163 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -611,9 +611,9 @@ let vernac_identity_coercion stre id qids qidt =
 
 (* Type classes *)
 
-let vernac_instance glob sup inst props pri =
+let vernac_instance abst glob sup inst props pri =
   Dumpglob.dump_constraint inst false "inst";
-  ignore(Classes.new_instance ~global:glob sup inst props pri)
+  ignore(Classes.new_instance ~abstract:abst ~global:glob sup inst props pri)
 
 let vernac_context l =
   List.iter (fun x -> Dumpglob.dump_local_binder x true "var") l;
@@ -1340,7 +1340,8 @@ let interp c = match c with
   | VernacIdentityCoercion (str,(_,id),s,t) -> vernac_identity_coercion str id s t
 
   (* Type classes *)
-  | VernacInstance (glob, sup, inst, props, pri) -> vernac_instance glob sup inst props pri
+  | VernacInstance (abst, glob, sup, inst, props, pri) ->
+      vernac_instance abst glob sup inst props pri
   | VernacContext sup -> vernac_context sup
   | VernacDeclareInstance (glob, id) -> vernac_declare_instance glob id
   | VernacDeclareClass id -> vernac_declare_class id
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 5be5c940b5..2df396e095 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -248,6 +248,7 @@ type vernac_expr =
 
   (* Type classes *)
   | VernacInstance of
+      bool * (* abstract instance *)
       bool * (* global *)
       local_binder list * (* super *)
 	typeclass_constraint * (* instance name, class name, params *)