From cbea91d815f134d63d02d8fb1bd78ed97db28cd1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 11 Nov 2016 19:52:48 +0100
Subject: Tacmach API using EConstr.

---
 ltac/extratactics.ml4 | 4 ++--
 ltac/rewrite.ml       | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'ltac')

diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index c3ca8f906f..3e7cf5d13b 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -734,7 +734,7 @@ let refl_equal =
   call it before it is defined. *)
 let  mkCaseEq a  : unit Proofview.tactic =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
-    let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g a) gl in
+    let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g (EConstr.of_constr a)) gl in
        Tacticals.New.tclTHENLIST
          [Tactics.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])];
           Proofview.Goal.nf_enter { enter = begin fun gl ->
@@ -789,7 +789,7 @@ let destauto t =
 
 let destauto_in id = 
   Proofview.Goal.nf_enter { enter = begin fun gl ->
-  let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g (mkVar id)) gl in
+  let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g (EConstr.mkVar id)) gl in
 (*  Pp.msgnl (Printer.pr_lconstr (mkVar id)); *)
 (*  Pp.msgnl (Printer.pr_lconstr (ctype)); *)
   destauto ctype
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index dfcfbfbd35..37b9a9edbc 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -2188,7 +2188,7 @@ let setoid_transitivity c =
     
 let setoid_symmetry_in id =
   Proofview.V82.tactic (fun gl ->
-  let ctype = pf_unsafe_type_of gl (mkVar id) in
+  let ctype = pf_unsafe_type_of gl (EConstr.mkVar id) in
   let binders,concl = decompose_prod_assum ctype in
   let (equiv, args) = decompose_app concl in
   let rec split_last_two = function
-- 
cgit v1.2.3