diff options
Diffstat (limited to 'library/declare.ml')
| -rw-r--r-- | library/declare.ml | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/library/declare.ml b/library/declare.ml index 49b7d7ba2..da723aa4b 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -138,8 +138,6 @@ let dummy_constant_entry = ConstantEntry (ParameterEntry (mkProp,false)) let dummy_constant (ce,_,mk) = dummy_constant_entry,[],mk -let export_constant cst = Some (dummy_constant cst) - let classify_constant cst = Substitute (dummy_constant cst) let (inConstant,_) = @@ -149,8 +147,7 @@ let (inConstant,_) = open_function = open_constant; classify_function = classify_constant; subst_function = ident_subst_function; - discharge_function = discharge_constant; - export_function = export_constant } + discharge_function = discharge_constant } let hcons_constant_declaration = function | DefinitionEntry ce when !Flags.hash_cons_proofs -> @@ -259,8 +256,6 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_finite = true; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds }) -let export_inductive x = Some (dummy_inductive_entry x) - let (inInductive,_) = declare_object {(default_object "INDUCTIVE") with cache_function = cache_inductive; @@ -268,8 +263,7 @@ let (inInductive,_) = open_function = open_inductive; classify_function = (fun a -> Substitute (dummy_inductive_entry a)); subst_function = ident_subst_function; - discharge_function = discharge_inductive; - export_function = export_inductive } + discharge_function = discharge_inductive } (* for initial declaration *) let declare_mind isrecord mie = |