diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 25fabac03e..d6332c553c 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -25,10 +25,10 @@ val make_clenv_binding_apply : val type_clenv_binding : walking_constraints -> constr * constr -> constr substitution -> constr +(*i (* [force_reference c] fails if [c] is not a reference *) -(* val force_reference : constr -> constr -*) +i*) val string_head : constr -> string val head_constr : constr -> constr list |