More abstraction in cases.mli.

1 files changed, 0 insertions, 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
-