diff options
| author | msozeau | 2009-10-09 22:21:30 +0000 |
|---|---|---|
| committer | msozeau | 2009-10-09 22:21:30 +0000 |
| commit | 562c684cd19c37e04901743c73933ea12148940b (patch) | |
| tree | 7257cade7643acce2e3080d5b289960ec6559167 /plugins | |
| parent | fa8272263e70535dc8db3c5e296c3635bf4139de (diff) | |
Fix bug #2162 and a name clashing bug in generalized binders.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12383 85f007b7-540e-0410-9357-904b9bb8a0f7
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 = |