Revert "More abstraction in cases.mli."

This reverts commit 975e2a05050c704161aca3fbac96376eeda6fb4a.

1 files changed, 69 insertions, 0 deletions

diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 07679567d..d7fff8af4 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -53,3 +53,72 @@ 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
+