aboutsummaryrefslogtreecommitdiff
path: root/intf
diff options
context:
space:
mode:
Diffstat (limited to 'intf')
-rw-r--r--intf/constrexpr.ml12
-rw-r--r--intf/decl_kinds.ml6
-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.ml18
-rw-r--r--intf/locus.ml2
-rw-r--r--intf/misctypes.ml2
-rw-r--r--intf/notation_term.ml2
-rw-r--r--intf/pattern.ml2
-rw-r--r--intf/tactypes.ml2
-rw-r--r--intf/vernacexpr.ml13
12 files changed, 43 insertions, 22 deletions
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml
index 614c097b5a..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 *)
@@ -31,8 +31,16 @@ type abstraction_kind = AbsLambda | AbsPi
type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
+(** Representation of integer literals that appear in Coq scripts.
+ We now use raw strings of digits in base 10 (big-endian), and a separate
+ sign flag. Note that this representation is not unique, due to possible
+ multiple leading zeros, and -0 = +0 *)
+
+type sign = bool
+type raw_natural_number = string
+
type prim_token =
- | Numeral of Bigint.bigint (** representation of integer literals that appear in Coq scripts. *)
+ | Numeral of raw_natural_number * sign
| String of string
type instance_expr = Misctypes.glob_level list
diff --git a/intf/decl_kinds.ml b/intf/decl_kinds.ml
index 8254b1b802..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 *)
@@ -14,7 +14,9 @@ type binding_kind = Explicit | Implicit
type polymorphic = bool
-type private_flag = bool
+type private_flag = bool
+
+type cumulative_inductive_flag = bool
type theorem_kind =
| Theorem
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 5da20c9d1c..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 *)
@@ -95,3 +95,19 @@ type closure = {
and closed_glob_constr = {
closure: closure;
term: glob_constr }
+
+(** Ltac variable maps *)
+type var_map = Pattern.constr_under_binders Id.Map.t
+type uconstr_var_map = closed_glob_constr Id.Map.t
+type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t
+
+type ltac_var_map = {
+ ltac_constrs : var_map;
+ (** Ltac variables bound to constrs *)
+ ltac_uconstrs : uconstr_var_map;
+ (** Ltac variables bound to untyped constrs *)
+ ltac_idents: Id.t Id.Map.t;
+ (** Ltac variables bound to identifiers *)
+ ltac_genargs : unbound_ltac_var_map;
+ (** Ltac variables bound to other kinds of arguments *)
+}
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..0fa0afdad7 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 *)
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 ab440c6b71..6ef9532ad7 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 *)
@@ -96,17 +96,13 @@ type locatable =
type showable =
| ShowGoal of goal_reference
- | ShowGoalImplicitly of int option
| ShowProof
- | ShowNode
| ShowScript
| ShowExistentials
| ShowUniverses
- | ShowTree
| ShowProofNames
| ShowIntros of bool
| ShowMatch of reference
- | ShowThesis
type comment =
| CommentConstr of constr_expr
@@ -335,12 +331,12 @@ type vernac_expr =
(* Gallina *)
| VernacDefinition of
(locality option * definition_object_kind) * plident * definition_expr
- | VernacStartTheoremProof of theorem_kind * proof_expr list * bool
+ | VernacStartTheoremProof of theorem_kind * proof_expr list
| VernacEndProof of proof_end
| VernacExactProof of constr_expr
| VernacAssumption of (locality option * assumption_object_kind) *
inline * (plident list * constr_expr) with_coercion list
- | VernacInductive of private_flag * inductive_flag * (inductive_expr * decl_notation list) list
+ | VernacInductive of cumulative_inductive_flag * private_flag * inductive_flag * (inductive_expr * decl_notation list) list
| VernacFixpoint of
locality option * (fixpoint_expr * decl_notation list) list
| VernacCoFixpoint of
@@ -499,10 +495,9 @@ type vernac_type =
| VtQed of vernac_qed_type
| VtProofStep of proof_step
| VtProofMode of string
- | VtQuery of vernac_part_of_script * report_with
+ | VtQuery of vernac_part_of_script * Feedback.route_id
| VtStm of vernac_control * vernac_part_of_script
| VtUnknown
-and report_with = Stateid.t * Feedback.route_id (* feedback on id/route *)
and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *)
and vernac_start = string * opacity_guarantee * Id.t list
and vernac_sideff_type = Id.t list
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 20:18:12 +0000