diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/macros.ml | 4 | ||||
| -rw-r--r-- | proofs/tacinterp.ml | 8 |
2 files changed, 6 insertions, 6 deletions
diff --git a/proofs/macros.ml b/proofs/macros.ml index 92cc8cf41c..4a7a826f96 100644 --- a/proofs/macros.ml +++ b/proofs/macros.ml @@ -39,12 +39,12 @@ let _ = let (inMD,outMD) = let add (na,md) = mactab := Stringmap.add na md !mactab in let cache_md (_,(na,md)) = add (na,md) in - let specification_md x = x in + let export_md x = Some x in declare_object ("TACTIC-MACRO-DATA", { cache_function = cache_md; load_function = (fun _ -> ()); open_function = cache_md; - specification_function = specification_md }) + export_function = export_md }) let add_macro_hint na (ids,body) = if Stringmap.mem na !mactab then errorlabstrm "add_macro_hint" diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index 72593da368..f45d896d45 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 = |