diff options
Diffstat (limited to 'pretyping/cases.mli')
| -rw-r--r-- | pretyping/cases.mli | 30 |
1 files changed, 8 insertions, 22 deletions
diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 2711276a..f773da0e 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -1,24 +1,23 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: cases.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Util open Names open Term open Evd open Environ open Inductiveops -open Rawterm +open Glob_term open Evarutil -(*i*) +(** {5 Compilation of pattern-matching } *) + +(** {6 Pattern-matching errors } *) type pattern_matching_error = | BadPattern of constructor * constr | BadConstructor of constructor * inductive @@ -46,27 +45,14 @@ 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 +(** {6 Compilation primitive. } *) module type S = sig val compile_cases : loc -> case_style -> - (type_constraint -> env -> evar_map ref -> rawconstr -> unsafe_judgment) * evar_map ref -> + (type_constraint -> env -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref -> type_constraint -> - env -> rawconstr option * tomatch_tuples * cases_clauses -> + env -> glob_constr option * tomatch_tuples * cases_clauses -> unsafe_judgment end |