Class_tactics API using EConstr.

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 =