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.

---
 tactics/auto.ml    | 2 +-
 tactics/tactics.ml | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 4218be0bbd..b548f8b928 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -152,7 +152,7 @@ let conclPattern concl pat tac =
      let open Genarg in
      let open Geninterp in
      let inj c = match val_tag (topwit Stdarg.wit_constr) with
-     | Val.Base tag -> Val.Dyn (tag, EConstr.Unsafe.to_constr c)
+     | Val.Base tag -> Val.Dyn (tag, c)
      | _ -> assert false
      in
      let fold id c accu = Id.Map.add id (inj c) accu in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 574f1c6f3c..4e833eb556 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -51,7 +51,7 @@ open Context.Named.Declaration
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
-let inj_with_occurrences e = (AllOccurrences,EConstr.Unsafe.to_constr e)
+let inj_with_occurrences e = (AllOccurrences,e)
 
 let dloc = Loc.ghost
 
@@ -922,7 +922,7 @@ let reduction_clause redexp cl =
 let reduce redexp cl =
   let trace () =
     let open Printer in
-    let pr = (pr_constr, pr_lconstr, pr_evaluable_reference, pr_constr_pattern) in
+    let pr = (pr_econstr, pr_leconstr, pr_evaluable_reference, pr_constr_pattern) in
     Pp.(hov 2 (Pputils.pr_red_expr pr str redexp))
   in
   Proofview.Trace.name_tactic trace begin
-- 
cgit v1.2.3