diff options
| author | herbelin | 2003-09-26 15:34:50 +0000 |
|---|---|---|
| committer | herbelin | 2003-09-26 15:34:50 +0000 |
| commit | 0ddfbbd940b47b133cfc9daf3c657a32c02e14ba (patch) | |
| tree | d4fc10b40f91c314e39426881f5318ea2b3c5965 /interp/topconstr.mli | |
| parent | ee4b850b8a165dc80016204ba2711dcf68a58676 (diff) | |
Syntaxe plus liberale pour le type des arguments de filtrage du 'match'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4491 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/topconstr.mli')
| -rw-r--r-- | interp/topconstr.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/interp/topconstr.mli b/interp/topconstr.mli index a4b20b65ca..3d9def4dd9 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -86,7 +86,7 @@ type constr_expr = | CApp of loc * (proj_flag * constr_expr) * (constr_expr * explicitation located option) list | CCases of loc * (constr_expr option * constr_expr option) * - (constr_expr * (name * (loc * reference * name list) option)) list * + (constr_expr * (name * constr_expr option)) list * (loc * cases_pattern_expr list * constr_expr) list | COrderedCase of loc * case_style * constr_expr option * constr_expr * constr_expr list @@ -117,6 +117,9 @@ val replace_vars_constr_expr : val occur_var_constr_expr : identifier -> constr_expr -> bool +(* Specific function for interning "in indtype" syntax of "match" *) +val names_of_cases_indtype : constr_expr -> identifier list + val mkIdentC : identifier -> constr_expr val mkRefC : reference -> constr_expr val mkAppC : constr_expr * constr_expr list -> constr_expr |