diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/evar_tactics.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/extratactics.ml4 | 2 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 6 | ||||
| -rw-r--r-- | plugins/ltac/tacexpr.mli | 2 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 15 | ||||
| -rw-r--r-- | plugins/ltac/tactic_debug.ml | 2 |
6 files changed, 14 insertions, 15 deletions
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index a299e11f8a..7ecfa57f6d 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -28,7 +28,7 @@ let instantiate_evar evk (ist,rawc) sigma = let filtered = Evd.evar_filtered_env evi in let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in let lvar = { - Pretyping.ltac_constrs = constrvars; + Glob_term.ltac_constrs = constrvars; ltac_uconstrs = Names.Id.Map.empty; ltac_idents = Names.Id.Map.empty; ltac_genargs = ist.Geninterp.lfun; diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 18d7b818cd..7259faecd0 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -365,7 +365,7 @@ let refine_tac ist simple with_classes c = let update = begin fun sigma -> c env sigma end in - let refine = Refine.refine ~unsafe:true update in + let refine = Refine.refine ~typecheck:false update in if simple then refine else refine <*> Tactics.New.reduce_after_refine <*> diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 3927ca7ce1..fad181c897 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1539,7 +1539,7 @@ let assert_replacing id newt tac = | d :: rem -> insert_dependent env sigma (LocalAssum (NamedDecl.get_id d, newt)) [] after @ rem in let env' = Environ.reset_with_named_context (val_of_named_context nc) env in - Refine.refine ~unsafe:false begin fun sigma -> + Refine.refine ~typecheck:true begin fun sigma -> let (sigma, ev) = Evarutil.new_evar env' sigma concl in let (sigma, ev') = Evarutil.new_evar env sigma newt in let map d = @@ -1573,7 +1573,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = match clause, prf with | Some id, Some p -> let tac = tclTHENLIST [ - Refine.refine ~unsafe:false (fun h -> (h,p)); + Refine.refine ~typecheck:true (fun h -> (h,p)); Proofview.Unsafe.tclNEWGOALS gls; ] in Proofview.Unsafe.tclEVARS undef <*> @@ -1590,7 +1590,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let (sigma, ev) = Evarutil.new_evar env sigma newt in (sigma, mkApp (p, [| ev |])) end in - Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls + Refine.refine ~typecheck:true make <*> Proofview.Unsafe.tclNEWGOALS gls end | None, None -> Proofview.Unsafe.tclEVARS undef <*> diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 9b6ac8a9ae..67893bd11e 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -386,7 +386,7 @@ type ltac_call_kind = | LtacNameCall of ltac_constant | LtacAtomCall of glob_atomic_tactic_expr | LtacVarCall of Id.t * glob_tactic_expr - | LtacConstrInterp of Glob_term.glob_constr * Pretyping.ltac_var_map + | LtacConstrInterp of Glob_term.glob_constr * Glob_term.ltac_var_map type ltac_trace = ltac_call_kind Loc.located list diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 9d8094205b..0cd3ee2f9c 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -22,7 +22,6 @@ open Nameops open Libnames open Globnames open Nametab -open Pfedit open Refiner open Tacmach.New open Tactic_debug @@ -605,10 +604,10 @@ let interp_gen kind ist pattern_mode flags env sigma c = let { closure = constrvars ; term } = interp_glob_closure ist env sigma ~kind:kind_for_intern ~pattern_mode c in let vars = { - Pretyping.ltac_constrs = constrvars.typed; - Pretyping.ltac_uconstrs = constrvars.untyped; - Pretyping.ltac_idents = constrvars.idents; - Pretyping.ltac_genargs = ist.lfun; + Glob_term.ltac_constrs = constrvars.typed; + Glob_term.ltac_uconstrs = constrvars.untyped; + Glob_term.ltac_idents = constrvars.idents; + Glob_term.ltac_genargs = ist.lfun; } in (* Jason Gross: To avoid unnecessary modifications to tacinterp, as suggested by Arnaud Spiwack, we run push_trace immediately. We do @@ -629,7 +628,7 @@ let interp_gen kind ist pattern_mode flags env sigma c = let constr_flags () = { use_typeclasses = true; solve_unification_constraints = true; - use_hook = solve_by_implicit_tactic (); + use_hook = Pfedit.solve_by_implicit_tactic (); fail_evar = true; expand_evars = true } @@ -644,14 +643,14 @@ let interp_type = interp_constr_gen IsType let open_constr_use_classes_flags () = { use_typeclasses = true; solve_unification_constraints = true; - use_hook = solve_by_implicit_tactic (); + use_hook = Pfedit.solve_by_implicit_tactic (); fail_evar = false; expand_evars = true } let open_constr_no_classes_flags () = { use_typeclasses = false; solve_unification_constraints = true; - use_hook = solve_by_implicit_tactic (); + use_hook = Pfedit.solve_by_implicit_tactic (); fail_evar = false; expand_evars = true } diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index b909c930db..53dc800231 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -364,7 +364,7 @@ let explain_ltac_call_trace last trace loc = | Tacexpr.LtacAtomCall te -> quote (Pptactic.pr_glob_tactic (Global.env()) (Tacexpr.TacAtom (Loc.tag te))) - | Tacexpr.LtacConstrInterp (c, { Pretyping.ltac_constrs = vars }) -> + | Tacexpr.LtacConstrInterp (c, { Glob_term.ltac_constrs = vars }) -> quote (Printer.pr_glob_constr_env (Global.env()) c) ++ (if not (Id.Map.is_empty vars) then strbrk " (with " ++ |