Fix mixup between Record, Structure and Class by adding a new variant for

the three cases.


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

5 files changed, 22 insertions, 15 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index b48548f98..d870c85eb 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -220,7 +220,9 @@ GEXTEND Gram
       | "CoInductive" -> false ] ]
   ;
   record_token:
-    [ [ IDENT "Record" -> (true,true) | IDENT "Structure" -> (false,true) ]]
+    [ [ IDENT "Record" -> (Record,true)
+      | IDENT "Structure" -> (Structure,true) 
+      | IDENT "Class" -> (Class,true) ] ]
   ;
   (* Simple definitions *)
   def_body:
@@ -254,8 +256,8 @@ GEXTEND Gram
 	      Constructors ((c id)::l)
       | id = identref ; c = constructor_type -> Constructors [ c id ]
       | cstr = identref; "{"; fs = LIST0 record_field SEP ";"; "}" -> 
-	     RecordDecl (false,Some cstr,fs) 
-      | "{";fs = LIST0 record_field SEP ";"; "}" -> RecordDecl (false,None,fs) 
+	     RecordDecl (Record,Some cstr,fs) 
+      | "{";fs = LIST0 record_field SEP ";"; "}" -> RecordDecl (Record,None,fs) 
       |  -> Constructors [] ] ]
   ;
 (*
@@ -503,7 +505,7 @@ GEXTEND Gram
       | IDENT "Class"; qid = identref; pars = binders_let;
            s = OPT [ ":"; c = lconstr -> c ];
 	   fs = class_fields ->
-	   VernacInductive (false, [((qid,pars,s,RecordDecl (false,None,fs)),None)])
+	   VernacInductive (false, [((qid,pars,s,RecordDecl (Class,None,fs)),None)])
 
       (* Type classes *)
       | IDENT "Class"; sup = OPT [ l = binders_let; "=>" -> l ];
@@ -511,7 +513,7 @@ GEXTEND Gram
          s = OPT [ ":"; c = lconstr -> c ];
 	 fs = class_fields ->
 	   VernacInductive 
-	     (false, [((qid,Option.cata (fun x -> x) [] sup @ pars,s,RecordDecl (false,None,fs)),None)])
+	     (false, [((qid,Option.cata (fun x -> x) [] sup @ pars,s,RecordDecl (Class,None,fs)),None)])
 	     
       | IDENT "Context"; c = binders_let -> 
 	  VernacContext c
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index e16b4e533..0fc28d35f 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -667,7 +667,7 @@ let rec pr_vernac = function
   (* Gallina extensions *)
   | VernacRecord ((b,coind),(oc,name),ps,s,c,fs) ->
       hov 2
-        (str (if b then "Record" else "Class") ++
+        (str (match b with Record -> "Record" | Structure -> "Structure" | Class -> "Class") ++
          (if oc then str" > " else str" ") ++ pr_lident name ++ 
           pr_and_type_binders_arg ps ++ str" :" ++ spc() ++ 
 	  Option.cata pr_lconstr_expr (mt()) s ++ str" := " ++ pr_record_decl b c fs)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index c066bae5c..f1ee0ab65 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -341,6 +341,8 @@ let declare_class finite id idbuild paramimpls params arity fieldimpls fields
       k.cl_projs coers;
     add_class k; impl
 
+open Vernacexpr
+
 (* [fs] corresponds to fields and [ps] to parameters; [coers] is a boolean 
    list telling if the corresponding fields must me declared as coercion *)
 let definition_structure (kind,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) =
@@ -358,9 +360,11 @@ let definition_structure (kind,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) =
     States.with_heavy_rollback (fun () ->
       typecheck_params_and_fields idstruc sc ps notations fs) ()
   in
-    if kind then
-      let arity = Option.cata (fun x -> x) (new_Type ()) sc in
-      let implfs = List.map
-	(fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs
-      in IndRef (declare_structure finite idstruc idbuild implpars params arity implfs fields is_coe coers)
-    else declare_class finite (loc,idstruc) idbuild implpars params sc implfs fields is_coe coers
+    match kind with
+    | Record | Structure ->
+	let arity = Option.cata (fun x -> x) (new_Type ()) sc in
+	let implfs = List.map
+	  (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs
+	in IndRef (declare_structure finite idstruc idbuild implpars params arity implfs fields is_coe coers)
+    | Class ->
+	declare_class finite (loc,idstruc) idbuild implpars params sc implfs fields is_coe coers
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 57d8cccc0..8a4ca735c 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -36,5 +36,5 @@ val declare_structure : bool (*coinductive?*)-> identifier -> identifier ->
   inductive
 
 val definition_structure :
-  bool (* structure or class *) * bool (*coinductive?*)*lident with_coercion * local_binder list *
+  record_kind * bool (*coinductive?*)*lident with_coercion * local_binder list *
   (local_decl_expr with_coercion with_notation) list * identifier * sorts option -> global_reference
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 8addcd3ca..5fff24fef 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -155,6 +155,7 @@ type local_decl_expr =
   | AssumExpr of lname * constr_expr
   | DefExpr of lname * constr_expr * constr_expr option
 
+type record_kind = Record | Structure | Class
 type decl_notation = (string * constr_expr * scope_name option) option
 type simple_binder = lident list  * constr_expr
 type class_binder = lident * constr_expr list
@@ -163,7 +164,7 @@ type 'a with_notation = 'a * decl_notation
 type constructor_expr = (lident * constr_expr) with_coercion
 type constructor_list_or_record_decl_expr =
   | Constructors of constructor_expr list
-  | RecordDecl of bool * lident option * local_decl_expr with_coercion with_notation list
+  | RecordDecl of record_kind * lident option * local_decl_expr with_coercion with_notation list
 type inductive_expr =
   lident * local_binder list * constr_expr option * constructor_list_or_record_decl_expr
 
@@ -216,7 +217,7 @@ type vernac_expr =
   | VernacCombinedScheme of lident * lident list
 
   (* Gallina extensions *)
-  | VernacRecord of (bool*bool) (* = Structure or Class * Inductive or CoInductive *)
+  | VernacRecord of (record_kind*bool) (* = Structure or Class * Inductive or CoInductive *)
       * lident with_coercion * local_binder list
       * constr_expr option * lident option * local_decl_expr with_coercion with_notation list
   | VernacBeginSection of lident