diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/subtac/subtac_classes.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml index 6fe14da34d..93b65cd000 100644 --- a/plugins/subtac/subtac_classes.ml +++ b/plugins/subtac/subtac_classes.ml @@ -95,7 +95,7 @@ let substitution_of_constrs ctx cstrs = let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) pri = let env = Global.env() in let isevars = ref Evd.empty in - let tclass = + let tclass, _ = match bk with | Implicit -> Implicit_quantifiers.implicit_application Idset.empty (* need no avoid *) @@ -110,7 +110,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p in t, avoid | None -> failwith ("new instance: under-applied typeclass")) cl - | Explicit -> cl + | Explicit -> cl, Idset.empty in let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in let k, ctx', imps, subst = |