aboutsummaryrefslogtreecommitdiff
path: root/intf
diff options
context:
space:
mode:
Diffstat (limited to 'intf')
-rw-r--r--intf/constrexpr.ml21
-rw-r--r--intf/decl_kinds.ml10
-rw-r--r--intf/evar_kinds.ml10
-rw-r--r--intf/extend.ml10
-rw-r--r--intf/genredexpr.ml10
-rw-r--r--intf/glob_term.ml10
-rw-r--r--intf/locus.ml10
-rw-r--r--intf/misctypes.ml10
-rw-r--r--intf/notation_term.ml10
-rw-r--r--intf/pattern.ml10
-rw-r--r--intf/vernacexpr.ml26
11 files changed, 85 insertions, 52 deletions
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml
index 5b51953bbe..31f811bc8a 100644
--- a/intf/constrexpr.ml
+++ b/intf/constrexpr.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Names
@@ -15,6 +17,11 @@ open Decl_kinds
(** [constr_expr] is the abstract syntax tree produced by the parser *)
+type universe_decl_expr = (lident list, glob_constraint list) gen_universe_decl
+
+type ident_decl = lident * universe_decl_expr option
+type name_decl = lname * universe_decl_expr option
+
type notation = string
type explicitation =
@@ -49,7 +56,7 @@ type cases_pattern_expr_r =
| CPatAlias of cases_pattern_expr * lname
| CPatCstr of reference
* cases_pattern_expr list option * cases_pattern_expr list
- (** [CPatCstr (_, c, Some l1, l2)] represents (@c l1) l2 *)
+ (** [CPatCstr (_, c, Some l1, l2)] represents [(@ c l1) l2] *)
| CPatAtom of reference option
| CPatOr of cases_pattern_expr list
| CPatNotation of notation * cases_pattern_notation_substitution
@@ -119,7 +126,7 @@ and recursion_order_expr =
| CWfRec of constr_expr
| CMeasureRec of constr_expr * constr_expr option (** measure, relation *)
-(** Anonymous defs allowed ?? *)
+(* Anonymous defs allowed ?? *)
and local_binder_expr =
| CLocalAssum of lname list * binder_kind * constr_expr
| CLocalDef of lname * constr_expr * constr_expr option
@@ -137,7 +144,7 @@ type constr_pattern_expr = constr_expr
type with_declaration_ast =
| CWith_Module of Id.t list Loc.located * qualid Loc.located
- | CWith_Definition of Id.t list Loc.located * constr_expr
+ | CWith_Definition of Id.t list Loc.located * universe_decl_expr option * constr_expr
type module_ast_r =
| CMident of qualid
diff --git a/intf/decl_kinds.ml b/intf/decl_kinds.ml
index b9a3f0c212..0d32853116 100644
--- a/intf/decl_kinds.ml
+++ b/intf/decl_kinds.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** Informal mathematical status of declarations *)
diff --git a/intf/evar_kinds.ml b/intf/evar_kinds.ml
index 428d6b6785..c5de383b21 100644
--- a/intf/evar_kinds.ml
+++ b/intf/evar_kinds.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Names
diff --git a/intf/extend.ml b/intf/extend.ml
index 78f0aa1178..10c9b3dc14 100644
--- a/intf/extend.ml
+++ b/intf/extend.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** Entry keys for constr notations *)
diff --git a/intf/genredexpr.ml b/intf/genredexpr.ml
index bdf3242ca3..80697461a6 100644
--- a/intf/genredexpr.ml
+++ b/intf/genredexpr.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** Reduction expressions *)
diff --git a/intf/glob_term.ml b/intf/glob_term.ml
index 3f48fa5479..39a7b956ab 100644
--- a/intf/glob_term.ml
+++ b/intf/glob_term.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** Untyped intermediate terms *)
diff --git a/intf/locus.ml b/intf/locus.ml
index 81fa704d88..95a2e495be 100644
--- a/intf/locus.ml
+++ b/intf/locus.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Names
diff --git a/intf/misctypes.ml b/intf/misctypes.ml
index aafd61b3c2..54a4861d09 100644
--- a/intf/misctypes.ml
+++ b/intf/misctypes.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Names
diff --git a/intf/notation_term.ml b/intf/notation_term.ml
index 86f5adbd78..a9c2e2a532 100644
--- a/intf/notation_term.ml
+++ b/intf/notation_term.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Names
diff --git a/intf/pattern.ml b/intf/pattern.ml
index 64873a0394..af2347674f 100644
--- a/intf/pattern.ml
+++ b/intf/pattern.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Names
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index ba28eaceaa..0a6e5b3b31 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Names
@@ -158,11 +160,6 @@ type option_ref_value =
(** Identifier and optional list of bound universes and constraints. *)
-type universe_decl_expr = (lident list, glob_constraint list) gen_universe_decl
-
-type ident_decl = lident * universe_decl_expr option
-type name_decl = lname * universe_decl_expr option
-
type sort_expr = Sorts.family
type definition_expr =
@@ -534,3 +531,14 @@ type vernac_when =
| VtNow
| VtLater
type vernac_classification = vernac_type * vernac_when
+
+
+(** Deprecated stuff *)
+type universe_decl_expr = Constrexpr.universe_decl_expr
+[@@ocaml.deprecated "alias of Constrexpr.universe_decl_expr"]
+
+type ident_decl = Constrexpr.ident_decl
+[@@ocaml.deprecated "alias of Constrexpr.ident_decl"]
+
+type name_decl = Constrexpr.name_decl
+[@@ocaml.deprecated "alias of Constrexpr.name_decl"]
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 14:15:00 +0000