Don't duplicate the inductive keyword for each block elt when parsing

6 files changed, 45 insertions, 47 deletions

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 84f09c385f..fdbad2ab9e 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1512,12 +1512,12 @@ let do_build_inductive
         let _time3 = System.get_time () in
 (* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
         let repacked_rel_inds =
-          List.map  (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn )
+          List.map  (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c, Vernacexpr.Constructors l),ntn )
                           rel_inds
         in
         let msg =
           str "while trying to define"++ spc () ++
-            Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)})
+            Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Vernacexpr.Inductive_kw,repacked_rel_inds)})
             ++ fnl () ++
             msg
         in
@@ -1527,12 +1527,12 @@ let do_build_inductive
         let _time3 = System.get_time () in
 (* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
         let repacked_rel_inds =
-          List.map  (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn )
+          List.map  (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c, Vernacexpr.Constructors l),ntn )
                           rel_inds
         in
         let msg =
           str "while trying to define"++ spc () ++
-            Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)})
+            Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Vernacexpr.Inductive_kw,repacked_rel_inds)})
             ++ fnl () ++
             CErrors.print reraise
         in
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index c5b3e0931b..65ef2ca8c6 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -131,7 +131,7 @@ let classify_vernac e =
         VtSideff ([id.CAst.v], VtLater)
     | VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id, VtLater)
     | VernacInductive (_, _,_,l) ->
-        let ids = List.map (fun (((_,({v=id},_)),_,_,_,cl),_) -> id :: match cl with
+        let ids = List.map (fun (((_,({v=id},_)),_,_,cl),_) -> id :: match cl with
         | Constructors l -> List.map (fun (_,({v=id},_)) -> id) l
         | RecordDecl (oid,l) -> (match oid with Some {v=x} -> [x] | _ -> []) @
            CList.map_filter (function
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index d0374bc4fa..74249301d7 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -21,7 +21,6 @@ open Constrexpr_ops
 open Extend
 open Decls
 open Declaremods
-open Declarations
 open Namegen
 open Tok (* necessary for camlp5 *)
 
@@ -200,9 +199,7 @@ GRAMMAR EXTEND Gram
       (* Gallina inductive declarations *)
       | cum = OPT cumulativity_token; priv = private_token; f = finite_token;
         indl = LIST1 inductive_definition SEP "with" ->
-          { let (k,f) = f in
-          let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
-          VernacInductive (cum, priv,f,indl) }
+          { VernacInductive (cum, priv, f, indl) }
       | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
           { VernacFixpoint (NoDischarge, recs) }
       | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
@@ -337,12 +334,12 @@ GRAMMAR EXTEND Gram
   ] ]
   ;
   finite_token:
-    [ [ IDENT "Inductive" -> { (Inductive_kw,Finite) }
-      | IDENT "CoInductive" -> { (CoInductive,CoFinite) }
-      | IDENT "Variant" -> { (Variant,BiFinite) }
-      | IDENT "Record" -> { (Record,BiFinite) }
-      | IDENT "Structure" -> { (Structure,BiFinite) }
-      | IDENT "Class" -> { (Class true,BiFinite) } ] ]
+    [ [ IDENT "Inductive" -> { Inductive_kw }
+      | IDENT "CoInductive" -> { CoInductive }
+      | IDENT "Variant" -> { Variant }
+      | IDENT "Record" -> { Record }
+      | IDENT "Structure" -> { Structure }
+      | IDENT "Class" -> { Class true } ] ]
   ;
   cumulativity_token:
     [ [ IDENT "Cumulative" -> { VernacCumulative }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 82132a1af6..6240120cb0 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -476,7 +476,7 @@ let string_of_theorem_kind = let open Decls in function
     let prpri = match pri with None -> mt() | Some i -> str "| " ++ int i in
     prx ++ prpri ++ prlist (pr_decl_notation @@ pr_constr env sigma) ntn
 
-  let pr_record_decl b c fs =
+  let pr_record_decl c fs =
     pr_opt pr_lident c ++ (if c = None then str"{" else str" {") ++
       hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}")
 
@@ -802,7 +802,7 @@ let string_of_definition_object_kind = let open Decls in function
                    (if coe then str":>" else str":") ++
                    Flags.without_option Flags.beautify pr_spc_lconstr c)
         in
-        let pr_constructor_list b l = match l with
+        let pr_constructor_list l = match l with
           | Constructors [] -> mt()
           | Constructors l ->
             let fst_sep = match l with [_] -> "   " | _ -> " | " in
@@ -810,21 +810,20 @@ let string_of_definition_object_kind = let open Decls in function
               fnl() ++ str fst_sep ++
               prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l
           | RecordDecl (c,fs) ->
-            pr_record_decl b c fs
+            pr_record_decl c fs
         in
-        let pr_oneind key (((coe,iddecl),indpar,s,k,lc),ntn) =
+        let pr_oneind key (((coe,iddecl),indpar,s,lc),ntn) =
           hov 0 (
             str key ++ spc() ++
               (if coe then str"> " else str"") ++ pr_ident_decl iddecl ++
               pr_and_type_binders_arg indpar ++
               pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr env sigma s) s ++
-              str" :=") ++ pr_constructor_list k lc ++
+              str" :=") ++ pr_constructor_list lc ++
             prlist (pr_decl_notation @@ pr_constr env sigma) ntn
         in
         let key =
