diff options
Diffstat (limited to 'pretyping/cases.mli')
| -rw-r--r-- | pretyping/cases.mli | 21 |
1 files changed, 17 insertions, 4 deletions
diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 30f68083..98923b2a 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: cases.mli 9976 2007-07-12 11:58:30Z msozeau $ i*) +(*i $Id: cases.mli 11014 2008-05-28 19:09:32Z herbelin $ i*) (*i*) open Util @@ -46,14 +46,27 @@ val error_wrong_predicate_arity_loc : loc -> env -> constr -> constr -> constr - val error_needs_inversion : env -> constr -> types -> 'a +val set_impossible_default_clause : constr * types -> unit (*s Compilation of pattern-matching. *) +type alias_constr = + | DepAlias + | NonDepAlias +type dep_status = KnownDep | KnownNotDep | DepUnknown +type tomatch_type = + | IsInd of types * inductive_type * name list + | NotInd of constr option * types +type tomatch_status = + | Pushed of ((constr * tomatch_type) * int list * (name * dep_status)) + | Alias of (constr * constr * alias_constr * constr) + | Abstract of rel_declaration + module type S = sig val compile_cases : - loc -> - (type_constraint -> env -> rawconstr -> unsafe_judgment) * evar_defs ref -> + loc -> case_style -> + (type_constraint -> env -> evar_defs ref -> rawconstr -> unsafe_judgment) * evar_defs ref -> type_constraint -> - env -> rawconstr option * tomatch_tuple * cases_clauses -> + env -> rawconstr option * tomatch_tuples * cases_clauses -> unsafe_judgment end |