diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-02 16:34:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-02 16:55:16 +0200 |
| commit | 67500967edf584fcddc41c74aea09d48ee80a03c (patch) | |
| tree | a0c46b71ac7536317462836a1336f8d497ab553e /tactics/tacintern.ml | |
| parent | 94b201b0a7b03978d96b8f8c9d631e4fa4bda4b0 (diff) | |
Better struture for Ltac internalization environments in Constrintern.
Diffstat (limited to 'tactics/tacintern.ml')
| -rw-r--r-- | tactics/tacintern.ml | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 2a66b32bc..c2f85d534 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -245,7 +245,11 @@ let intern_binding_name ist x = let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env} c = let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in let scope = if isarity then Pretyping.IsType else Pretyping.WithoutTypeConstraint in - let ltacvars = (lfun, Id.Set.empty,Id.Map.empty) in + let ltacvars = { + Constrintern.ltac_vars = lfun; + ltac_bound = Id.Set.empty; + ltac_subst = Id.Map.empty; + } in let c' = warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars env) c in @@ -318,7 +322,11 @@ let intern_flag ist red = let intern_constr_with_occurrences ist (l,c) = (l,intern_constr ist c) let intern_constr_pattern ist ~as_type ~ltacvars pc = - let ltacvars = ltacvars, Id.Set.empty,Id.Map.empty in + let ltacvars = { + Constrintern.ltac_vars = ltacvars; + ltac_bound = Id.Set.empty; + ltac_subst = Id.Map.empty; + } in let metas,pat = Constrintern.intern_constr_pattern ist.genv ~as_type ~ltacvars pc in |