diff options
| author | filliatr | 2000-11-15 07:56:21 +0000 |
|---|---|---|
| committer | filliatr | 2000-11-15 07:56:21 +0000 |
| commit | b2c9129662f55eea46a8937f9fd0cfabc029457a (patch) | |
| tree | fb3cb41fe45c41b58149559228088607621c8007 /pretyping | |
| 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 'pretyping')
| -rwxr-xr-x | pretyping/classops.ml | 4 | ||||
| -rwxr-xr-x | pretyping/recordops.ml | 6 | ||||
| -rw-r--r-- | pretyping/syntax_def.ml | 2 |
3 files changed, 6 insertions, 6 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index b4274e9fe9..306f2b8ce2 100755 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -173,7 +173,7 @@ let (inClass,outClass) = { load_function = (fun _ -> ()); open_function = cache_class; cache_function = cache_class; - specification_function = (function x -> x) }) + export_function = (function x -> Some x) }) let add_new_class (cl,s,stre,p) = Lib.add_anonymous_leaf (inClass ((cl,{cL_STR=s;cL_STRE=stre;cL_PARAM=p}))) @@ -324,4 +324,4 @@ let (inCoercion,outCoercion) = { load_function = (fun _ -> ()); open_function = cache_coercion; cache_function = cache_coercion; - specification_function = (function x -> x) }) + export_function = (function x -> Some x) }) diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index b3b0af4634..45b16c935e 100755 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -38,7 +38,7 @@ let (inStruc,outStruc) = { load_function = (fun _ -> ()); cache_function = cache_structure; open_function = cache_structure; - specification_function = (function x -> x) }) + export_function = (function x -> Some x) }) let add_new_struc (s,c,n,l) = Lib.add_anonymous_leaf (inStruc (s,{s_CONST=c;s_PARAM=n;s_PROJ=l})) @@ -72,7 +72,7 @@ let (inObjDef,outObjDef) = { load_function = (fun _ -> ()); open_function = cache_obj; cache_function = cache_obj; - specification_function = (function x -> x)}) + export_function = (function x -> Some x)}) let add_new_objdef (o,c,la,lp,l) = try @@ -88,7 +88,7 @@ let ((inObjDef1 : section_path -> obj),(outObjDef1 : obj -> section_path)) = { load_function = (fun _ -> ()); open_function = cache_objdef1; cache_function = cache_objdef1; - specification_function = (function x -> x)}) + export_function = (function x -> Some x)}) let objdef_info o = List.assoc o !oBJDEFS diff --git a/pretyping/syntax_def.ml b/pretyping/syntax_def.ml index 736a2be67f..00ed971c1a 100644 --- a/pretyping/syntax_def.ml +++ b/pretyping/syntax_def.ml @@ -31,7 +31,7 @@ let (in_syntax_constant, out_syntax_constant) = cache_function = cache_syntax_constant; load_function = (fun _ -> ()); open_function = cache_syntax_constant; - specification_function = (fun x -> x) } + export_function = (fun x -> Some x) } in declare_object ("SYNTAXCONSTANT", od) |