diff options
Diffstat (limited to 'pretyping/rawterm.mli')
| -rw-r--r-- | pretyping/rawterm.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index d6543323e..e8b0726c9 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -12,6 +12,7 @@ open Names open Sign open Term +open Libnames open Nametab (*i*) @@ -57,7 +58,7 @@ type 'ctxt reference = | REVar of int * 'ctxt type rawconstr = - | RRef of loc * global_reference + | RRef of loc * Libnames.global_reference | RVar of loc * identifier | REvar of loc * existential_key | RMeta of loc * int @@ -93,6 +94,8 @@ val loc_of_rawconstr : rawconstr -> loc val set_loc_of_rawconstr : loc -> rawconstr -> rawconstr val join_loc : loc -> loc -> loc +val subst_raw : Names.substitution -> rawconstr -> rawconstr + type 'a raw_red_flag = { rBeta : bool; rIota : bool; |