diff options
| -rw-r--r-- | pretyping/pretyping.ml | 27 | ||||
| -rw-r--r-- | pretyping/pretyping.mli | 13 | ||||
| -rw-r--r-- | proofs/evar_refiner.ml | 2 | ||||
| -rw-r--r-- | tactics/evar_tactics.ml | 7 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 7 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 12 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 2 |
7 files changed, 53 insertions, 17 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index f18aa364b..cb3e81efe 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -48,7 +48,11 @@ type typing_constraint = OfType of types | IsType | WithoutTypeConstraint type var_map = constr_under_binders Id.Map.t type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t type unbound_ltac_var_map = Genarg.tlevel Genarg.generic_argument Id.Map.t -type ltac_var_map = var_map * uconstr_var_map * unbound_ltac_var_map +type ltac_var_map = { + ltac_constrs : var_map; + ltac_uconstrs : uconstr_var_map; + ltac_genargs : unbound_ltac_var_map; +} type glob_constr_ltac_closure = ltac_var_map * glob_constr type pure_open_constr = evar_map * constr @@ -237,7 +241,7 @@ let protected_get_type_of env sigma c = (str "Cannot reinterpret " ++ quote (print_constr c) ++ str " in the current environment.") -let pretype_id pretype loc env evdref (lvar,globvar,unbndltacvars) id = +let pretype_id pretype loc env evdref lvar id = let sigma = !evdref in (* Look for the binder of [id] *) try @@ -246,21 +250,22 @@ let pretype_id pretype loc env evdref (lvar,globvar,unbndltacvars) id = with Not_found -> (* Check if [id] is an ltac variable *) try - let (ids,c) = Id.Map.find id lvar in + let (ids,c) = Id.Map.find id lvar.ltac_constrs in let subst = List.map (invert_ltac_bound_name env id) ids in let c = substl subst c in { uj_val = c; uj_type = protected_get_type_of env sigma c } with Not_found -> try - let {closure;term} = Id.Map.find id globvar in + let {closure;term} = Id.Map.find id lvar.ltac_uconstrs in + let lvar = { lvar with ltac_constrs = closure.typed; ltac_uconstrs = closure.untyped } in (* spiwack: I'm catching [Not_found] potentially too eagerly here, as the call to the main pretyping function is caught inside the try but I want to avoid refactoring this function too much for now. *) - pretype env evdref (closure.typed,closure.untyped,unbndltacvars) term + pretype env evdref lvar term with Not_found -> (* Check if [id] is a ltac variable not bound to a term *) (* and build a nice error message *) - if Id.Map.mem id unbndltacvars then + if Id.Map.mem id lvar.ltac_genargs then user_err_loc (loc,"", str "Variable " ++ pr_id id ++ str " should be bound to a term."); (* Check if [id] is a section or goal variable *) @@ -362,7 +367,7 @@ let is_GHole = function | GHole _ -> true | _ -> false -let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t = +let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var_map) t = let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in let pretype_type = pretype_type resolve_tc in let pretype = pretype resolve_tc in @@ -410,7 +415,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t = | Some ty -> ty | None -> new_type_evar evdref env loc in - let ist = Util.pi3 lvar in + let ist = lvar.ltac_genargs in let (c, sigma) = Hook.get f_genarg_interp ty env !evdref ist arg in let () = evdref := sigma in { uj_val = c; uj_type = ty } @@ -907,7 +912,11 @@ let no_classes_no_fail_inference_flags = { let all_and_fail_flags = default_inference_flags true let all_no_fail_flags = default_inference_flags false -let empty_lvar : ltac_var_map = (Id.Map.empty, Id.Map.empty, Id.Map.empty) +let empty_lvar : ltac_var_map = { + ltac_constrs = Id.Map.empty; + ltac_uconstrs = Id.Map.empty; + ltac_genargs = Id.Map.empty; +} let on_judgment f j = let c = mkCast(j.uj_val,DEFAULTcast, j.uj_type) in diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 4a80226bd..33f5e420d 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -30,7 +30,18 @@ type typing_constraint = OfType of types | IsType | WithoutTypeConstraint type var_map = Pattern.constr_under_binders Id.Map.t type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t type unbound_ltac_var_map = Genarg.tlevel Genarg.generic_argument Id.Map.t -type ltac_var_map = var_map * uconstr_var_map * unbound_ltac_var_map + +type ltac_var_map = { + ltac_constrs : var_map; + (** Ltac variables bound to constrs *) + ltac_uconstrs : uconstr_var_map; + (** Ltac variables bound to untyped constrs *) + ltac_genargs : unbound_ltac_var_map; + (** Ltac variables bound to other kinds of arguments *) +} + +val empty_lvar : ltac_var_map + type glob_constr_ltac_closure = ltac_var_map * glob_constr type pure_open_constr = evar_map * constr diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 4746177ac..98a97a91c 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -64,6 +64,6 @@ let instantiate_pf_com evk com sigma = let evi = Evd.find sigma evk in let env = Evd.evar_filtered_env evi in let rawc = Constrintern.intern_constr env com in - let ltac_vars = (Id.Map.empty, Id.Map.empty, Id.Map.empty) in + let ltac_vars = Pretyping.empty_lvar in let sigma' = w_refine (evk, evi) (ltac_vars, rawc) sigma in sigma' diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index 27986eab6..478019b41 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -44,7 +44,12 @@ let instantiate_tac n (ist,rawc) ido = let evi = Evd.find sigma evk in let filtered = Evd.evar_filtered_env evi in let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in - let sigma' = w_refine (evk,evi) ((constrvars,Names.Id.Map.empty, ist.Geninterp.lfun),rawc) sigma in + let lvar = { + Pretyping.ltac_constrs = constrvars; + ltac_uconstrs = Names.Id.Map.empty; + ltac_genargs = ist.Geninterp.lfun; + } in + let sigma' = w_refine (evk,evi) (lvar ,rawc) sigma in tclEVARS sigma' gl end diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 214db580a..af28f5145 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -364,8 +364,11 @@ let refine_tac {Glob_term.closure=closure;term=term} = Goal.bind Goal.concl (fun concl -> let flags = Pretyping.all_no_fail_flags in let tycon = Pretyping.OfType concl in - Goal.Refinable.constr_of_raw h tycon flags - Glob_term.(closure.typed,closure.untyped,Id.Map.empty) term + let lvar = { Pretyping.empty_lvar with + Pretyping.ltac_constrs = closure.Glob_term.typed; + Pretyping.ltac_uconstrs = closure.Glob_term.untyped; + } in + Goal.Refinable.constr_of_raw h tycon flags lvar term ) end in Proofview.Goal.lift c begin fun c -> 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 diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 7c42d7a8f..7497393e5 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1173,7 +1173,7 @@ let explain_ltac_call_trace last trace loc = | Proof_type.LtacAtomCall te -> quote (Pptactic.pr_glob_tactic (Global.env()) (Tacexpr.TacAtom (Loc.ghost,te))) - | Proof_type.LtacConstrInterp (c,(vars,_,unboundvars)) -> + | Proof_type.LtacConstrInterp (c, { Pretyping.ltac_constrs = vars }) -> quote (pr_glob_constr_env (Global.env()) c) ++ (if not (Id.Map.is_empty vars) then strbrk " (with " ++ |