diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/constrexpr.ml | 2 | ||||
| -rw-r--r-- | intf/glob_term.ml | 2 | ||||
| -rw-r--r-- | intf/intf.mllib | 1 | ||||
| -rw-r--r-- | intf/misctypes.ml | 3 | ||||
| -rw-r--r-- | intf/notation_term.ml | 2 | ||||
| -rw-r--r-- | intf/pattern.ml | 4 | ||||
| -rw-r--r-- | intf/tactypes.ml | 33 |
7 files changed, 7 insertions, 40 deletions
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml index 8eadafe667..e0d2d7bf48 100644 --- a/intf/constrexpr.ml +++ b/intf/constrexpr.ml @@ -79,7 +79,7 @@ and constr_expr_r = | CRecord of (reference * constr_expr) list (* representation of the "let" and "match" constructs *) - | CCases of case_style (* determines whether this value represents "let" or "match" construct *) + | CCases of Constr.case_style (* determines whether this value represents "let" or "match" construct *) * constr_expr option (* return-clause *) * case_expr list * branch_expr list (* branches *) diff --git a/intf/glob_term.ml b/intf/glob_term.ml index 508990a580..72c91db6a0 100644 --- a/intf/glob_term.ml +++ b/intf/glob_term.ml @@ -46,7 +46,7 @@ type 'a glob_constr_r = | GLambda of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g | GProd of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g | GLetIn of Name.t * 'a glob_constr_g * 'a glob_constr_g option * 'a glob_constr_g - | GCases of case_style * 'a glob_constr_g option * 'a tomatch_tuples_g * 'a cases_clauses_g + | GCases of Constr.case_style * 'a glob_constr_g option * 'a tomatch_tuples_g * 'a cases_clauses_g (** [GCases(style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *) | GLetTuple of Name.t list * (Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g | GIf of 'a glob_constr_g * (Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g diff --git a/intf/intf.mllib b/intf/intf.mllib index 523e4b2650..38a2a71cc0 100644 --- a/intf/intf.mllib +++ b/intf/intf.mllib @@ -3,7 +3,6 @@ Evar_kinds Genredexpr Locus Notation_term -Tactypes Decl_kinds Extend Glob_term diff --git a/intf/misctypes.ml b/intf/misctypes.ml index 8b70731432..87484ccd50 100644 --- a/intf/misctypes.ml +++ b/intf/misctypes.ml @@ -61,12 +61,13 @@ type existential_key = Evar.t (** Case style, shared with Term *) -type case_style = Term.case_style = +type case_style = Constr.case_style = | LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle (** infer printing form from number of constructor *) +[@@ocaml.deprecated "Alias for Constr.case_style"] (** Casts *) diff --git a/intf/notation_term.ml b/intf/notation_term.ml index c342da3dca..7823d3febb 100644 --- a/intf/notation_term.ml +++ b/intf/notation_term.ml @@ -31,7 +31,7 @@ type notation_constr = | NProd of Name.t * notation_constr * notation_constr | NBinderList of Id.t * Id.t * notation_constr * notation_constr | NLetIn of Name.t * notation_constr * notation_constr option * notation_constr - | NCases of case_style * notation_constr option * + | NCases of Constr.case_style * notation_constr option * (notation_constr * (Name.t * (inductive * Name.t list) option)) list * (cases_pattern list * notation_constr) list | NLetTuple of Name.t list * (Name.t * notation_constr option) * diff --git a/intf/pattern.ml b/intf/pattern.ml index 16c4807355..20636accfa 100644 --- a/intf/pattern.ml +++ b/intf/pattern.ml @@ -8,13 +8,13 @@ open Names open Globnames -open Term +open Constr open Misctypes (** {5 Patterns} *) type case_info_pattern = - { cip_style : case_style; + { cip_style : Constr.case_style; cip_ind : inductive option; cip_ind_tags : bool list option; (** indicates LetIn/Lambda in arity *) cip_extensible : bool (** does this match end with _ => _ ? *) } diff --git a/intf/tactypes.ml b/intf/tactypes.ml deleted file mode 100644 index 2c42e13110..0000000000 --- a/intf/tactypes.ml +++ /dev/null @@ -1,33 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <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 *) -(************************************************************************) - -(** Tactic-related types that are not totally Ltac specific and still used in - lower API. It's not clear whether this is a temporary API or if this is - meant to stay. *) - -open Loc -open Names -open Constrexpr -open Pattern -open Misctypes - -(** In globalize tactics, we need to keep the initial [constr_expr] to recompute - in the environment by the effective calls to Intro, Inversion, etc - The [constr_expr] field is [None] in TacDef though *) -type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option -type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * constr_pattern - -type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a - -type delayed_open_constr = EConstr.constr delayed_open -type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open - -type intro_pattern = delayed_open_constr intro_pattern_expr located -type intro_patterns = delayed_open_constr intro_pattern_expr located list -type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr located -type intro_pattern_naming = intro_pattern_naming_expr located |