diff options
author | 2016-11-30 23:08:19 +0100 | |
---|---|---|
committer | 2017-05-03 20:05:57 +0200 | |
commit | 9262f440e8d8b8559c5488b1333c023f7305d811 (patch) | |
tree | f09ec49bd38357d949876ca4e494fe22ff2b6a0c /plugins/ltac/tacintern.ml | |
parent | 267c880c5e8b73770316518a2a820e779c121fdb (diff) |
Allowing to pass arbitrary data in internalization environments.
Diffstat (limited to 'plugins/ltac/tacintern.ml')
-rw-r--r-- | plugins/ltac/tacintern.ml | 24 |
1 files changed, 14 insertions, 10 deletions
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 75227def0..40a299f76 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -41,13 +41,12 @@ let error_tactic_expected ?loc = type glob_sign = Genintern.glob_sign = { ltacvars : Id.Set.t; (* ltac variables and the subset of vars introduced by Intro/Let/... *) - genv : Environ.env } + genv : Environ.env; + extra : Genintern.Store.t; +} -let fully_empty_glob_sign = - { ltacvars = Id.Set.empty; genv = Environ.empty_env } - -let make_empty_glob_sign () = - { fully_empty_glob_sign with genv = Global.env () } +let fully_empty_glob_sign = Genintern.empty_glob_sign Environ.empty_env +let make_empty_glob_sign () = Genintern.empty_glob_sign (Global.env ()) (* We have identifier <| global_reference <| constr *) @@ -192,12 +191,13 @@ let intern_binding_name ist x = and if a term w/o ltac vars, check the name is indeed quantified *) x -let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env} c = +let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env; extra} 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 = { Constrintern.ltac_vars = lfun; ltac_bound = Id.Set.empty; + ltac_extra = extra; } in let c' = warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars env) c @@ -313,6 +313,7 @@ let intern_constr_pattern ist ~as_type ~ltacvars pc = let ltacvars = { Constrintern.ltac_vars = ltacvars; ltac_bound = Id.Set.empty; + ltac_extra = ist.extra; } in let metas,pat = Constrintern.intern_constr_pattern ist.genv ~as_type ~ltacvars pc @@ -344,7 +345,11 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = let r = match r with | AN r -> r | _ -> Qualid (loc,qualid_of_path (path_of_global (smart_global r))) in - let sign = { Constrintern.ltac_vars = ist.ltacvars; Constrintern.ltac_bound = Id.Set.empty } in + let sign = { + Constrintern.ltac_vars = ist.ltacvars; + ltac_bound = Id.Set.empty; + ltac_extra = ist.extra; + } in let c = Constrintern.interp_reference sign r in match c with | GRef (_,r,None) -> @@ -708,8 +713,7 @@ let glob_tactic_env l env x = let ltacvars = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in Flags.with_option strict_check - (intern_pure_tactic - { ltacvars; genv = env }) + (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars }) x let split_ltac_fun = function |