From 05afd04095e35d77ca135bd2c1cb8d303ea2d6a8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Nov 2016 18:18:17 +0100
Subject: Ltac now uses evar-based constrs.

---
 ltac/g_class.ml4 | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'ltac/g_class.ml4')

diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4
index a983a4fea7..b7f0881f14 100644
--- a/ltac/g_class.ml4
+++ b/ltac/g_class.ml4
@@ -62,19 +62,19 @@ TACTIC EXTEND typeclasses_eauto
 END
 
 TACTIC EXTEND head_of_constr
-  [ "head_of_constr" ident(h) constr(c) ] -> [ head_of_constr h (EConstr.of_constr c) ]
+  [ "head_of_constr" ident(h) constr(c) ] -> [ head_of_constr h c ]
 END
 
 TACTIC EXTEND not_evar
-  [ "not_evar" constr(ty) ] -> [ not_evar (EConstr.of_constr ty) ]
+  [ "not_evar" constr(ty) ] -> [ not_evar ty ]
 END
 
 TACTIC EXTEND is_ground
-  [ "is_ground" constr(ty) ] -> [ Proofview.V82.tactic (is_ground (EConstr.of_constr ty)) ]
+  [ "is_ground" constr(ty) ] -> [ Proofview.V82.tactic (is_ground ty) ]
 END
 
 TACTIC EXTEND autoapply
-  [ "autoapply" constr(c) "using" preident(i) ] -> [ Proofview.V82.tactic (autoapply (EConstr.of_constr c) i) ]
+  [ "autoapply" constr(c) "using" preident(i) ] -> [ Proofview.V82.tactic (autoapply c i) ]
 END
 
 (** TODO: DEPRECATE *)
-- 
cgit v1.2.3