diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-06-01 20:44:16 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-06-01 20:44:16 +0000 |
| commit | 5139432d6087f49ef549d8375a1a61db56f86dd1 (patch) | |
| tree | 5d49a28094c8ae88b21737946f93174318a87cb3 /pretyping/cases.mli | |
| parent | e563ed5bf7681b910e36d2dc4ea99406da940cec (diff) | |
Mise en place d'un choix constr/typed_type en remplacement de certains Cast
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@484 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/cases.mli')
| -rw-r--r-- | pretyping/cases.mli | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/pretyping/cases.mli b/pretyping/cases.mli index fbf77e402..2beb7441c 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -14,7 +14,18 @@ open Evarutil (* Used for old cases in pretyping *) val branch_scheme : - env -> 'a evar_defs -> bool -> int -> inductive_family -> constr + env -> 'a evar_defs -> bool -> inductive_family -> constr array + +val pred_case_ml_onebranch : env -> 'c evar_map -> bool -> + inductive_type -> int * constr * constr -> constr + +(*i Utilisés dans Program +val pred_case_ml : env -> 'c evar_map -> bool -> + constr * (inductive * constr list * constr list) + -> constr array -> int * constr ->constr +val make_case_ml : + bool -> constr -> constr -> case_info -> constr array -> constr +i*) (* Compilation of pattern-matching. *) |