diff options
Diffstat (limited to 'library/declare.ml')
| -rw-r--r-- | library/declare.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/declare.ml b/library/declare.ml index a973e6a55..0cd1250c7 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -141,7 +141,7 @@ 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 classify_constant cst = Substitute (dummy_constant cst) let (inConstant,_) = declare_object { (default_object "CONSTANT") with @@ -267,7 +267,7 @@ let (inInductive,_) = cache_function = cache_inductive; load_function = load_inductive; open_function = open_inductive; - classify_function = (fun (_,a) -> Substitute (dummy_inductive_entry a)); + classify_function = (fun a -> Substitute (dummy_inductive_entry a)); subst_function = ident_subst_function; discharge_function = discharge_inductive; export_function = export_inductive } |