diff options
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index ce8c6f5ee..8666db633 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -80,6 +80,8 @@ val interp_constrpattern_gen : val interp_constrpattern : evar_map -> env -> constr_expr -> int list * constr_pattern +val interp_reference : identifier list -> reference -> rawconstr + (* Interprets into a abbreviatable constr *) val interp_aconstr : constr_expr -> aconstr |