From 4dab4fc5b2c20e9b7db88aec25a920b56ac83cb6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 14 Apr 2018 23:35:43 +0200
Subject: Moving part of pretyping dealing with ltac and renaming in new module
 GlobEnv.

This module contains:
- the former ExtraEnv in pretyping
- a few functions to traverse binders in pretyping.ml and cases.ml
- the part of pretyping dealing with genarg interpretation

The dependency of pretyping in an interpretation of names as names of
variables of identifier is now hidden in GlobEnv (no more explicit
"lvar" management in pretyping.ml). Similarly for the interpretation
of names as terms and for the interpretation of tactics-in-terms.

We keep empty_lvar in Glob_ops for compatibility, even though it is a
bit isolated there.
---
 plugins/ltac/tacinterp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index a0446bd6a0..f4313a8fa3 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2029,7 +2029,7 @@ let _ =
     let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in
     (EConstr.of_constr c, sigma)
   in
-  Pretyping.register_constr_interp0 wit_tactic eval
+  GlobEnv.register_constr_interp0 wit_tactic eval
 
 let vernac_debug b =
   set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)
-- 
cgit v1.2.3