diff options
Diffstat (limited to 'pretyping/rawterm.mli')
| -rw-r--r-- | pretyping/rawterm.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index f78520a16f..5f67a8a927 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -32,7 +32,7 @@ type 'ctxt reference = | RMeta of int type rawconstr = - | RRef of loc * rawconstr array reference + | RRef of loc * Term.constr array reference | RApp of loc * rawconstr * rawconstr list | RBinder of loc * binder_kind * name * rawconstr * rawconstr | RCases of loc * Term.case_style * rawconstr option * rawconstr list * @@ -61,7 +61,7 @@ val dummy_loc : loc val loc_of_rawconstr : rawconstr -> loc type constr_pattern = - | PRef of constr_pattern array reference + | PRef of Term.constr array reference | PRel of int | PApp of constr_pattern * constr_pattern array | PSoApp of int * int list |