diff options
Diffstat (limited to 'proofs/tacinterp.ml')
| -rw-r--r-- | proofs/tacinterp.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index 72593da36..f45d896d4 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -944,10 +944,10 @@ let (inMD,outMD) = let ve=val_interp (Evd.empty,Environ.empty_env,[],[],None,get_debug ()) td in add (na,ve) in declare_object ("TACTIC-DEFINITION", - {cache_function = cache_md; - load_function = (fun _ -> ()); - open_function = cache_md; - specification_function = (fun x -> x)}) + {cache_function = cache_md; + load_function = (fun _ -> ()); + open_function = cache_md; + export_function = (fun x -> Some x)}) (* Adds a Tactic Definition in the table *) let add_tacdef na vbody = |