diff options
| author | Arnaud Spiwack | 2014-09-08 09:48:47 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-09-08 10:58:23 +0200 |
| commit | 340bc24c06e0051b5e373dcdbe1691dfe9544054 (patch) | |
| tree | 3043920889e1ab03b51e003b54797ac7da803eb7 | |
| parent | 9486c0bcaa39465ec254db72a13bd51313457ff1 (diff) | |
Rename [extract_ltac_uconstr_values] to [extract_ltac_constr_context].
The latter is more representative of its actual function: extract from the Ltac context the values which are relevant to the interpretation of terms (either type or untyped).
| -rw-r--r-- | tactics/tacinterp.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index dde6c7ab2e..c3869ec293 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -468,7 +468,7 @@ let interp_fresh_id ist env l = (* Extract the uconstr list from lfun *) -let extract_ltac_uconstr_values ist env = +let extract_ltac_constr_context ist env = let open Glob_term in let fold id v ({idents;typed;untyped} as accu) = try @@ -490,9 +490,9 @@ let extract_ltac_uconstr_values ist env = untyped constr, it suffices to adjoin a closure environment. *) let interp_uconstr ist env = function | (term,None) -> - { closure = extract_ltac_uconstr_values ist env ; term } + { closure = extract_ltac_constr_context ist env ; term } | (_,Some ce) -> - let ( {typed ; untyped } as closure) = extract_ltac_uconstr_values ist env in + let ( {typed ; untyped } as closure) = extract_ltac_constr_context ist env in let ltacvars = { Constrintern.ltac_vars = Id.(Set.union (Map.domain typed) (Map.domain untyped)); ltac_bound = Id.Map.domain ist.lfun; @@ -500,7 +500,7 @@ let interp_uconstr ist env = function { closure ; term = intern_gen WithoutTypeConstraint ~ltacvars env ce } let interp_gen kind ist allow_patvar flags env sigma (c,ce) = - let constrvars = extract_ltac_uconstr_values ist env in + let constrvars = extract_ltac_constr_context ist env in let vars = { Pretyping.ltac_constrs = constrvars.typed; Pretyping.ltac_uconstrs = constrvars.untyped; |