From b9ad51bb8aa4fbd1bd54314797428a1a0ae19fde Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 25 May 2018 16:11:56 +0200
Subject: Adapting to move of register_constr_interp0 from Pretyping to
 GlobEnv.

---
 src/tac2core.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/tac2core.ml b/src/tac2core.ml
index 13265ee080..d745d52c82 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -974,7 +974,7 @@ let () =
     let c, sigma = Pfedit.refine_by_tactic env sigma concl tac in
     (EConstr.of_constr c, sigma)
   in
-  Pretyping.register_constr_interp0 wit_ltac2 interp
+  GlobEnv.register_constr_interp0 wit_ltac2 interp
 
 let () =
   let interp ist env sigma concl id =
@@ -984,7 +984,7 @@ let () =
     let sigma = Typing.check env sigma c concl in
     (c, sigma)
   in
-  Pretyping.register_constr_interp0 wit_ltac2_quotation interp
+  GlobEnv.register_constr_interp0 wit_ltac2_quotation interp
 
 let () =
   let pr_raw id = Genprint.PrinterBasic mt in
-- 
cgit v1.2.3