diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/constrexpr.mli | 31 | ||||
| -rw-r--r-- | intf/decl_kinds.mli | 2 | ||||
| -rw-r--r-- | intf/evar_kinds.mli | 2 | ||||
| -rw-r--r-- | intf/extend.mli | 65 | ||||
| -rw-r--r-- | intf/genredexpr.mli | 2 | ||||
| -rw-r--r-- | intf/glob_term.mli | 10 | ||||
| -rw-r--r-- | intf/locus.mli | 2 | ||||
| -rw-r--r-- | intf/misctypes.mli | 14 | ||||
| -rw-r--r-- | intf/notation_term.mli | 4 | ||||
| -rw-r--r-- | intf/pattern.mli | 2 | ||||
| -rw-r--r-- | intf/tacexpr.mli | 61 | ||||
| -rw-r--r-- | intf/vernacexpr.mli | 64 |
12 files changed, 160 insertions, 99 deletions
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index 79f4e99e1f..efd5129b66 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -32,21 +32,23 @@ type abstraction_kind = AbsLambda | AbsPi type proj_flag = int option (** [Some n] = proj of the n-th visible argument *) -type prim_token = Numeral of Bigint.bigint | String of string +type prim_token = + | Numeral of Bigint.bigint (** representation of integer literals that appear in Coq scripts. *) + | String of string type raw_cases_pattern_expr = | RCPatAlias of Loc.t * raw_cases_pattern_expr * Id.t | RCPatCstr of Loc.t * Globnames.global_reference * raw_cases_pattern_expr list * raw_cases_pattern_expr list - (** [CPatCstr (_, Inl c, l1, l2)] represents (@c l1) l2 *) + (** [CPatCstr (_, c, l1, l2)] represents ((@c l1) l2) *) | RCPatAtom of Loc.t * Id.t option | RCPatOr of Loc.t * raw_cases_pattern_expr list type cases_pattern_expr = | CPatAlias of Loc.t * cases_pattern_expr * Id.t | CPatCstr of Loc.t * reference - * cases_pattern_expr list * cases_pattern_expr list - (** [CPatCstr (_, Inl c, l1, l2)] represents (@c l1) l2 *) + * cases_pattern_expr list option * cases_pattern_expr list + (** [CPatCstr (_, c, Some l1, l2)] represents (@c l1) l2 *) | CPatAtom of Loc.t * reference option | CPatOr of Loc.t * cases_pattern_expr list | CPatNotation of Loc.t * notation * cases_pattern_notation_substitution @@ -73,9 +75,15 @@ type constr_expr = | CAppExpl of Loc.t * (proj_flag * reference * instance_expr option) * constr_expr list | CApp of Loc.t * (proj_flag * constr_expr) * (constr_expr * explicitation located option) list - | CRecord of Loc.t * constr_expr option * (reference * constr_expr) list - | CCases of Loc.t * case_style * constr_expr option * - case_expr list * branch_expr list + | CRecord of Loc.t * (reference * constr_expr) list + + (* representation of the "let" and "match" constructs *) + | CCases of Loc.t (* position of the "match" keyword *) + * case_style (* determines whether this value represents "let" or "match" construct *) + * constr_expr option (* return-clause *) + * case_expr list + * branch_expr list (* branches *) + | CLetTuple of Loc.t * Name.t located list * (Name.t located option * constr_expr option) * constr_expr * constr_expr | CIf of Loc.t * constr_expr * (Name.t located option * constr_expr option) @@ -90,8 +98,9 @@ type constr_expr = | CPrim of Loc.t * prim_token | CDelimiters of Loc.t * string * constr_expr -and case_expr = - constr_expr * (Name.t located option * cases_pattern_expr option) +and case_expr = constr_expr (* expression that is being matched *) + * Name.t located option (* as-clause *) + * cases_pattern_expr option (* in-clause *) and branch_expr = Loc.t * cases_pattern_expr list located list * constr_expr @@ -121,7 +130,7 @@ and constr_notation_substitution = constr_expr list list * (** for recursive notations *) local_binder list list (** for binders subexpressions *) -type typeclass_constraint = Name.t located * binding_kind * constr_expr +type typeclass_constraint = (Name.t located * Id.t located list option) * binding_kind * constr_expr and typeclass_context = typeclass_constraint list diff --git a/intf/decl_kinds.mli b/intf/decl_kinds.mli index 6886083c87..6a4e188337 100644 --- a/intf/decl_kinds.mli +++ b/intf/decl_kinds.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli index 38a3e81f44..afc5e3bab9 100644 --- a/intf/evar_kinds.mli +++ b/intf/evar_kinds.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/intf/extend.mli b/intf/extend.mli index ad9706f3a5..10713745e4 100644 --- a/intf/extend.mli +++ b/intf/extend.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -50,3 +50,66 @@ type constr_prod_entry_key = type simple_constr_prod_entry_key = (production_level,unit) constr_entry_key_gen + +(** {5 AST for user-provided entries} *) + +type user_symbol = +| Ulist1 : user_symbol -> user_symbol +| Ulist1sep : user_symbol * string -> user_symbol +| Ulist0 : user_symbol -> user_symbol +| Ulist0sep : user_symbol * string -> user_symbol +| Uopt : user_symbol -> user_symbol +| Uentry : string -> user_symbol +| Uentryl : string * int -> user_symbol + +(** {5 Type-safe grammar extension} *) + +(** (a, b, r) adj => [a = x₁ -> ... xₙ -> r] & [b = x₁ * (... (xₙ * unit))]. *) +type (_, _, _) adj = +| Adj0 : ('r, unit, 'r) adj +| AdjS : ('s, 'b, 'r) adj -> ('a -> 's, 'a * 'b, 'r) adj + +type _ index = +| I0 : 'a -> ('a * 'r) index +| IS : 'a index -> ('b * 'a) index + +(** This type should be marshallable, this is why we use a convoluted + representation in the [Arules] constructor instead of putting a function. *) +type ('self, 'a) symbol = +| Atoken : Tok.t -> ('self, string) symbol +| Alist1 : ('self, 'a) symbol -> ('self, 'a list) symbol +| Alist1sep : ('self, 'a) symbol * string -> ('self, 'a list) symbol +| Alist0 : ('self, 'a) symbol -> ('self, 'a list) symbol +| Alist0sep : ('self, 'a) symbol * string -> ('self, 'a list) symbol +| Aopt : ('self, 'a) symbol -> ('self, 'a option) symbol +| Aself : ('self, 'self) symbol +| Anext : ('self, 'self) symbol +| Aentry : 'a Entry.t -> ('self, 'a) symbol +| Aentryl : 'a Entry.t * int -> ('self, 'a) symbol +| Arules : 'a rules -> ('self, 'a index) symbol + +and ('self, _, 'r) rule = +| Stop : ('self, 'r, 'r) rule +| Next : ('self, 'a, 'r) rule * ('self, 'b) symbol -> ('self, 'b -> 'a, 'r) rule + +and 'a rules = +| Rule0 : unit rules +| RuleS : + ('any, 'act, Loc.t -> Loc.t * 'a) rule * + ('act, 'a, Loc.t -> Loc.t * 'a) adj * + 'b rules -> ((Loc.t * 'a) * 'b) rules + +type 'a production_rule = +| Rule : ('a, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule + +type 'a single_extend_statment = + string option * + (** Level *) + gram_assoc option * + (** Associativity *) + 'a production_rule list + (** Symbol list with the interpretation function *) + +type 'a extend_statment = + gram_position option * + 'a single_extend_statment list diff --git a/intf/genredexpr.mli b/intf/genredexpr.mli index 6134091457..ff036a13f2 100644 --- a/intf/genredexpr.mli +++ b/intf/genredexpr.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/intf/glob_term.mli b/intf/glob_term.mli index 32cf9eaf13..b3159c860c 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -29,9 +29,14 @@ type cases_pattern = | PatCstr of Loc.t * constructor * cases_pattern list * Name.t (** [PatCstr(p,C,l,x)] = "|'C' 'l' as 'x'" *) +(** Representation of an internalized (or in other words globalized) term. *) type glob_constr = | GRef of (Loc.t * global_reference * glob_level list option) + (** An identifier that represents a reference to an object defined + either in the (global) environment or in the (local) context. *) | GVar of (Loc.t * Id.t) + (** An identifier that cannot be regarded as "GRef". + Bound variables are typically represented this way. *) | GEvar of Loc.t * existential_name * (Id.t * glob_constr) list | GPatVar of Loc.t * (bool * patvar) (** Used for patterns only *) | GApp of Loc.t * glob_constr * glob_constr list @@ -39,8 +44,7 @@ type glob_constr = | GProd of Loc.t * Name.t * binding_kind * glob_constr * glob_constr | GLetIn of Loc.t * Name.t * glob_constr * glob_constr | GCases of Loc.t * case_style * glob_constr option * tomatch_tuples * cases_clauses - (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in - [MatchStyle]) *) + (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *) | GLetTuple of Loc.t * Name.t list * (Name.t * glob_constr option) * glob_constr * glob_constr | GIf of Loc.t * glob_constr * (Name.t * glob_constr option) * glob_constr * glob_constr diff --git a/intf/locus.mli b/intf/locus.mli index 808577943e..57b398ab46 100644 --- a/intf/locus.mli +++ b/intf/locus.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/intf/misctypes.mli b/intf/misctypes.mli index 74e136904d..1452bbc347 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -31,7 +31,8 @@ and 'constr intro_pattern_action_expr = | IntroApplyOn of 'constr * (Loc.t * 'constr intro_pattern_expr) | IntroRewrite of bool and 'constr or_and_intro_pattern_expr = - (Loc.t * 'constr intro_pattern_expr) list list + | IntroOrPattern of (Loc.t * 'constr intro_pattern_expr) list list + | IntroAndPattern of (Loc.t * 'constr intro_pattern_expr) list (** Move destination for hypothesis *) @@ -43,9 +44,12 @@ type 'id move_location = (** Sorts *) -type 'a glob_sort_gen = GProp | GSet | GType of 'a -type sort_info = string list -type level_info = string option +type 'a glob_sort_gen = + | GProp (** representation of [Prop] literal *) + | GSet (** representation of [Set] literal *) + | GType of 'a (** representation of [Type] literal *) +type sort_info = string Loc.located list +type level_info = string Loc.located option type glob_sort = sort_info glob_sort_gen type glob_level = level_info glob_sort_gen diff --git a/intf/notation_term.mli b/intf/notation_term.mli index 5a563bf953..39a36310d1 100644 --- a/intf/notation_term.mli +++ b/intf/notation_term.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -61,7 +61,7 @@ type subscopes = tmp_scope_name option * scope_name list (** Type of the meta-variables of an notation_constr: in a recursive pattern x..y, x carries the sequence of objects bound to the list x..y *) type notation_var_instance_type = - | NtnTypeConstr | NtnTypeConstrList | NtnTypeBinderList + | NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList (** Type of variables when interpreting a constr_expr as an notation_constr: in a recursive pattern x..y, both x and y carry the individual type diff --git a/intf/pattern.mli b/intf/pattern.mli index 18cd2df0c4..329ae837e1 100644 --- a/intf/pattern.mli +++ b/intf/pattern.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index ce53680f38..0aa3b936ca 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -119,13 +119,15 @@ type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option type open_constr_expr = unit * constr_expr type open_glob_constr = unit * glob_constr_and_expr +type binding_bound_vars = Id.Set.t type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern -type delayed_open_constr_with_bindings = - Environ.env -> Evd.evar_map -> Evd.evar_map * Term.constr with_bindings +type 'a delayed_open = 'a Pretyping.delayed_open = + { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma } -type delayed_open_constr = - Environ.env -> Evd.evar_map -> Evd.evar_map * Term.constr +type delayed_open_constr_with_bindings = Term.constr with_bindings delayed_open + +type delayed_open_constr = Term.constr delayed_open type intro_pattern = delayed_open_constr intro_pattern_expr located type intro_patterns = delayed_open_constr intro_pattern_expr located list @@ -140,18 +142,15 @@ type 'a gen_atomic_tactic_expr = | TacIntroMove of Id.t option * 'nam move_location | TacExact of 'trm | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list * - (clear_flag * 'nam * 'dtrm intro_pattern_expr located option) option + ('nam * 'dtrm intro_pattern_expr located option) option | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option | TacCase of evars_flag * 'trm with_bindings_arg - | TacFix of Id.t option * int | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list - | TacCofix of Id.t option | TacMutualCofix of Id.t * (Id.t * 'trm) list | TacAssert of bool * 'tacexpr option * 'dtrm intro_pattern_expr located option * 'trm | TacGeneralize of ('trm with_occurrences * Name.t) list - | TacGeneralizeDep of 'trm | TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag * intro_pattern_naming_expr located option @@ -160,26 +159,13 @@ type 'a gen_atomic_tactic_expr = rec_flag * evars_flag * ('trm,'dtrm,'nam) induction_clause_list | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis - (* Automation tactics *) - | TacTrivial of debug * 'trm list * string list option - | TacAuto of debug * int or_var option * 'trm list * string list option - (* Context management *) - | TacClear of bool * 'nam list - | TacClearBody of 'nam list - | TacMove of 'nam * 'nam move_location | TacRename of ('nam *'nam) list - (* Trmuctors *) - | TacSplit of evars_flag * 'trm bindings list - (* Conversion *) | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr | TacChange of 'pat option * 'dtrm * 'nam clause_expr - (* Equivalence relations *) - | TacSymmetry of 'nam clause_expr - (* Equality and inversion *) | TacRewrite of evars_flag * (bool * multi * 'dtrm with_bindings_arg) list * 'nam clause_expr * @@ -194,7 +180,6 @@ type 'a gen_atomic_tactic_expr = constraint 'a = < term:'trm; - utrm: 'utrm; dterm: 'dtrm; pattern:'pat; constant:'cst; @@ -207,11 +192,8 @@ constraint 'a = < (** Possible arguments of a tactic definition *) and 'a gen_tactic_arg = - | TacDynamic of Loc.t * Dyn.t | TacGeneric of 'lev generic_argument - | MetaIdArg of Loc.t * bool * string | ConstrMayEval of ('trm,'cst,'pat) may_eval - | UConstr of 'utrm | Reference of 'ref | TacCall of Loc.t * 'ref * 'a gen_tactic_arg list @@ -222,7 +204,6 @@ and 'a gen_tactic_arg = constraint 'a = < term:'trm; - utrm: 'utrm; dterm: 'dtrm; pattern:'pat; constant:'cst; @@ -295,13 +276,12 @@ and 'a gen_tactic_expr = | TacFun of 'a gen_tactic_fun_ast | TacArg of 'a gen_tactic_arg located (* For ML extensions *) - | TacML of Loc.t * ml_tactic_entry * 'l generic_argument list + | TacML of Loc.t * ml_tactic_entry * 'a gen_tactic_arg list (* For syntax extensions *) - | TacAlias of Loc.t * KerName.t * (Id.t * 'l generic_argument) list + | TacAlias of Loc.t * KerName.t * 'a gen_tactic_arg list constraint 'a = < term:'t; - utrm: 'utrm; dterm: 'dtrm; pattern:'p; constant:'c; @@ -316,7 +296,6 @@ and 'a gen_tactic_fun_ast = constraint 'a = < term:'t; - utrm: 'utrm; dterm: 'dtrm; pattern:'p; constant:'c; @@ -329,15 +308,13 @@ constraint 'a = < (** Globalized tactics *) type g_trm = glob_constr_and_expr -type g_utrm = g_trm -type g_pat = glob_constr_and_expr * constr_pattern +type g_pat = glob_constr_pattern_and_expr type g_cst = evaluable_global_reference and_short_name or_var type g_ref = ltac_constant located or_var type g_nam = Id.t located type g_dispatch = < term:g_trm; - utrm:g_utrm; dterm:g_trm; pattern:g_pat; constant:g_cst; @@ -359,7 +336,6 @@ type glob_tactic_arg = (** Raw tactics *) type r_trm = constr_expr -type r_utrm = r_trm type r_pat = constr_pattern_expr type r_cst = reference or_by_notation type r_ref = reference @@ -368,7 +344,6 @@ type r_lev = rlevel type r_dispatch = < term:r_trm; - utrm:r_utrm; dterm:r_trm; pattern:r_pat; constant:r_cst; @@ -390,7 +365,6 @@ type raw_tactic_arg = (** Interpreted tactics *) type t_trm = Term.constr -type t_utrm = Glob_term.closed_glob_constr type t_pat = constr_pattern type t_cst = evaluable_global_reference type t_ref = ltac_constant located @@ -398,7 +372,6 @@ type t_nam = Id.t type t_dispatch = < term:t_trm; - utrm:t_utrm; dterm:g_trm; pattern:t_pat; constant:t_cst; @@ -421,3 +394,15 @@ type tactic_arg = type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen type glob_red_expr = (g_trm, g_cst, g_pat) red_expr_gen + +(** Traces *) + +type ltac_call_kind = + | LtacMLCall of glob_tactic_expr + | LtacNotationCall of KerName.t + | LtacNameCall of ltac_constant + | LtacAtomCall of glob_atomic_tactic_expr + | LtacVarCall of Id.t * glob_tactic_expr + | LtacConstrInterp of Glob_term.glob_constr * Pretyping.ltac_var_map + +type ltac_trace = (Loc.t * ltac_call_kind) list diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 94e3739d4a..14a80379ec 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -19,7 +19,6 @@ open Libnames type lident = Id.t located type lname = Name.t located type lstring = string located -type lreference = reference type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation @@ -32,7 +31,6 @@ type goal_selector = | SelectNth of int | SelectId of Id.t | SelectAll - | SelectAllParallel type goal_identifier = string type scope_name = string @@ -40,7 +38,8 @@ type scope_name = string type goal_reference = | OpenSubgoals | NthGoal of int - | GoalId of goal_identifier + | GoalId of Id.t + | GoalUid of goal_identifier type printable = | PrintTables @@ -61,7 +60,6 @@ type printable = | PrintClasses | PrintTypeClasses | PrintInstances of reference or_by_notation - | PrintLtac of reference | PrintCoercions | PrintCoercionPaths of class_rawexpr * class_rawexpr | PrintCanonicalConversions @@ -69,7 +67,6 @@ type printable = | PrintHint of reference or_by_notation | PrintHintGoal | PrintHintDbName of string - | PrintRewriteHintDbName of string | PrintHintDb | PrintScopes | PrintScope of string @@ -155,11 +152,15 @@ type option_value = Goptions.option_value = | BoolValue of bool | IntValue of int option | StringValue of string + | StringOptValue of string option type option_ref_value = | StringRefValue of string | QualidRefValue of reference +(** Identifier and optional list of bound universes. *) +type plident = lident * lident list option + type sort_expr = glob_sort type definition_expr = @@ -168,10 +169,10 @@ type definition_expr = * constr_expr option type fixpoint_expr = - Id.t located * (Id.t located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr option + plident * (Id.t located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr option type cofixpoint_expr = - Id.t located * local_binder list * constr_expr * constr_expr option + plident * local_binder list * constr_expr * constr_expr option type local_decl_expr = | AssumExpr of lname * constr_expr @@ -190,15 +191,18 @@ type constructor_list_or_record_decl_expr = | Constructors of constructor_expr list | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list type inductive_expr = - lident with_coercion * local_binder list * constr_expr option * inductive_kind * + plident with_coercion * local_binder list * constr_expr option * inductive_kind * constructor_list_or_record_decl_expr type one_inductive_expr = - lident * local_binder list * constr_expr option * constructor_expr list + plident * local_binder list * constr_expr option * constructor_expr list + +type proof_expr = + plident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option) type grammar_tactic_prod_item_expr = | TacTerm of string - | TacNonTerm of Loc.t * string * (Names.Id.t * string) option + | TacNonTerm of Loc.t * string * (Names.Id.t * string) type syntax_modifier = | SetItemLevel of string list * Extend.production_level @@ -218,12 +222,12 @@ type scheme = | EqualityScheme of reference or_by_notation type section_subset_expr = - | SsSet of lident list + | SsEmpty + | SsSingl of lident | SsCompl of section_subset_expr | SsUnion of section_subset_expr * section_subset_expr | SsSubstr of section_subset_expr * section_subset_expr - -type section_subset_descr = SsAll | SsType | SsExpr of section_subset_expr + | SsFwdClose of section_subset_expr (** Extension identifiers for the VERNAC EXTEND mechanism. *) type extend_name = @@ -279,15 +283,13 @@ type module_binder = bool option * lident list * module_ast_inl type vernac_expr = (* Control *) | VernacLoad of verbose_flag * string - | VernacTime of vernac_list - | VernacRedirect of string * vernac_list + | VernacTime of vernac_expr located + | VernacRedirect of string * vernac_expr located | VernacTimeout of int * vernac_expr | VernacFail of vernac_expr | VernacError of exn (* always fails *) (* Syntax *) - | VernacTacticNotation of - int * grammar_tactic_prod_item_expr list * raw_tactic_expr | VernacSyntaxExtension of obsolete_locality * (lstring * syntax_modifier list) | VernacOpenCloseScope of obsolete_locality * (bool * scope_name) @@ -302,14 +304,12 @@ type vernac_expr = (* Gallina *) | VernacDefinition of - (locality option * definition_object_kind) * lident * definition_expr - | VernacStartTheoremProof of theorem_kind * - (lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)) list * - bool + (locality option * definition_object_kind) * plident * definition_expr + | VernacStartTheoremProof of theorem_kind * proof_expr list * bool | VernacEndProof of proof_end | VernacExactProof of constr_expr | VernacAssumption of (locality option * assumption_object_kind) * - inline * simple_binder with_coercion list + inline * (plident list * constr_expr) with_coercion list | VernacInductive of private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of locality option * (fixpoint_expr * decl_notation list) list @@ -324,14 +324,14 @@ type vernac_expr = | VernacBeginSection of lident | VernacEndSegment of lident | VernacRequire of - lreference option * export_flag option * lreference list - | VernacImport of export_flag * lreference list + reference option * export_flag option * reference list + | VernacImport of export_flag * reference list | VernacCanonical of reference or_by_notation | VernacCoercion of obsolete_locality * reference or_by_notation * class_rawexpr * class_rawexpr | VernacIdentityCoercion of obsolete_locality * lident * class_rawexpr * class_rawexpr - | VernacNameSectionHypSet of lident * section_subset_descr + | VernacNameSectionHypSet of lident * section_subset_expr (* Type classes *) | VernacInstance of @@ -359,7 +359,6 @@ type vernac_expr = (* Solving *) - | VernacSolve of goal_selector * int option * raw_tactic_expr * bool | VernacSolveExistential of int * constr_expr (* Auxiliary file and library management *) @@ -380,8 +379,6 @@ type vernac_expr = | VernacBackTo of int (* Commands *) - | VernacDeclareTacticDefinition of - (rec_flag * (reference * bool * raw_tactic_expr) list) | VernacCreateHintDb of string * bool | VernacRemoveHints of string list * reference list | VernacHints of obsolete_locality * string list * hints_expr @@ -415,7 +412,6 @@ type vernac_expr = | VernacLocate of locatable | VernacRegister of lident * register_kind | VernacComments of comment list - | VernacNop (* Stm backdoor *) | VernacStm of vernac_expr stm_vernac @@ -436,7 +432,7 @@ type vernac_expr = | VernacEndSubproof | VernacShow of showable | VernacCheckGuard - | VernacProof of raw_tactic_expr option * section_subset_descr option + | VernacProof of raw_tactic_expr option * section_subset_expr option | VernacProofMode of string (* Toplevel control *) | VernacToplevelControl of exn @@ -449,9 +445,9 @@ type vernac_expr = | VernacPolymorphic of bool * vernac_expr | VernacLocal of bool * vernac_expr -and vernac_list = located_vernac_expr list - -and located_vernac_expr = Loc.t * vernac_expr +and tacdef_body = + | TacticDefinition of Id.t Loc.located * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) + | TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) (* A vernac classifier has to tell if a command: vernac_when: has to be executed now (alters the parser) or later |