diff options
Diffstat (limited to 'pretyping/typeclasses.ml')
| -rw-r--r-- | pretyping/typeclasses.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 2f2796f1c..52e2eb24e 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -168,7 +168,7 @@ let (class_input,class_output) = cache_function = cache_class; load_function = (fun _ -> load_class); open_function = (fun _ -> load_class); - classify_function = (fun (_,x) -> Substitute x); + classify_function = (fun x -> Substitute x); discharge_function = (fun a -> Some (discharge_class a)); rebuild_function = rebuild_class; subst_function = subst_class; @@ -212,7 +212,7 @@ let (instance_input,instance_output) = cache_function = cache_instance; load_function = (fun _ -> load_instance); open_function = (fun _ -> load_instance); - classify_function = (fun (_,x) -> Substitute x); + classify_function = (fun x -> Substitute x); discharge_function = (fun a -> Some (discharge_instance a)); rebuild_function = rebuild_instance; subst_function = subst_instance; |