-          let (_,_,_,k,_),_ = List.hd l in
           let kind =
-            match k with Record -> "Record" | Structure -> "Structure"
+            match f with Record -> "Record" | Structure -> "Structure"
                        | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
                        | Class _ -> "Class" | Variant -> "Variant"
           in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index f8eef68997..bb8df512ca 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -661,25 +661,30 @@ let vernac_record ~template udecl cum k poly finite records =
 let extract_inductive_udecl (indl:(inductive_expr * decl_notation list) list) =
   match indl with
   | [] -> assert false
-  | (((coe,(id,udecl)),b,c,k,d),e) :: rest ->
-    let rest = List.map (fun (((coe,(id,udecl)),b,c,k,d),e) ->
+  | (((coe,(id,udecl)),b,c,d),e) :: rest ->
+    let rest = List.map (fun (((coe,(id,udecl)),b,c,d),e) ->
         if Option.has_some udecl
         then user_err ~hdr:"inductive udecl" Pp.(strbrk "Universe binders must be on the first inductive of the block.")
-        else (((coe,id),b,c,k,d),e))
+        else (((coe,id),b,c,d),e))
         rest
     in
-    udecl, (((coe,id),b,c,k,d),e) :: rest
+    udecl, (((coe,id),b,c,d),e) :: rest
+
+let finite_of_kind = let open Declarations in function
+  | Inductive_kw -> Finite
+  | CoInductive -> CoFinite
+  | Variant | Record | Structure | Class _ -> BiFinite
 
 (** When [poly] is true the type is declared polymorphic. When [lo] is true,
     then the type is declared private (as per the [Private] keyword). [finite]
     indicates whether the type is inductive, co-inductive or
     neither. *)
-let vernac_inductive ~atts cum lo finite indl =
+let vernac_inductive ~atts cum lo kind indl =
   let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in
   let open Pp in
   let udecl, indl = extract_inductive_udecl indl in
   if Dumpglob.dump () then
