diff options
Diffstat (limited to 'pretyping/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index d286b98e83..0b8cbff36c 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -838,3 +838,8 @@ let subterm_source evk (loc,k) = | Evar_kinds.SubEvar (evk) -> evk | _ -> evk in (loc,Evar_kinds.SubEvar evk) + + +(** Term exploration up to isntantiation. *) +let kind_of_term_upto sigma t = + Constr.kind (Reductionops.whd_evar sigma t) |