diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/constrexpr.mli | 2 | ||||
| -rw-r--r-- | intf/tactypes.mli | 1 | ||||
| -rw-r--r-- | intf/vernacexpr.mli | 9 |
3 files changed, 5 insertions, 7 deletions
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index 49bafadc8e..a4a6eb9092 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -19,7 +19,7 @@ open Decl_kinds type notation = string type explicitation = - | ExplByPos of int * Id.t option + | ExplByPos of int * Id.t option (* a reference to the n-th product starting from left *) | ExplByName of Id.t type binder_kind = diff --git a/intf/tactypes.mli b/intf/tactypes.mli index 02cfc44e29..ef90b911c5 100644 --- a/intf/tactypes.mli +++ b/intf/tactypes.mli @@ -13,7 +13,6 @@ open Loc open Names open Constrexpr -open Glob_term open Pattern open Misctypes diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 25d3c705f4..cb093d85d5 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -71,7 +71,7 @@ type printable = | PrintScopes | PrintScope of string | PrintVisibility of string option - | PrintAbout of reference or_by_notation*int option + | PrintAbout of reference or_by_notation * goal_selector option | PrintImplicit of reference or_by_notation | PrintAssumptions of bool * bool * reference or_by_notation | PrintStrategy of reference or_by_notation option @@ -209,7 +209,7 @@ type one_inductive_expr = plident * local_binder_expr list * constr_expr option * constructor_expr list type proof_expr = - plident option * (local_binder_expr list * constr_expr * (lident option * recursion_order_expr) option) + plident option * (local_binder_expr list * constr_expr) type syntax_modifier = | SetItemLevel of string list * Extend.production_level @@ -316,7 +316,6 @@ type vernac_expr = | VernacRedirect of string * vernac_expr located | VernacTimeout of int * vernac_expr | VernacFail of vernac_expr - | VernacError of exn (* always fails *) (* Syntax *) | VernacSyntaxExtension of @@ -436,11 +435,11 @@ type vernac_expr = | VernacRemoveOption of Goptions.option_name * option_ref_value list | VernacMemOption of Goptions.option_name * option_ref_value list | VernacPrintOption of Goptions.option_name - | VernacCheckMayEval of Genredexpr.raw_red_expr option * int option * constr_expr + | VernacCheckMayEval of Genredexpr.raw_red_expr option * goal_selector option * constr_expr | VernacGlobalCheck of constr_expr | VernacDeclareReduction of string * Genredexpr.raw_red_expr | VernacPrint of printable - | VernacSearch of searchable * int option * search_restriction + | VernacSearch of searchable * goal_selector option * search_restriction | VernacLocate of locatable | VernacRegister of lident * register_kind | VernacComments of comment list |