diff options
Diffstat (limited to 'pretyping/rawterm.mli')
| -rw-r--r-- | pretyping/rawterm.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 336b3ffa1..8d5184299 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -12,6 +12,7 @@ open Names open Sign open Term +open Nametab (*i*) (* Untyped intermediate terms, after ASTs and before constr. *) @@ -26,6 +27,8 @@ type cases_pattern = type rawsort = RProp of Term.contents | RType of Univ.universe option +type fix_kind = RFix of (int array * int) | RCoFix of int + type binder_kind = BProd | BLambda | BLetIn type 'ctxt reference = |