From 975e2a05050c704161aca3fbac96376eeda6fb4a Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 26 Apr 2016 13:34:39 +0200 Subject: More abstraction in cases.mli. --- pretyping/cases.mli | 69 ----------------------------------------------------- 1 file changed, 69 deletions(-) diff --git a/pretyping/cases.mli b/pretyping/cases.mli index d7fff8af4..07679567d 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -53,72 +53,3 @@ val constr_of_pat : (Context.Rel.Declaration.t list * Term.constr * (Term.types * Term.constr list) * Glob_term.cases_pattern) * Names.Id.t list - -type 'a rhs = - { rhs_env : env; - rhs_vars : Id.t list; - avoid_ids : Id.t list; - it : 'a option} - -type 'a equation = - { patterns : cases_pattern list; - rhs : 'a rhs; - alias_stack : Name.t list; - eqn_loc : Loc.t; - used : bool ref } - -type 'a matrix = 'a equation list - -(* 1st argument of IsInd is the original ind before extracting the summary *) -type tomatch_type = - | IsInd of types * inductive_type * Name.t list - | NotInd of constr option * types - -(* spiwack: The first argument of [Pushed] is [true] for initial - Pushed and [false] otherwise. Used to decide whether the term being - matched on must be aliased in the variable case (only initial - Pushed need to be aliased). The first argument of [Alias] is [true] - if the alias was introduced by an initial pushed and [false] - otherwise.*) -type tomatch_status = - | Pushed of (bool*((constr * tomatch_type) * int list * Name.t)) - | Alias of (bool * (Name.t * constr * (constr * types))) - | NonDepAlias - | Abstract of int * Context.Rel.Declaration.t - -type tomatch_stack = tomatch_status list - -(* We keep a constr for aliases and a cases_pattern for error message *) - -type pattern_history = - | Top - | MakeConstructor of constructor * pattern_continuation - -and pattern_continuation = - | Continuation of int * cases_pattern list * pattern_history - | Result of cases_pattern list - -type 'a pattern_matching_problem = - { env : env; - evdref : evar_map ref; - pred : constr; - tomatch : tomatch_stack; - history : pattern_continuation; - mat : 'a matrix; - caseloc : Loc.t; - casestyle : case_style; - typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment } - - -val compile : 'a pattern_matching_problem -> Environ.unsafe_judgment - -val prepare_predicate : Loc.t -> - (Evarutil.type_constraint -> - Environ.env -> Evd.evar_map ref -> 'a -> Environ.unsafe_judgment) -> - Environ.env -> - Evd.evar_map -> - (Term.types * tomatch_type) list -> - Context.Rel.t list -> - Constr.constr option -> - 'a option -> (Evd.evar_map * Names.name list * Term.constr) list - -- cgit v1.2.3