diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-15 07:56:21 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-15 07:56:21 +0000 |
| commit | b2c9129662f55eea46a8937f9fd0cfabc029457a (patch) | |
| tree | fb3cb41fe45c41b58149559228088607621c8007 /proofs | |
| parent | e4639721323887555d278b963b84b11244871632 (diff) | |
methode export
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@851 85f007b7-540e-0410-9357-904b9bb8a0f7
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 92cc8cf41..4a7a826f9 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 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 = |