-    List.iter (fun (((coe,lid), _, _, _, cstrs), _) ->
+    List.iter (fun (((coe,lid), _, _, cstrs), _) ->
       match cstrs with
         | Constructors cstrs ->
             Dumpglob.dump_definition lid false "ind";
@@ -688,16 +693,17 @@ let vernac_inductive ~atts cum lo finite indl =
         | _ -> () (* dumping is done by vernac_record (called below) *) )
       indl;
 
+  let finite = finite_of_kind kind in
   let is_record = function
-  | ((_ , _ , _ , _, RecordDecl _), _) -> true
+  | ((_ , _ , _ , RecordDecl _), _) -> true
   | _ -> false
   in
   let is_constructor = function
-  | ((_ , _ , _ , _, Constructors _), _) -> true
+  | ((_ , _ , _ , Constructors _), _) -> true
   | _ -> false
   in
-  let is_defclass = match indl with
-  | [ ( id , bl , c , Class _, Constructors [l]), [] ] -> Some (id, bl, c, l)
+  let is_defclass = match kind, indl with
+  | Class _, [ ( id , bl , c , Constructors [l]), [] ] -> Some (id, bl, c, l)
   | _ -> None
   in
   if Option.has_some is_defclass then
@@ -710,38 +716,35 @@ let vernac_inductive ~atts cum lo finite indl =
     vernac_record ~template udecl cum (Class true) poly finite [id, bl, c, None, [f]]
   else if List.for_all is_record indl then
     (* Mutual record case *)
-    let check_kind ((_, _, _, kind, _), _) = match kind with
-    | Variant ->
-      user_err (str "The Variant keyword does not support syntax { ... }.")
-    | Record | Structure | Class _ | Inductive_kw | CoInductive -> ()
+    let () = match kind with
+      | Variant ->
+        user_err (str "The Variant keyword does not support syntax { ... }.")
+      | Record | Structure | Class _ | Inductive_kw | CoInductive -> ()
     in
-    let () = List.iter check_kind indl in
-    let check_where ((_, _, _, _, _), wh) = match wh with
+    let check_where ((_, _, _, _), wh) = match wh with
     | [] -> ()
     | _ :: _ ->
       user_err (str "where clause not supported for records")
     in
     let () = List.iter check_where indl in
-    let unpack ((id, bl, c, _, decl), _) = match decl with
+    let unpack ((id, bl, c, decl), _) = match decl with
     | RecordDecl (oc, fs) ->
       (id, bl, c, oc, fs)
     | Constructors _ -> assert false (* ruled out above *)
     in
-    let ((_, _, _, kind, _), _) = List.hd indl in
     let kind = match kind with Class _ -> Class false | _ -> kind in
     let recordl = List.map unpack indl in
     vernac_record ~template udecl cum kind poly finite recordl
   else if List.for_all is_constructor indl then
     (* Mutual inductive case *)
-    let check_kind ((_, _, _, kind, _), _) = match kind with
+    let () = match kind with
     | (Record | Structure) ->
       user_err (str "The Record keyword is for types defined using the syntax { ... }.")
     | Class _ ->
       user_err (str "Inductive classes not supported")
     | Variant | Inductive_kw | CoInductive -> ()
     in
-    let () = List.iter check_kind indl in
-    let check_name ((na, _, _, _, _), _) = match na with
+    let check_name ((na, _, _, _), _) = match na with
     | (true, _) ->
       user_err (str "Variant types do not handle the \"> Name\" \
         syntax, which is reserved for records. Use the \":>\" \
@@ -749,7 +752,7 @@ let vernac_inductive ~atts cum lo finite indl =
     | _ -> ()
     in
     let () = List.iter check_name indl in
-    let unpack (((_, id) , bl, c, _, decl), ntn) = match decl with
+    let unpack (((_, id) , bl, c, decl), ntn) = match decl with
     | Constructors l -> (id, bl, c, l), ntn
     | RecordDecl _ -> assert false (* ruled out above *)
     in
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 22a8de7f99..8ead56dfdf 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -104,7 +104,6 @@ type coercion_flag  = bool (* true = AddCoercion    false = NoCoercion     *)
 type instance_flag  = bool option
   (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *)
 type export_flag    = bool (* true = Export;        false = Import         *)
-type inductive_flag = Declarations.recursivity_kind
 type onlyparsing_flag = { onlyparsing : bool }
  (* Some v = Parse only;  None = Print also.
     If v<>Current, it contains the name of the coq version
@@ -165,7 +164,7 @@ type constructor_list_or_record_decl_expr =
   | Constructors of constructor_expr list
   | RecordDecl of lident option * (local_decl_expr * record_field_attr) list
 type inductive_expr =
-  ident_decl with_coercion * local_binder_expr list * constr_expr option * inductive_kind *
+  ident_decl with_coercion * local_binder_expr list * constr_expr option *
     constructor_list_or_record_decl_expr
 
 type one_inductive_expr =
@@ -306,7 +305,7 @@ type nonrec vernac_expr =
   | VernacExactProof of constr_expr
   | VernacAssumption of (discharge * Decls.assumption_object_kind) *
       Declaremods.inline * (ident_decl list * constr_expr) with_coercion list
-  | VernacInductive of vernac_cumulative option * bool (* private *) * inductive_flag * (inductive_expr * decl_notation list) list
+  | VernacInductive of vernac_cumulative option * bool (* private *) * inductive_kind * (inductive_expr * decl_notation list) list
   | VernacFixpoint of discharge * fixpoint_expr list
   | VernacCoFixpoint of discharge * cofixpoint_expr list
   | VernacScheme of (lident option * scheme) list