diff options
| author | Hugo Herbelin | 2019-11-18 16:04:45 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-12-06 17:31:39 +0100 |
| commit | 490704f4b2db98f4ef15f5e380b63e49e13a418b (patch) | |
| tree | 625e60c878e2768dbce36129e1df80ceace17495 /plugins | |
| parent | 28c4f57e0614523879201d1c59816cde188e5b22 (diff) | |
Moving the diversity of constr printers to a label style.
This allows to give access to all printing options (e.g. a scope or
being-in-context) to every printer w/o increasing the numbers of
functions.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/firstorder/sequent.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/gen_principle.ml | 6 | ||||
| -rw-r--r-- | plugins/ltac/pptactic.ml | 2 |
3 files changed, 5 insertions, 5 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/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 -> |