diff options
Diffstat (limited to 'pretyping/rawterm.mli')
| -rw-r--r-- | pretyping/rawterm.mli | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 440d9ed442..8c93eecd9f 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -11,10 +11,11 @@ open Type_errors type loc = int * int -type pattern = (* locs here refers to the ident's location, not whole pat *) +(* locs here refers to the ident's location, not whole pat *) +(* the last argument of PatCstr is a possible alias ident for the pattern *) +type pattern = | PatVar of loc * name - | PatCstr of loc * (constructor_path * identifier list) * pattern list - | PatAs of loc * identifier * pattern + | PatCstr of loc * (constructor_path * identifier list) * pattern list * name type binder_kind = BProd | BLambda type fix_kind = RFix of int array * int | RCofix of int @@ -56,3 +57,6 @@ type rawconstr = - boolean in POldCase means it is recursive - option in PHole tell if the "?" was apparent or has been implicitely added i*) + +val dummy_loc : loc +val loc_of_rawconstr : rawconstr -> loc |