diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 4 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 14 |
2 files changed, 9 insertions, 9 deletions
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 = |