diff options
| author | Hugo Herbelin | 2018-04-14 23:35:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-10 10:41:05 +0200 |
| commit | 4dab4fc5b2c20e9b7db88aec25a920b56ac83cb6 (patch) | |
| tree | 9b96b878a2ccaf9f7cabfd231791b6a3442d286e /plugins | |
| parent | 077bb33552ecaa08ea8974cd90a06a272f6ce2ab (diff) | |
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.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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) |