aboutsummaryrefslogtreecommitdiff
path: root/intf
diff options
context:
space:
mode:
Diffstat (limited to 'intf')
-rw-r--r--intf/constrexpr.ml2
-rw-r--r--intf/decl_kinds.ml2
-rw-r--r--intf/evar_kinds.ml2
-rw-r--r--intf/extend.ml2
-rw-r--r--intf/genredexpr.ml2
-rw-r--r--intf/glob_term.ml2
-rw-r--r--intf/locus.ml2
-rw-r--r--intf/misctypes.ml2
-rw-r--r--intf/notation_term.ml7
-rw-r--r--intf/pattern.ml2
-rw-r--r--intf/tactypes.ml2
-rw-r--r--intf/vernacexpr.ml12
12 files changed, 24 insertions, 15 deletions
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml
index 593b190a6b..413cd9704b 100644
--- a/intf/constrexpr.ml
+++ b/intf/constrexpr.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/intf/decl_kinds.ml b/intf/decl_kinds.ml
index c15c009887..a977588332 100644
--- a/intf/decl_kinds.ml
+++ b/intf/decl_kinds.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/intf/evar_kinds.ml b/intf/evar_kinds.ml
index ac0d96e96b..36c421c6ca 100644
--- a/intf/evar_kinds.ml
+++ b/intf/evar_kinds.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/intf/extend.ml b/intf/extend.ml
index 99401d06f0..5552bed559 100644
--- a/intf/extend.ml
+++ b/intf/extend.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/intf/genredexpr.ml b/intf/genredexpr.ml
index 2a542e0ff2..a8c37c6207 100644
--- a/intf/genredexpr.ml
+++ b/intf/genredexpr.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/intf/glob_term.ml b/intf/glob_term.ml
index a35dae4aae..dd122b972d 100644
--- a/intf/glob_term.ml
+++ b/intf/glob_term.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/intf/locus.ml b/intf/locus.ml
index 57b398ab46..81fa704d88 100644
--- a/intf/locus.ml
+++ b/intf/locus.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/intf/misctypes.ml b/intf/misctypes.ml
index 2ab70a78ef..807882b42f 100644
--- a/intf/misctypes.ml
+++ b/intf/misctypes.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/intf/notation_term.ml b/intf/notation_term.ml
index 753fa657a8..cee96040bd 100644
--- a/intf/notation_term.ml
+++ b/intf/notation_term.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -83,9 +83,10 @@ type notation_interp_env = {
type grammar_constr_prod_item =
| GramConstrTerminal of Tok.t
| GramConstrNonTerminal of Extend.constr_prod_entry_key * Id.t option
- | GramConstrListMark of int * bool
+ | GramConstrListMark of int * bool * int
(* tells action rule to make a list of the n previous parsed items;
- concat with last parsed list if true *)
+ concat with last parsed list when true; additionally release
+ the p last items as if they were parsed autonomously *)
type notation_grammar = {
notgram_level : int;
diff --git a/intf/pattern.ml b/intf/pattern.ml
index 48381cacdc..2ab526984a 100644
--- a/intf/pattern.ml
+++ b/intf/pattern.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/intf/tactypes.ml b/intf/tactypes.ml
index 5c1d31946c..2c42e13110 100644
--- a/intf/tactypes.ml
+++ b/intf/tactypes.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 31ec444707..2adf522b74 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -305,6 +305,14 @@ type inline =
type module_ast_inl = module_ast * inline
type module_binder = bool option * lident list * module_ast_inl
+(** Cumulativity can be set globally, locally or unset locally and it
+ can not enabled at all. *)
+type cumulative_inductive_parsing_flag =
+ | GlobalCumulativity
+ | GlobalNonCumulativity
+ | LocalCumulativity
+ | LocalNonCumulativity
+
(** {6 The type of vernacular expressions} *)
type vernac_expr =
@@ -336,7 +344,7 @@ type vernac_expr =
| VernacExactProof of constr_expr
| VernacAssumption of (locality option * assumption_object_kind) *
inline * (plident list * constr_expr) with_coercion list
- | VernacInductive of cumulative_inductive_flag * private_flag * inductive_flag * (inductive_expr * decl_notation list) list
+ | VernacInductive of cumulative_inductive_parsing_flag * private_flag * inductive_flag * (inductive_expr * decl_notation list) list
| VernacFixpoint of
locality option * (fixpoint_expr * decl_notation list) list
| VernacCoFixpoint of
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 15:36:38 +0000