aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/g_tactic.mlg2
-rw-r--r--plugins/ltac/pptactic.ml4
-rw-r--r--plugins/ltac/rewrite.ml14
-rw-r--r--plugins/ltac/tacinterp.ml30
4 files changed, 20 insertions, 30 deletions
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index d82eadcfc7..f0d6258cd1 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -135,7 +135,7 @@ let mk_cofix_tac (loc,id,bl,ann,ty) =
~hdr:"Constr:mk_cofix_tac"
(Pp.str"Annotation forbidden in cofix expression.")) ann in
let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,bk,t)) bl in
- (id,CAst.make ~loc @@ CProdN(bl,ty))
+ (id,if bl = [] then ty else CAst.make ~loc @@ CProdN(bl,ty))
(* Functions overloaded by quotifier *)
let destruction_arg_of_constr (c,lbind as clbind) = match lbind with
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 =
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 9633c9bd77..98aa649b62 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -212,12 +212,11 @@ let constr_of_id env id =
(** Generic arguments : table of interpretation functions *)
-(* Some of the code further down depends on the fact that push_trace does not modify sigma (the evar map) *)
let push_trace call ist =
if is_traced () then match TacStore.get ist.extra f_trace with
- | None -> Proofview.tclUNIT [call]
- | Some trace -> Proofview.tclUNIT (call :: trace)
- else Proofview.tclUNIT []
+ | None -> [call]
+ | Some trace -> (call :: trace)
+ else []
let propagate_trace ist loc id v =
if has_type v (topwit wit_tacvalue) then
@@ -225,7 +224,7 @@ let propagate_trace ist loc id v =
match tacv with
| VFun (appl,_,lfun,it,b) ->
let t = if List.is_empty it then b else TacFun (it,b) in
- push_trace(loc,LtacVarCall (id,t)) ist >>= fun trace ->
+ let trace = push_trace(loc,LtacVarCall (id,t)) ist in
let ans = VFun (appl,trace,lfun,it,b) in
Proofview.tclUNIT (of_tacvalue ans)
| _ -> Proofview.tclUNIT v
@@ -536,16 +535,7 @@ let interp_gen kind ist pattern_mode flags env sigma c =
ltac_idents = constrvars.idents;
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
- this with the kludge of an empty proofview, and rely on the
- invariant that running the tactic returned by push_trace does
- not modify sigma. *)
- let (_, dummy_proofview) = Proofview.init sigma [] in
-
- (* Again this is called at times with no open proof! *)
- let name, poly = Id.of_string "tacinterp", ist.poly in
- let (trace,_,_,_) = Proofview.apply ~name ~poly env (push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist) dummy_proofview in
+ let trace = push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist in
let (evd,c) =
catch_error trace (understand_ltac flags env sigma vars kind) term
in
@@ -1067,7 +1057,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti
and eval_tactic ist tac : unit Proofview.tactic = match tac with
| TacAtom {loc;v=t} ->
let call = LtacAtomCall t in
- push_trace(loc,call) ist >>= fun trace ->
+ let trace = push_trace(loc,call) ist in
Profile_ltac.do_profile "eval_tactic:2" trace
(catch_error_tac trace (interp_atomic ist t))
| TacFun _ | TacLetIn _ | TacMatchGoal _ | TacMatch _ -> interp_tactic ist tac
@@ -1100,7 +1090,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
end
| TacAbstract (t,ido) ->
let call = LtacMLCall tac in
- push_trace(None,call) ist >>= fun trace ->
+ let trace = push_trace(None,call) ist in
Profile_ltac.do_profile "eval_tactic:TacAbstract" trace
(catch_error_tac trace begin
Proofview.Goal.enter begin fun gl -> Abstract.tclABSTRACT
@@ -1153,7 +1143,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
let tac l =
let addvar x v accu = Id.Map.add x v accu in
let lfun = List.fold_right2 addvar alias.Tacenv.alias_args l ist.lfun in
- Ftactic.lift (push_trace (loc,LtacNotationCall s) ist) >>= fun trace ->
+ let trace = push_trace (loc,LtacNotationCall s) ist in
let ist = {
lfun
; poly
@@ -1179,7 +1169,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
Ftactic.run tac (fun () -> Proofview.tclUNIT ())
| TacML {loc; v=(opn,l)} ->
- push_trace (Loc.tag ?loc @@ LtacMLCall tac) ist >>= fun trace ->
+ let trace = push_trace (Loc.tag ?loc @@ LtacMLCall tac) ist in
let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in
let tac = Tacenv.interp_ml_tactic opn in
let args = Ftactic.List.map_right (fun a -> interp_tacarg ist a) l in
@@ -1214,7 +1204,7 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t =
let ids = extract_ids [] ist.lfun Id.Set.empty in
let loc_info = (Option.default loc loc',LtacNameCall r) in
let extra = TacStore.set ist.extra f_avoid_ids ids in
- push_trace loc_info ist >>= fun trace ->
+ let trace = push_trace loc_info ist in
let extra = TacStore.set extra f_trace trace in
let ist = { lfun = Id.Map.empty; poly; extra } in
let appl = GlbAppl[r,[]] in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 08:15:26 +0000