From 21994cc4c617582f4f94577c1c582a7b51b7770b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 7 Aug 2014 16:42:39 +0200 Subject: Better structure for Ltac pretyping environments. --- tactics/tacinterp.ml | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) (limited to 'tactics/tacinterp.ml') diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 4372f87a4..35f36f008 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -485,7 +485,11 @@ let interp_uconstr ist env = function let interp_gen kind ist allow_patvar flags env sigma (c,ce) = let constrvars = extract_ltac_constr_values ist env in - let vars = (constrvars, Id.Map.empty, ist.lfun) in + let vars = { + Pretyping.ltac_constrs = constrvars; + Pretyping.ltac_uconstrs = Id.Map.empty; + Pretyping.ltac_genargs = ist.lfun; + } in let c = match ce with | None -> c (* If at toplevel (ce<>None), the error can be due to an incorrect @@ -1185,7 +1189,11 @@ and interp_tacarg ist arg : typed_generic_argument GTac.t = let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let {closure;term} = interp_uconstr ist env c in - let vars = closure.typed , closure.untyped , ist.lfun in + let vars = { + Pretyping.ltac_constrs = closure.typed; + Pretyping.ltac_uconstrs = closure.untyped; + Pretyping.ltac_genargs = ist.lfun; + } in let (sigma,c_interp) = Pretyping.understand_ltac constr_flags sigma env vars WithoutTypeConstraint term in -- cgit v1.2.3