diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/subtac/subtac_classes.ml | 4 | ||||
| -rw-r--r-- | contrib/subtac/subtac_pretyping_F.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml index 28fc7e2906..cf9c90e17e 100644 --- a/contrib/subtac/subtac_classes.ml +++ b/contrib/subtac/subtac_classes.ml @@ -147,7 +147,9 @@ let new_instance ctx (instid, bk, cl) props = App (c, args) -> let cl = Option.get (class_of_constr c) in cl, ctx, substitution_of_constrs (List.map snd cl.cl_context) (List.rev (Array.to_list args)) - | _ -> assert false) + | _ -> + let cl = Option.get (class_of_constr c) in + cl, ctx, []) in let env' = Classes.push_named_context ctx' env in isevars := Evarutil.nf_evar_defs !isevars; diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index 36a0e9c91a..986825f25c 100644 --- a/contrib/subtac/subtac_pretyping_F.ml +++ b/contrib/subtac/subtac_pretyping_F.ml @@ -566,8 +566,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (pretype_type empty_valcon env isevars lvar c).utj_val in let evd,_ = consider_remaining_unif_problems env !isevars in let evd = nf_evar_defs evd in - let c' = nf_evar (evars_of evd) c' in -(* let evd = undefined_evars evd in *) let evd = Typeclasses.resolve_typeclasses env (evars_of evd) evd in let c' = nf_evar (evars_of evd) c' in isevars := evd; |