diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 8e55d4f5c..8d8b94c6c 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2836,8 +2836,7 @@ let (inMD,outMD) = load_function = load_md; open_function = open_md; subst_function = subst_md; - classify_function = (fun o -> Substitute o); - export_function = (fun x -> Some x)} + classify_function = (fun o -> Substitute o)} let print_ltac id = try |