diff options
Diffstat (limited to 'pretyping/classops.ml')
| -rw-r--r-- | pretyping/classops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 911ded641..901341e7b 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -384,7 +384,7 @@ let (inCoercion,_) = load_function = load_coercion; cache_function = cache_coercion; subst_function = subst_coercion; - classify_function = (fun (_,x) -> Substitute x); + classify_function = (fun x -> Substitute x); discharge_function = discharge_coercion; export_function = (function x -> Some x) } |