diff options
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/g_class.ml4 | 6 | ||||
| -rw-r--r-- | ltac/rewrite.ml | 2 |
2 files changed, 5 insertions, 3 deletions
diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4 index ea9a2b6e17..45ee86c4ef 100644 --- a/ltac/g_class.ml4 +++ b/ltac/g_class.ml4 @@ -62,15 +62,15 @@ TACTIC EXTEND typeclasses_eauto END TACTIC EXTEND head_of_constr - [ "head_of_constr" ident(h) constr(c) ] -> [ head_of_constr h c ] + [ "head_of_constr" ident(h) constr(c) ] -> [ head_of_constr h (EConstr.of_constr c) ] END TACTIC EXTEND not_evar - [ "not_evar" constr(ty) ] -> [ not_evar ty ] + [ "not_evar" constr(ty) ] -> [ not_evar (EConstr.of_constr ty) ] END TACTIC EXTEND is_ground - [ "is_ground" constr(ty) ] -> [ Proofview.V82.tactic (is_ground ty) ] + [ "is_ground" constr(ty) ] -> [ Proofview.V82.tactic (is_ground (EConstr.of_constr ty)) ] END TACTIC EXTEND autoapply diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index f2ffb0413b..a2b6cb97c1 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -132,6 +132,7 @@ let find_class_proof proof_type proof_method env evars carrier relation = try let evars, goal = app_poly_check env evars proof_type [| carrier ; relation |] in let evars', c = Typeclasses.resolve_one_typeclass env (goalevars evars) (EConstr.of_constr goal) in + let c = EConstr.Unsafe.to_constr c in if extends_undefined (goalevars evars) evars' then raise Not_found else app_poly_check env (evars',cstrevars evars) proof_method [| carrier; relation; c |] with e when Logic.catchable_exception e -> raise Not_found @@ -1951,6 +1952,7 @@ let default_morphism sign m = in let evars, morph = app_poly_check env evars PropGlobal.proper_type [| t; sign; m |] in let evars, mor = resolve_one_typeclass env (goalevars evars) (EConstr.of_constr morph) in + let mor = EConstr.Unsafe.to_constr mor in mor, proper_projection mor morph let add_setoid global binders a aeq t n = |