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 edbf9fb62a..d7634d6e09 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -47,6 +47,8 @@ type full_implicits_env = identifier list * implicits_env type ltac_sign = identifier list * unbound_ltac_var_map +val insert_maximal_implicit : bool ref + (*s Internalisation performs interpretation of global names and notations *) val intern_constr : evar_map -> env -> constr_expr -> rawconstr |