diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index b310dd645..90e4582fa 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2844,7 +2844,7 @@ let subst_md (subst,(local,defs)) = let classify_md (local,defs as o) = if local then Dispose else Substitute o -let inMD = +let inMD : bool * (tacdef_kind * glob_tactic_expr) list -> obj = declare_object {(default_object "TAC-DEFINITION") with cache_function = cache_md; load_function = load_md; |