diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-01-16 14:03:05 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-01-16 14:03:05 +0000 |
| commit | 655f6a6305812d3f95d27f5579e119523ae3bef0 (patch) | |
| tree | 0bc3e45faeea4fe18c388aa69e2722dc600b1e2a /pretyping/detyping.mli | |
| parent | 58529cf2252bf6ae386a45c8587bdc9b3285c1c5 (diff) | |
Version préliminaire d'inversion de la compilation du filtrage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7881 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/detyping.mli')
| -rw-r--r-- | pretyping/detyping.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 2a16b9e7e..71aed9373 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -32,8 +32,9 @@ val detype : bool -> identifier list -> names_context -> constr -> rawconstr val detype_case : bool -> ('a -> rawconstr) -> - (constructor -> int -> 'a -> loc * identifier list * cases_pattern list * - rawconstr) -> ('a -> int -> bool) -> + (constructor array -> int array -> 'a array -> + (loc * identifier list * cases_pattern list * rawconstr) list) -> + ('a -> int -> bool) -> identifier list -> inductive * case_style * int * int array * int -> 'a option -> 'a -> 'a array -> rawconstr |