aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/firstorder/sequent.ml2
-rw-r--r--plugins/funind/gen_principle.ml6
-rw-r--r--plugins/ltac/g_tactic.mlg2
-rw-r--r--plugins/ltac/pptactic.ml2
-rw-r--r--plugins/ltac/tacinterp.ml30
5 files changed, 16 insertions, 26 deletions
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 9ff05c33e4..7d84ee6851 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -231,7 +231,7 @@ let print_cmap map=
let print_entry c l s=
let env = Global.env () in
let sigma = Evd.from_env env in
- let xc=Constrextern.extern_constr false env sigma (EConstr.of_constr c) in
+ let xc=Constrextern.extern_constr env sigma (EConstr.of_constr c) in
str "| " ++
prlist Printer.pr_global l ++
str " : " ++
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 6add56dd5b..58efee1518 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -142,7 +142,7 @@ let recompute_binder_list fixpoint_exprl =
with rec_order = ComFixpoint.adjust_rec_order ~structonly:false fix.binders fix.rec_order }) fixpoint_exprl in
let ((_,_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl in
let constr_expr_typel =
- with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in
+ with_full_print (List.map (fun c -> Constrextern.extern_constr (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in
let fixpoint_exprl_with_new_bl =
List.map2 (fun ({ Vernacexpr.binders } as fp) fix_typ ->
let binders, rtype = rebuild_bl [] binders fix_typ in
@@ -1902,8 +1902,8 @@ let make_graph (f_ref : GlobRef.t) =
let env = Global.env () in
let extern_body,extern_type =
with_full_print (fun () ->
- (Constrextern.extern_constr false env sigma (EConstr.of_constr body),
- Constrextern.extern_type false env sigma
+ (Constrextern.extern_constr env sigma (EConstr.of_constr body),
+ Constrextern.extern_type env sigma
(EConstr.of_constr (*FIXME*) c_body.Declarations.const_type)
)
)
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..0e8c225a8f 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -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/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 11:09:56 +0000