diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/evar_tactics.ml | 12 | ||||
| -rw-r--r-- | plugins/ltac/pptactic.ml | 4 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 14 |
3 files changed, 16 insertions, 14 deletions
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index c87eb7c3c9..3ea4974a87 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -26,9 +26,9 @@ module NamedDecl = Context.Named.Declaration (* The instantiate tactic *) -let instantiate_evar evk (ist,rawc) sigma = +let instantiate_evar evk (ist,rawc) env sigma = let evi = Evd.find sigma evk in - let filtered = Evd.evar_filtered_env evi in + let filtered = Evd.evar_filtered_env env evi in let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in let lvar = { ltac_constrs = constrvars; @@ -36,7 +36,7 @@ let instantiate_evar evk (ist,rawc) sigma = ltac_idents = Names.Id.Map.empty; ltac_genargs = ist.Geninterp.lfun; } in - let sigma' = w_refine (evk,evi) (lvar ,rawc) sigma in + let sigma' = w_refine (evk,evi) (lvar ,rawc) env sigma in tclEVARS sigma' let evar_list sigma c = @@ -48,6 +48,7 @@ let evar_list sigma c = let instantiate_tac n c ido = Proofview.V82.tactic begin fun gl -> + let env = Global.env () in let sigma = gl.sigma in let evl = match ido with @@ -69,16 +70,17 @@ let instantiate_tac n c ido = user_err Pp.(str "Not enough uninstantiated existential variables."); if n <= 0 then user_err Pp.(str "Incorrect existential variable index."); let evk,_ = List.nth evl (n-1) in - instantiate_evar evk c sigma gl + instantiate_evar evk c env sigma gl end let instantiate_tac_by_name id c = Proofview.V82.tactic begin fun gl -> + let env = Global.env () in let sigma = gl.sigma in let evk = try Evd.evar_key id sigma with Not_found -> user_err Pp.(str "Unknown existential variable.") in - instantiate_evar evk c sigma gl + instantiate_evar evk c env sigma gl end let let_evar name typ = diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 6df068883c..7843faaef3 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -971,7 +971,7 @@ let pr_goal_selector ~toplevel s = | TacTime (s,t) -> hov 1 ( keyword "time" - ++ pr_opt str s ++ spc () + ++ pr_opt qstring s ++ spc () ++ pr_tac (ltactical,E) t), ltactical | TacRepeat t -> @@ -1273,7 +1273,7 @@ let pr_intro_pattern_env p = Genprint.TopPrinterNeedsContext (fun env sigma -> Miscprint.pr_intro_pattern print_constr p) let pr_red_expr_env r = Genprint.TopPrinterNeedsContext (fun env sigma -> - pr_red_expr env sigma (pr_econstr_env, pr_leconstr_env, + pr_red_expr env sigma ((fun e -> pr_econstr_env e), (fun e -> pr_leconstr_env e), pr_evaluable_reference_env env, pr_constr_pattern_env) r) let pr_bindings_env bl = Genprint.TopPrinterNeedsContext (fun env sigma -> diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 2998e1c767..98d14f3d33 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -924,10 +924,10 @@ let reset_env env = let env' = Global.env_of_context (Environ.named_context_val env) in Environ.push_rel_context (Environ.rel_context env) env' -let fold_match ?(force=false) env sigma c = +let fold_match env sigma c = let (ci, p, c, brs) = destCase sigma c in let cty = Retyping.get_type_of env sigma c in - let dep, pred, exists, (sk,eff) = + let dep, pred, exists, sk = let env', ctx, body = let ctx, pred = decompose_lam_assum sigma p in let env' = push_rel_context ctx env in @@ -954,8 +954,8 @@ let fold_match ?(force=false) env sigma c = else case_scheme_kind_from_type) in let exists = Ind_tables.check_scheme sk ci.ci_ind in - if exists || force then - dep, pred, exists, Ind_tables.find_scheme sk ci.ci_ind + if exists then + dep, pred, exists, Ind_tables.lookup_scheme sk ci.ci_ind else raise Not_found in let app = @@ -964,7 +964,7 @@ let fold_match ?(force=false) env sigma c = let meths = List.map (fun br -> br) (Array.to_list brs) in applist (mkConst sk, pars @ [pred] @ meths @ args @ [c]) in - sk, (if exists then env else reset_env env), app, eff + sk, (if exists then env else reset_env env), app let unfold_match env sigma sk app = match EConstr.kind sigma app with @@ -1222,7 +1222,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = else match try Some (fold_match env (goalevars evars) t) with Not_found -> None with | None -> state, c' - | Some (cst, _, t', eff (*FIXME*)) -> + | Some (cst, _, t') -> let state, res = aux { state ; env ; unfresh ; term1 = t' ; ty1 = ty ; cstr = (prop,cstr) ; evars } in @@ -1930,7 +1930,7 @@ let build_morphism_signature env sigma m = let evd = solve_constraints env !evd in let evd = Evd.minimize_universes evd in let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in - Pretyping.check_evars env (Evd.from_env env) evd (EConstr.of_constr m); + Pretyping.check_evars env evd (EConstr.of_constr m); Evd.evar_universe_context evd, m let default_morphism sign m = |