aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/btauto/refl_btauto.ml3
-rw-r--r--plugins/funind/functional_principles_proofs.ml16
-rw-r--r--plugins/funind/functional_principles_types.ml10
-rw-r--r--plugins/funind/glob_term_to_relation.ml85
-rw-r--r--plugins/funind/indfun.ml17
-rw-r--r--plugins/funind/indfun_common.ml18
-rw-r--r--plugins/funind/invfun.ml2
-rw-r--r--plugins/funind/merge.ml16
-rw-r--r--plugins/funind/recdef.ml35
-rw-r--r--plugins/ltac/extraargs.ml44
-rw-r--r--plugins/ltac/g_auto.ml48
-rw-r--r--plugins/ltac/g_rewrite.ml412
-rw-r--r--plugins/ltac/pptactic.ml58
-rw-r--r--plugins/ltac/tacsubst.ml7
-rw-r--r--plugins/ltac/tactic_debug.ml7
-rw-r--r--plugins/micromega/coq_micromega.ml23
-rw-r--r--plugins/micromega/micromega.ml16
-rw-r--r--plugins/romega/refl_omega.ml3
-rw-r--r--plugins/setoid_ring/g_newring.ml410
-rw-r--r--plugins/setoid_ring/newring.ml20
-rw-r--r--plugins/ssr/ssrcommon.ml12
-rw-r--r--plugins/ssr/ssrelim.ml8
-rw-r--r--plugins/ssr/ssrequality.ml28
-rw-r--r--plugins/ssr/ssrfwd.ml23
-rw-r--r--plugins/ssr/ssripats.ml2
-rw-r--r--plugins/ssr/ssrparser.ml42
-rw-r--r--plugins/ssr/ssrprinters.ml2
-rw-r--r--plugins/ssr/ssrvernac.ml412
-rw-r--r--plugins/ssrmatching/ssrmatching.ml49
29 files changed, 272 insertions, 196 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index da8955f0d..a09abfa19 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -200,7 +200,8 @@ module Btauto = struct
let assign = List.combine env var in
let map_msg (key, v) =
let b = if v then str "true" else str "false" in
- let term = Printer.pr_constr key in
+ let sigma, env = Pfedit.get_current_context () in
+ let term = Printer.pr_constr_env env sigma key in
term ++ spc () ++ str ":=" ++ spc () ++ b
in
let assign = List.map map_msg assign in
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index bd5fb1d92..29e824f44 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -44,6 +44,10 @@ let observe_tac s tac g = observe_tac_stream (str s) tac g
*)
+let pr_leconstr_fp =
+ let sigma, env = Pfedit.get_current_context () in
+ Printer.pr_leconstr_env env sigma
+
let debug_queue = Stack.create ()
let rec print_debug_queue e =
@@ -172,7 +176,7 @@ let is_incompatible_eq sigma t =
| _ -> false
with e when CErrors.noncritical e -> false
in
- if res then observe (str "is_incompatible_eq " ++ Printer.pr_leconstr t);
+ if res then observe (str "is_incompatible_eq " ++ pr_leconstr_fp t);
res
let change_hyp_with_using msg hyp_id t tac : tactic =
@@ -220,7 +224,8 @@ let find_rectype env sigma c =
let isAppConstruct ?(env=Global.env ()) sigma t =
try
let t',l = find_rectype env sigma t in
- observe (str "isAppConstruct : " ++ Printer.pr_leconstr t ++ str " -> " ++ Printer.pr_leconstr (applist (t',l)));
+ observe (str "isAppConstruct : " ++ Printer.pr_leconstr_env env sigma t ++ str " -> " ++
+ Printer.pr_leconstr_env env sigma (applist (t',l)));
true
with Not_found -> false
@@ -233,7 +238,8 @@ exception NoChange
let change_eq env sigma hyp_id (context:rel_context) x t end_of_type =
let nochange ?t' msg =
begin
- observe (str ("Not treating ( "^msg^" )") ++ pr_leconstr t ++ str " " ++ match t' with None -> str "" | Some t -> Printer.pr_leconstr t );
+ observe (str ("Not treating ( "^msg^" )") ++ pr_leconstr_env env sigma t ++ str " " ++
+ match t' with None -> str "" | Some t -> Printer.pr_leconstr_env env sigma t );
raise NoChange;
end
in
@@ -841,7 +847,7 @@ let build_proof
| Rel _ -> anomaly (Pp.str "Free var in goal conclusion!")
and build_proof do_finalize dyn_infos g =
(* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *)
- observe_tac_stream (str "build_proof with " ++ Printer.pr_leconstr dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g
+ observe_tac_stream (str "build_proof with " ++ pr_leconstr_fp dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g
and build_proof_args do_finalize dyn_infos (* f_args' args *) :tactic =
fun g ->
let (f_args',args) = dyn_infos.info in
@@ -1135,7 +1141,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
princ_params
);
observe (str "fbody_with_full_params := " ++
- pr_leconstr fbody_with_full_params
+ pr_leconstr_env (Global.env ()) !evd fbody_with_full_params
);
let all_funs_with_full_params =
Array.map (fun f -> applist(f, List.rev_map var_of_decl full_params)) all_funs
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 722dbc16b..3899bc709 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -115,7 +115,9 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
let dummy_var = mkVar (Id.of_string "________") in
let mk_replacement c i args =
let res = mkApp(rel_to_fun.(i), Array.map pop (array_get_start args)) in
- observe (str "replacing " ++ pr_lconstr c ++ str " by " ++ pr_lconstr res);
+ observe (str "replacing " ++
+ pr_lconstr_env env Evd.empty c ++ str " by " ++
+ pr_lconstr_env env Evd.empty res);
res
in
let rec compute_new_princ_type remove env pre_princ : types*(constr list) =
@@ -565,7 +567,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
List.map (* we can now compute the other principles *)
(fun scheme_type ->
incr i;
- observe (Printer.pr_lconstr scheme_type);
+ observe (Printer.pr_lconstr_env env sigma scheme_type);
let type_concl = (strip_prod_assum scheme_type) in
let applied_f = List.hd (List.rev (snd (decompose_app type_concl))) in
let f = fst (decompose_app applied_f) in
@@ -577,8 +579,8 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
let g = fst (decompose_app applied_g) in
if Constr.equal f g
then raise (Found_type j);
- observe (Printer.pr_lconstr f ++ str " <> " ++
- Printer.pr_lconstr g)
+ observe (Printer.pr_lconstr_env env sigma f ++ str " <> " ++
+ Printer.pr_lconstr_env env sigma g)
)
ta;
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 8ab6dbcdf..d04b7a33d 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -379,29 +379,30 @@ let add_pat_variables pat typ env : Environ.env =
fst (
Context.Rel.fold_outside
(fun decl (env,ctxt) ->
- let open Context.Rel.Declaration in
- match decl with
+ let open Context.Rel.Declaration in
+ let sigma, _ = Pfedit.get_current_context () in
+ match decl with
| LocalAssum (Anonymous,_) | LocalDef (Anonymous,_,_) -> assert false
| LocalAssum (Name id, t) ->
- let new_t = substl ctxt t in
- observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++
- str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++
- str "new type := " ++ Printer.pr_lconstr new_t ++ fnl ()
- );
- let open Context.Named.Declaration in
- (Environ.push_named (LocalAssum (id,new_t)) env,mkVar id::ctxt)
- | LocalDef (Name id, v, t) ->
- let new_t = substl ctxt t in
- let new_v = substl ctxt v in
- observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++
- str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++
- str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () ++
- str "old value := " ++ Printer.pr_lconstr v ++ fnl () ++
- str "new value := " ++ Printer.pr_lconstr new_v ++ fnl ()
- );
- let open Context.Named.Declaration in
- (Environ.push_named (LocalDef (id,new_v,new_t)) env,mkVar id::ctxt)
- )
+ let new_t = substl ctxt t in
+ observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++
+ str "old type := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++
+ str "new type := " ++ Printer.pr_lconstr_env env sigma new_t ++ fnl ()
+ );
+ let open Context.Named.Declaration in
+ (Environ.push_named (LocalAssum (id,new_t)) env,mkVar id::ctxt)
+ | LocalDef (Name id, v, t) ->
+ let new_t = substl ctxt t in
+ let new_v = substl ctxt v in
+ observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++
+ str "old type := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++
+ str "new type := " ++ Printer.pr_lconstr_env env sigma new_t ++ fnl () ++
+ str "old value := " ++ Printer.pr_lconstr_env env sigma v ++ fnl () ++
+ str "new value := " ++ Printer.pr_lconstr_env env sigma new_v ++ fnl ()
+ );
+ let open Context.Named.Declaration in
+ (Environ.push_named (LocalDef (id,new_v,new_t)) env,mkVar id::ctxt)
+ )
(Environ.rel_context new_env)
~init:(env,[])
)
@@ -479,7 +480,7 @@ let rec pattern_to_term_and_type env typ = DAst.with_val (function
let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
- observe (str " Entering : " ++ Printer.pr_glob_constr rt);
+ observe (str " Entering : " ++ Printer.pr_glob_constr_env env rt);
let open CAst in
match DAst.get rt with
| GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ ->
@@ -652,8 +653,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
try Inductiveops.find_inductive env (Evd.from_env env) b_typ
with Not_found ->
user_err (str "Cannot find the inductive associated to " ++
- Printer.pr_glob_constr b ++ str " in " ++
- Printer.pr_glob_constr rt ++ str ". try again with a cast")
+ Printer.pr_glob_constr_env env b ++ str " in " ++
+ Printer.pr_glob_constr_env env rt ++ str ". try again with a cast")
in
let case_pats = build_constructors_of_type (fst ind) [] in
assert (Int.equal (Array.length case_pats) 2);
@@ -684,8 +685,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
try Inductiveops.find_inductive env (Evd.from_env env) b_typ
with Not_found ->
user_err (str "Cannot find the inductive associated to " ++
- Printer.pr_glob_constr b ++ str " in " ++
- Printer.pr_glob_constr rt ++ str ". try again with a cast")
+ Printer.pr_glob_constr_env env b ++ str " in " ++
+ Printer.pr_glob_constr_env env rt ++ str ". try again with a cast")
in
let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in
assert (Int.equal (Array.length case_pats) 1);
@@ -897,24 +898,24 @@ let same_raw_term rt1 rt2 =
| GHole _, GHole _ -> true
| _ -> false
let decompose_raw_eq lhs rhs =
- let rec decompose_raw_eq lhs rhs acc =
- observe (str "decomposing eq for " ++ pr_glob_constr lhs ++ str " " ++ pr_glob_constr rhs);
- let (rhd,lrhs) = glob_decompose_app rhs in
- let (lhd,llhs) = glob_decompose_app lhs in
- observe (str "lhd := " ++ pr_glob_constr lhd);
- observe (str "rhd := " ++ pr_glob_constr rhd);
+ let _, env = Pfedit.get_current_context () in
+ let rec decompose_raw_eq lhs rhs acc =
+ observe (str "decomposing eq for " ++ pr_glob_constr_env env lhs ++ str " " ++ pr_glob_constr_env env rhs);
+ let (rhd,lrhs) = glob_decompose_app rhs in
+ let (lhd,llhs) = glob_decompose_app lhs in
+ observe (str "lhd := " ++ pr_glob_constr_env env lhd);
+ observe (str "rhd := " ++ pr_glob_constr_env env rhd);
observe (str "llhs := " ++ int (List.length llhs));
observe (str "lrhs := " ++ int (List.length lrhs));
- let sllhs = List.length llhs in
- let slrhs = List.length lrhs in
- if same_raw_term lhd rhd && Int.equal sllhs slrhs
+ let sllhs = List.length llhs in
+ let slrhs = List.length lrhs in
+ if same_raw_term lhd rhd && Int.equal sllhs slrhs
then
(* let _ = assert false in *)
List.fold_right2 decompose_raw_eq llhs lrhs acc
else (lhs,rhs)::acc
in
decompose_raw_eq lhs rhs []
-
exception Continue
(*
@@ -923,7 +924,7 @@ exception Continue
eliminates some meaningless equalities, applies some rewrites......
*)
let rec rebuild_cons env nb_args relname args crossed_types depth rt =
- observe (str "rebuilding : " ++ pr_glob_constr rt);
+ observe (str "rebuilding : " ++ pr_glob_constr_env env rt);
let open Context.Rel.Declaration in
let open CAst in
match DAst.get rt with
@@ -967,7 +968,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
let id = match DAst.get id with GVar id -> id | _ -> assert false in
begin
try
- observe (str "computing new type for eq : " ++ pr_glob_constr rt);
+ observe (str "computing new type for eq : " ++ pr_glob_constr_env env rt);
let t' =
try fst (Pretyping.understand env (Evd.from_env env) t)(*FIXME*)
with e when CErrors.noncritical e -> raise Continue
@@ -1012,7 +1013,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
let eq' =
DAst.make ?loc:loc1 @@ GApp(DAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;DAst.make ?loc:loc3 @@ GVar id;rt_typ;rt])
in
- observe (str "computing new type for jmeq : " ++ pr_glob_constr eq');
+ observe (str "computing new type for jmeq : " ++ pr_glob_constr_env env eq');
let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in
observe (str " computing new type for jmeq : done") ;
let new_args =
@@ -1099,7 +1100,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
rebuild_cons env nb_args relname args crossed_types depth new_rt
else raise Continue
with Continue ->
- observe (str "computing new type for prod : " ++ pr_glob_constr rt);
+ observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt);
let t',ctx = Pretyping.understand env (Evd.from_env env) t in
let new_env = Environ.push_rel (LocalAssum (n,t')) env in
let new_b,id_to_exclude =
@@ -1115,7 +1116,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
| _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
end
| _ ->
- observe (str "computing new type for prod : " ++ pr_glob_constr rt);
+ observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt);
let t',ctx = Pretyping.understand env (Evd.from_env env) t in
let new_env = Environ.push_rel (LocalAssum (n,t')) env in
let new_b,id_to_exclude =
@@ -1134,7 +1135,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
begin
let not_free_in_t id = not (is_free_in id t) in
let new_crossed_types = t :: crossed_types in
- observe (str "computing new type for lambda : " ++ pr_glob_constr rt);
+ observe (str "computing new type for lambda : " ++ pr_glob_constr_env env rt);
let t',ctx = Pretyping.understand env (Evd.from_env env) t in
match n with
| Name id ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index dab094f91..f01b6669d 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -46,7 +46,7 @@ let functional_induction with_clean c princl pat =
try find_Function_infos c'
with Not_found ->
user_err (str "Cannot find induction information on "++
- Printer.pr_leconstr (mkConst c') )
+ Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') )
in
match Tacticals.elimination_sort_of_goal g with
| InProp -> finfo.prop_lemma
@@ -74,7 +74,7 @@ let functional_induction with_clean c princl pat =
(* mkConst(const_of_id princ_name ),g (\* FIXME *\) *)
with Not_found -> (* This one is neither defined ! *)
user_err (str "Cannot find induction principle for "
- ++Printer.pr_leconstr (mkConst c') )
+ ++ Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') )
in
let princ = EConstr.of_constr princ in
(princ,NoBindings,Tacmach.pf_unsafe_type_of g' princ,g')
@@ -841,12 +841,13 @@ let rec get_args b t : Constrexpr.local_binder_expr list *
let make_graph (f_ref:global_reference) =
let c,c_body =
match f_ref with
- | ConstRef c ->
- begin try c,Global.lookup_constant c
- with Not_found ->
- raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr (mkConst c)) )
- end
- | _ -> raise (UserError (None, str "Not a function reference") )
+ | ConstRef c ->
+ begin try c,Global.lookup_constant c
+ with Not_found ->
+ let sigma, env = Pfedit.get_current_context () in
+ raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr_env env sigma (mkConst c)) )
+ end
+ | _ -> raise (UserError (None, str "Not a function reference") )
in
(match Global.body_of_constant_body c_body with
| None -> error "Cannot build a graph over an axiom!"
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index e9102e9c8..8bf6e48fd 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -333,15 +333,17 @@ let discharge_Function (_,finfos) =
}
let pr_ocst c =
- Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) c (mt ())
+ let sigma, env = Pfedit.get_current_context () in
+ Option.fold_right (fun v acc -> Printer.pr_lconstr_env env sigma (mkConst v)) c (mt ())
let pr_info f_info =
+ let sigma, env = Pfedit.get_current_context () in
str "function_constant := " ++
- Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++
+ Printer.pr_lconstr_env env sigma (mkConst f_info.function_constant)++ fnl () ++
str "function_constant_type := " ++
(try
- Printer.pr_lconstr
- (fst (Global.type_of_global_in_context (Global.env ()) (ConstRef f_info.function_constant)))
+ Printer.pr_lconstr_env env sigma
+ (fst (Global.type_of_global_in_context env (ConstRef f_info.function_constant)))
with e when CErrors.noncritical e -> mt ()) ++ fnl () ++
str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++
str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++
@@ -349,7 +351,7 @@ let pr_info f_info =
str "rect_lemma := " ++ pr_ocst f_info.rect_lemma ++ fnl () ++
str "rec_lemma := " ++ pr_ocst f_info.rec_lemma ++ fnl () ++
str "prop_lemma := " ++ pr_ocst f_info.prop_lemma ++ fnl () ++
- str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl ()
+ str "graph_ind := " ++ Printer.pr_lconstr_env env sigma (mkInd f_info.graph_ind) ++ fnl ()
let pr_table tb =
let l = Cmap_env.fold (fun k v acc -> v::acc) tb [] in
@@ -550,11 +552,11 @@ type tcc_lemma_value =
| Value of constr
| Not_needed
-(* We only "purify" on exceptions *)
+(* We only "purify" on exceptions. XXX: What is this doing here? *)
let funind_purify f x =
- let st = Vernacentries.freeze_interp_state `No in
+ let st = Vernacstate.freeze_interp_state `No in
try f x
with e ->
let e = CErrors.push e in
- Vernacentries.unfreeze_interp_state st;
+ Vernacstate.unfreeze_interp_state st;
Exninfo.iraise e
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 692a874d3..694c80051 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -851,7 +851,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt
in
let type_of_lemma = nf_zeta type_of_lemma in
- observe (str "type_of_lemma := " ++ Printer.pr_leconstr type_of_lemma);
+ observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env env !evd type_of_lemma);
type_of_lemma,type_info
)
funs_constr
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index b372241d2..9e2774ff3 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -90,20 +90,28 @@ let next_ident_fresh (id:Id.t) =
(* comment this line to see debug msgs *)
let msg x = () ;; let pr_lconstr c = str ""
(* uncomment this to see debugging *)
-let prconstr c = msg (str" " ++ Printer.pr_lconstr c)
-let prconstrnl c = msg (str" " ++ Printer.pr_lconstr c ++ str"\n")
+let prconstr c =
+ let sigma, env = Pfedit.get_current_context () in
+ msg (str" " ++ Printer.pr_lconstr_env env sigma c)
+
+let prconstrnl c =
+ let sigma, env = Pfedit.get_current_context () in
+ msg (str" " ++ Printer.pr_lconstr_env env sigma c ++ str"\n")
+
let prlistconstr lc = List.iter prconstr lc
let prstr s = msg(str s)
let prNamedConstr s c =
+ let sigma, env = Pfedit.get_current_context () in
begin
msg(str "");
- msg(str(s^" {§ ") ++ Printer.pr_lconstr c ++ str " §} ");
+ msg(str(s^" {§ ") ++ Printer.pr_lconstr_env env sigma c ++ str " §} ");
msg(str "");
end
let prNamedRConstr s c =
+ let sigma, env = Pfedit.get_current_context () in
begin
msg(str "");
- msg(str(s^" {§ ") ++ Printer.pr_glob_constr c ++ str " §} ");
+ msg(str(s^" {§ ") ++ Printer.pr_glob_constr_env env c ++ str " §} ");
msg(str "");
end
let prNamedLConstr_aux lc = List.iter (prNamedConstr "\n") lc
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 2fdc3bc37..04d729b10 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -54,6 +54,10 @@ let coq_constant m s = EConstr.of_constr @@ Universes.constr_of_global @@
let arith_Nat = ["Arith";"PeanoNat";"Nat"]
let arith_Lt = ["Arith";"Lt"]
+let pr_leconstr_rd =
+ let sigma, env = Pfedit.get_current_context () in
+ Printer.pr_leconstr_env env sigma
+
let coq_init_constant s =
EConstr.of_constr (
Universes.constr_of_global @@
@@ -337,7 +341,8 @@ let check_not_nested sigma forbidden e =
try
check_not_nested e
with UserError(_,p) ->
- user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_leconstr e ++ str " " ++ p)
+ let _, env = Pfedit.get_current_context () in
+ user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_leconstr_env env sigma e ++ str " " ++ p)
(* ['a info] contains the local information for traveling *)
type 'a infos =
@@ -455,7 +460,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
jinfo.otherS () expr_info continuation_tac expr_info g
with e when CErrors.noncritical e ->
- user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
+ user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
end
| Lambda(n,t,b) ->
begin
@@ -463,7 +468,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
jinfo.otherS () expr_info continuation_tac expr_info g
with e when CErrors.noncritical e ->
- user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
+ user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
end
| Case(ci,t,a,l) ->
begin
@@ -491,8 +496,8 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
jinfo.apP (f,args) expr_info continuation_tac in
travel_args jinfo
expr_info.is_main_branch new_continuation_tac new_infos g
- | Case _ -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)")
- | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr expr_info.info ++ Pp.str ".")
+ | Case _ -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)")
+ | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ Pp.str ".")
end
| Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} g
| Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ ->
@@ -515,7 +520,7 @@ and travel_args jinfo is_final continuation_tac infos =
{infos with info=arg;is_final=false}
and travel jinfo continuation_tac expr_info =
observe_tac
- (str jinfo.message ++ Printer.pr_leconstr expr_info.info)
+ (str jinfo.message ++ pr_leconstr_rd expr_info.info)
(travel_aux jinfo continuation_tac expr_info)
(* Termination proof *)
@@ -731,7 +736,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
let destruct_tac,rev_to_thin_intro =
mkDestructEq [expr_info.rec_arg_id] a' g in
let to_thin_intro = List.rev rev_to_thin_intro in
- observe_tac (str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr a')
+ observe_tac (str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr_env (pf_env g) sigma a')
(try
(tclTHENS
destruct_tac
@@ -740,7 +745,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
with
| UserError(Some "Refiner.thensn_tac3",_)
| UserError(Some "Refiner.tclFAIL_s",_) ->
- (observe_tac (str "is computable " ++ Printer.pr_leconstr new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} )
+ (observe_tac (str "is computable " ++ Printer.pr_leconstr_env (pf_env g) sigma new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} )
))
g
@@ -991,11 +996,11 @@ let rec intros_values_eq expr_info acc =
let equation_others _ expr_info continuation_tac infos =
if expr_info.is_final && expr_info.is_main_branch
then
- observe_tac (str "equation_others (cont_tac +intros) " ++ Printer.pr_leconstr expr_info.info)
+ observe_tac (str "equation_others (cont_tac +intros) " ++ pr_leconstr_rd expr_info.info)
(tclTHEN
(continuation_tac infos)
- (observe_tac (str "intros_values_eq equation_others " ++ Printer.pr_leconstr expr_info.info) (intros_values_eq expr_info [])))
- else observe_tac (str "equation_others (cont_tac) " ++ Printer.pr_leconstr expr_info.info) (continuation_tac infos)
+ (observe_tac (str "intros_values_eq equation_others " ++ pr_leconstr_rd expr_info.info) (intros_values_eq expr_info [])))
+ else observe_tac (str "equation_others (cont_tac) " ++ pr_leconstr_rd expr_info.info) (continuation_tac infos)
let equation_app f_and_args expr_info continuation_tac infos =
if expr_info.is_final && expr_info.is_main_branch
@@ -1225,8 +1230,8 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
let get_current_subgoals_types () =
let p = Proof_global.give_me_the_proof () in
- let { Evd.it=sgs ; sigma=sigma } = Proof.V82.subgoals p in
- sigma, List.map (Goal.V82.abstract_type sigma) sgs
+ let sgs,_,_,_,sigma = Proof.proof p in
+ sigma, List.map (Goal.V82.abstract_type sigma) sgs
exception EmptySubgoals
let build_and_l sigma l =
@@ -1419,7 +1424,7 @@ let com_terminate
nb_args ctx
hook =
let start_proof ctx (tac_start:tactic) (tac_end:tactic) =
- let (evmap, env) = Lemmas.get_current_context() in
+ let evmap, env = Pfedit.get_current_context () in
Lemmas.start_proof thm_name
(Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env)
ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) hook;
@@ -1471,7 +1476,7 @@ let (com_eqn : int -> Id.t ->
| ConstRef c -> is_opaque_constant c
| _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.")
in
- let (evmap, env) = Lemmas.get_current_context() in
+ let evmap, env = Pfedit.get_current_context () in
let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in
let f_constr = constr_of_global f_ref in
let equation_lemma_type = subst1 f_constr equation_lemma_type in
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 89feea8dc..bb01aca55 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -133,7 +133,9 @@ let pr_occurrences = pr_occurrences () () ()
let pr_gen prc _prlc _prtac c = prc c
-let pr_globc _prc _prlc _prtac (_,glob) = Printer.pr_glob_constr glob
+let pr_globc _prc _prlc _prtac (_,glob) =
+ let _, env = Pfedit.get_current_context () in
+ Printer.pr_glob_constr_env env glob
let interp_glob ist gl (t,_) = Tacmach.project gl , (ist,t)
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index 5baa0d5c1..84e79d8ab 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -51,8 +51,12 @@ let eval_uconstrs ist cs =
List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs
let pr_auto_using_raw _ _ _ = Pptactic.pr_auto_using Ppconstr.pr_constr_expr
-let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> Printer.pr_glob_constr c)
-let pr_auto_using _ _ _ = Pptactic.pr_auto_using Printer.pr_closed_glob
+let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) ->
+ let _, env = Pfedit.get_current_context () in
+ Printer.pr_glob_constr_env env c)
+let pr_auto_using _ _ _ = Pptactic.pr_auto_using
+ (let sigma, env = Pfedit.get_current_context () in
+ Printer.pr_closed_glob_env env sigma)
ARGUMENT EXTEND auto_using
TYPED AS uconstr_list
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index b148d962e..91abe1019 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -31,8 +31,12 @@ type constr_expr_with_bindings = constr_expr with_bindings
type glob_constr_with_bindings = Tacexpr.glob_constr_and_expr with_bindings
type glob_constr_with_bindings_sign = interp_sign * Tacexpr.glob_constr_and_expr with_bindings
-let pr_glob_constr_with_bindings_sign _ _ _ (ge : glob_constr_with_bindings_sign) = Printer.pr_glob_constr (fst (fst (snd ge)))
-let pr_glob_constr_with_bindings _ _ _ (ge : glob_constr_with_bindings) = Printer.pr_glob_constr (fst (fst ge))
+let pr_glob_constr_with_bindings_sign _ _ _ (ge : glob_constr_with_bindings_sign) =
+ let _, env = Pfedit.get_current_context () in
+ Printer.pr_glob_constr_env env (fst (fst (snd ge)))
+let pr_glob_constr_with_bindings _ _ _ (ge : glob_constr_with_bindings) =
+ let _, env = Pfedit.get_current_context () in
+ Printer.pr_glob_constr_env env (fst (fst ge))
let pr_constr_expr_with_bindings prc _ _ (ge : constr_expr_with_bindings) = prc (fst ge)
let interp_glob_constr_with_bindings ist gl c = Tacmach.project gl , (ist, c)
let glob_glob_constr_with_bindings ist l = Tacintern.intern_constr_with_bindings ist l
@@ -272,5 +276,7 @@ TACTIC EXTEND setoid_transitivity
END
VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY
- [ "Print" "Rewrite" "HintDb" preident(s) ] -> [ Feedback.msg_notice (Autorewrite.print_rewrite_hintdb s) ]
+ [ "Print" "Rewrite" "HintDb" preident(s) ] ->
+ [ let sigma, env = Pfedit.get_current_context () in
+ Feedback.msg_notice (Autorewrite.print_rewrite_hintdb env sigma s) ]
END
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 38460c669..d70751245 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -84,6 +84,14 @@ type 'a extra_genarg_printer =
(tolerability -> Val.t -> Pp.t) ->
'a -> Pp.t
+let string_of_genarg_arg (ArgumentType arg) =
+ let rec aux : type a b c. (a, b, c) genarg_type -> string = function
+ | ListArg t -> aux t ^ "_list"
+ | OptArg t -> aux t ^ "_opt"
+ | PairArg (t1, t2) -> assert false (* No parsing/printing rule for it *)
+ | ExtraArg s -> ArgT.repr s in
+ aux arg
+
let keyword x = tag_keyword (str x)
let primitive x = tag_primitive (str x)
@@ -536,15 +544,24 @@ let pr_goal_selector ~toplevel s =
let pr_funvar n = spc () ++ Name.print n
- let pr_let_clause k pr (na,(bl,t)) =
+ let pr_let_clause k pr_gen pr_arg (na,(bl,t)) =
+ let pr = function
+ | TacGeneric arg ->
+ let name = string_of_genarg_arg (genarg_tag arg) in
+ if name = "unit" || name = "int" then
+ (* Hard-wired parsing rules *)
+ pr_gen arg
+ else
+ str name ++ str ":" ++ surround (pr_gen arg)
+ | _ -> pr_arg (TacArg (Loc.tag t)) in
hov 0 (keyword k ++ spc () ++ pr_lname na ++ prlist pr_funvar bl ++
- str " :=" ++ brk (1,1) ++ pr (TacArg (Loc.tag t)))
+ str " :=" ++ brk (1,1) ++ pr t)
- let pr_let_clauses recflag pr = function
+ let pr_let_clauses recflag pr_gen pr = function
| hd::tl ->
hv 0
- (pr_let_clause (if recflag then "let rec" else "let") pr hd ++
- prlist (fun t -> spc () ++ pr_let_clause "with" pr t) tl)
+ (pr_let_clause (if recflag then "let rec" else "let") pr_gen pr hd ++
+ prlist (fun t -> spc () ++ pr_let_clause "with" pr_gen pr t) tl)
| [] -> anomaly (Pp.str "LetIn must declare at least one binding.")
let pr_seq_body pr tl =
@@ -858,7 +875,7 @@ let pr_goal_selector ~toplevel s =
let llc = List.map (fun (id,t) -> (id,extract_binders t)) llc in
v 0
(hv 0 (
- pr_let_clauses recflag (pr_tac ltop) llc
+ pr_let_clauses recflag pr.pr_generic (pr_tac ltop) llc
++ spc () ++ keyword "in"
) ++ fnl () ++ pr_tac (llet,E) u),
llet
@@ -1003,7 +1020,7 @@ let pr_goal_selector ~toplevel s =
| TacAtom (loc,t) ->
pr_with_comments ?loc (hov 1 (pr_atom pr strip_prod_binders tag_atom t)), ltatom
| TacArg(_,Tacexp e) ->
- pr.pr_tactic (latom,E) e, latom
+ pr_tac inherited e, latom
| TacArg(_,ConstrMayEval (ConstrTerm c)) ->
keyword "constr:" ++ pr.pr_constr c, latom
| TacArg(_,ConstrMayEval c) ->
@@ -1226,6 +1243,15 @@ let make_constr_printer f c =
let lift f a = Genprint.PrinterBasic (fun () -> f a)
+
+let pr_glob_constr_pptac c =
+ let _, env = Pfedit.get_current_context () in
+ pr_glob_constr_env env c
+
+let pr_lglob_constr_pptac c =
+ let _, env = Pfedit.get_current_context () in
+ pr_lglob_constr_env env c
+
let () =
let pr_bool b = if b then str "true" else str "false" in
let pr_unit _ = str "()" in
@@ -1240,7 +1266,7 @@ let () =
Genprint.register_print0
wit_intro_pattern
(Miscprint.pr_intro_pattern pr_constr_expr)
- (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c))
+ (Miscprint.pr_intro_pattern (fun (c, _) -> pr_glob_constr_pptac c))
pr_intro_pattern_env;
Genprint.register_print0
wit_clause_dft_concl
@@ -1251,45 +1277,45 @@ let () =
Genprint.register_print0
wit_constr
Ppconstr.pr_constr_expr
- (fun (c, _) -> Printer.pr_glob_constr c)
+ (fun (c, _) -> pr_glob_constr_pptac c)
(make_constr_printer Printer.pr_econstr_n_env)
;
Genprint.register_print0
wit_uconstr
Ppconstr.pr_constr_expr
- (fun (c,_) -> Printer.pr_glob_constr c)
+ (fun (c, _) -> pr_glob_constr_pptac c)
(make_constr_printer Printer.pr_closed_glob_n_env)
;
Genprint.register_print0
wit_open_constr
Ppconstr.pr_constr_expr
- (fun (c, _) -> Printer.pr_glob_constr c)
+ (fun (c, _) -> pr_glob_constr_pptac c)
(make_constr_printer Printer.pr_econstr_n_env)
;
Genprint.register_print0 wit_red_expr
(pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr))
- (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_and_constr_expr pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr))
+ (pr_red_expr (pr_and_constr_expr pr_glob_constr_pptac, pr_and_constr_expr pr_lglob_constr_pptac, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr_pptac))
pr_red_expr_env
;
Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis (lift pr_quantified_hypothesis);
Genprint.register_print0 wit_bindings
(Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr)
- (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
+ (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))
pr_bindings_env
;
Genprint.register_print0 wit_constr_with_bindings
(pr_with_bindings pr_constr_expr pr_lconstr_expr)
- (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
+ (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))
pr_with_bindings_env
;
Genprint.register_print0 wit_open_constr_with_bindings
(pr_with_bindings pr_constr_expr pr_lconstr_expr)
- (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
+ (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))
pr_with_bindings_env
;
Genprint.register_print0 Tacarg.wit_destruction_arg
(pr_destruction_arg pr_constr_expr pr_lconstr_expr)
- (pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
+ (pr_destruction_arg (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))
pr_destruction_arg_env
;
Genprint.register_print0 Stdarg.wit_int int int (lift int);
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 180fb2db4..918d1faeb 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -91,9 +91,10 @@ let subst_global_reference subst =
let subst_global ref =
let ref',t' = subst_global subst ref in
if not (is_global ref' t') then
- Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++
- str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++
- pr_global ref') ;
+ (let sigma, env = Pfedit.get_current_context () in
+ Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++
+ str " expanded to \"" ++ pr_lconstr_env env sigma t' ++ str "\", but to " ++
+ pr_global ref'));
ref'
in
subst_or_var (subst_located subst_global)
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index a669692fc..2dd7c9a74 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -20,7 +20,9 @@ let prmatchpatt env sigma hyp =
Pptactic.pr_match_pattern (Printer.pr_constr_pattern_env env sigma) hyp
let prmatchrl rl =
Pptactic.pr_match_rule false (Pptactic.pr_glob_tactic (Global.env()))
- (fun (_,p) -> Printer.pr_constr_pattern p) rl
+ (fun (_,p) ->
+ let sigma, env = Pfedit.get_current_context () in
+ Printer.pr_constr_pattern_env env sigma p) rl
(* This module intends to be a beginning of debugger for tactic expressions.
Currently, it is quite simple and we can hope to have, in the future, a more
@@ -369,7 +371,8 @@ let explain_ltac_call_trace last trace loc =
strbrk " (with " ++
prlist_with_sep pr_comma
(fun (id,c) ->
- Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders c)
+ let sigma, env = Pfedit.get_current_context () in
+ Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders_env env sigma c)
(List.rev (Id.Map.bindings vars)) ++ str ")"
else mt())
in
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 218342efe..cb54cac3f 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -984,7 +984,9 @@ struct
let parse_expr sigma parse_constant parse_exp ops_spec env term =
if debug
- then Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr term);
+ then (
+ let _, env = Pfedit.get_current_context () in
+ Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env env sigma term));
(*
let constant_or_variable env term =
@@ -1103,9 +1105,10 @@ struct
| _ -> raise ParseError
- let rconstant sigma term =
+ let rconstant sigma term =
+ let _, env = Pfedit.get_current_context () in
if debug
- then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.pr_leconstr term ++ fnl ());
+ then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.pr_leconstr_env env sigma term ++ fnl ());
let res = rconstant sigma term in
if debug then
(Printf.printf "rconstant -> %a\n" pp_Rcst res ; flush stdout) ;
@@ -1145,9 +1148,9 @@ struct
let parse_arith parse_op parse_expr env cstr gl =
let sigma = gl.sigma in
- if debug
- then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr cstr ++ fnl ());
- match EConstr.kind sigma cstr with
+ if debug
+ then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr_env gl.env sigma cstr ++ fnl ());
+ match EConstr.kind sigma cstr with
| Term.App(op,args) ->
let (op,lhs,rhs) = parse_op gl (op,args) in
let (e1,env) = parse_expr sigma env lhs in
@@ -1908,7 +1911,7 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2
let formula_typ = (EConstr.mkApp(Lazy.force coq_Cstr, [|spec.coeff|])) in
let ff = dump_formula formula_typ
(dump_cstr spec.typ spec.dump_coeff) ff in
- Feedback.msg_notice (Printer.pr_leconstr ff);
+ Feedback.msg_notice (Printer.pr_leconstr_env gl.env gl.sigma ff);
Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff
end;
@@ -1932,9 +1935,9 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2
Feedback.msg_notice (Pp.str "\nAFormula\n") ;
let formula_typ = (EConstr.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in
let ff' = dump_formula formula_typ
- (dump_cstr spec.typ spec.dump_coeff) ff' in
- Feedback.msg_notice (Printer.pr_leconstr ff');
- Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff'
+ (dump_cstr spec.typ spec.dump_coeff) ff' in
+ Feedback.msg_notice (Printer.pr_leconstr_env gl.env gl.sigma ff');
+ Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff'
end;
(* Even if it does not work, this does not mean it is not provable
diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml
index 7da4a3b82..52c6ef983 100644
--- a/plugins/micromega/micromega.ml
+++ b/plugins/micromega/micromega.ml
@@ -981,8 +981,8 @@ let rec or_cnf unsat deduce f f' =
(** val and_cnf : 'a1 cnf -> 'a1 cnf -> 'a1 cnf **)
-let and_cnf f1 f2 =
- app f1 f2
+let and_cnf =
+ app
(** val xcnf :
('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1
@@ -1204,22 +1204,22 @@ type 't formula = { flhs : 't pExpr; fop : op2; frhs : 't pExpr }
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
-> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol **)
-let norm cO cI cplus ctimes cminus copp ceqb =
- norm_aux cO cI cplus ctimes cminus copp ceqb
+let norm =
+ norm_aux
(** val psub0 :
'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1
-> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **)
-let psub0 cO cplus cminus copp ceqb =
- psub cO cplus cminus copp ceqb
+let psub0 =
+ psub
(** val padd0 :
'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol
-> 'a1 pol **)
-let padd0 cO cplus ceqb =
- padd cO cplus ceqb
+let padd0 =
+ padd
(** val xnormalise :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 430b608f4..54ff44fbd 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -183,8 +183,9 @@ let print_env_reification env =
let rec loop c i = function
[] -> str " ===============================\n\n"
| t :: l ->
+ let sigma, env = Pfedit.get_current_context () in
let s = Printf.sprintf "(%c%02d)" c i in
- spc () ++ str s ++ str " := " ++ Printer.pr_lconstr t ++ fnl () ++
+ spc () ++ str s ++ str " := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++
loop c (succ i) l
in
let prop_info = str "ENVIRONMENT OF PROPOSITIONS :" ++ fnl () ++ loop 'P' 0 env.props in
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index 05ab8ab32..a7d6d5bb2 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -82,10 +82,11 @@ VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF
| [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [
Feedback.msg_notice (strbrk "The following ring structures have been declared:");
Spmap.iter (fun fn fi ->
+ let sigma, env = Pfedit.get_current_context () in
Feedback.msg_notice (hov 2
(Ppconstr.pr_id (Libnames.basename fn)++spc()++
- str"with carrier "++ pr_constr fi.ring_carrier++spc()++
- str"and equivalence relation "++ pr_constr fi.ring_req))
+ str"with carrier "++ pr_constr_env env sigma fi.ring_carrier++spc()++
+ str"and equivalence relation "++ pr_constr_env env sigma fi.ring_req))
) !from_name ]
END
@@ -117,10 +118,11 @@ VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF
| [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [
Feedback.msg_notice (strbrk "The following field structures have been declared:");
Spmap.iter (fun fn fi ->
+ let sigma, env = Pfedit.get_current_context () in
Feedback.msg_notice (hov 2
(Ppconstr.pr_id (Libnames.basename fn)++spc()++
- str"with carrier "++ pr_constr fi.field_carrier++spc()++
- str"and equivalence relation "++ pr_constr fi.field_req))
+ str"with carrier "++ pr_constr_env env sigma fi.field_carrier++spc()++
+ str"and equivalence relation "++ pr_constr_env env sigma fi.field_req))
) !field_from_name ]
END
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 9e4b896f8..1c3bdb958 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -344,8 +344,6 @@ let _ = add_map "ring"
(****************************************************************************)
(* Ring database *)
-let pr_constr c = pr_econstr c
-
module Cmap = Map.Make(Constr)
let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table"
@@ -368,7 +366,7 @@ let find_ring_structure env sigma l =
with Not_found ->
CErrors.user_err ~hdr:"ring"
(str"cannot find a declared ring structure over"++
- spc()++str"\""++pr_constr ty++str"\""))
+ spc() ++ str"\"" ++ pr_econstr_env env sigma ty ++ str"\""))
| [] -> assert false
let add_entry (sp,_kn) e =
@@ -529,19 +527,19 @@ let ring_equality env evd (r,add,mul,opp,req) =
op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in
Flags.if_verbose
Feedback.msg_info
- (str"Using setoid \""++pr_constr req++str"\""++spc()++
- str"and morphisms \""++pr_constr add_m_lem ++
- str"\","++spc()++ str"\""++pr_constr mul_m_lem++
- str"\""++spc()++str"and \""++pr_constr opp_m_lem++
+ (str"Using setoid \""++ pr_econstr_env env !evd req++str"\""++spc()++
+ str"and morphisms \""++pr_econstr_env env !evd add_m_lem ++
+ str"\","++spc()++ str"\""++pr_econstr_env env !evd mul_m_lem++
+ str"\""++spc()++str"and \""++pr_econstr_env env !evd opp_m_lem++
str"\"");
op_morph)
| None ->
(Flags.if_verbose
Feedback.msg_info
- (str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++
- str"and morphisms \""++pr_constr add_m_lem ++
+ (str"Using setoid \""++pr_econstr_env env !evd req ++str"\"" ++ spc() ++
+ str"and morphisms \""++pr_econstr_env env !evd add_m_lem ++
str"\""++spc()++str"and \""++
- pr_constr mul_m_lem++str"\"");
+ pr_econstr_env env !evd mul_m_lem++str"\"");
op_smorph r add mul req add_m_lem mul_m_lem) in
(setoid,op_morph)
@@ -861,7 +859,7 @@ let find_field_structure env sigma l =
with Not_found ->
CErrors.user_err ~hdr:"field"
(str"cannot find a declared field structure over"++
- spc()++str"\""++pr_constr ty++str"\""))
+ spc()++str"\""++pr_econstr_env env sigma ty++str"\""))
| [] -> assert false
let add_field_entry (sp,_kn) e =
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index c1d7e6278..83b454769 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -240,7 +240,7 @@ let interp_refine ist gl rc =
in
let sigma, c = Pretyping.understand_ltac flags (pf_env gl) (project gl) vars kind rc in
(* ppdebug(lazy(str"sigma@interp_refine=" ++ pr_evar_map None sigma)); *)
- ppdebug(lazy(str"c@interp_refine=" ++ Printer.pr_econstr c));
+ ppdebug(lazy(str"c@interp_refine=" ++ Printer.pr_econstr_env (pf_env gl) sigma c));
(sigma, (sigma, c))
@@ -539,7 +539,7 @@ module Intset = Evar.Set
let pf_abs_evars_pirrel gl (sigma, c0) =
pp(lazy(str"==PF_ABS_EVARS_PIRREL=="));
- pp(lazy(str"c0= " ++ Printer.pr_constr c0));
+ pp(lazy(str"c0= " ++ Printer.pr_constr_env (pf_env gl) sigma c0));
let sigma0 = project gl in
let c0 = nf_evar sigma0 (nf_evar sigma c0) in
let nenv = env_size (pf_env gl) in
@@ -563,7 +563,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) =
| _ -> Constr.fold put evlist c in
let evlist = put [] c0 in
if evlist = [] then 0, c0 else
- let pr_constr t = Printer.pr_econstr (Reductionops.nf_beta (project gl) (EConstr.of_constr t)) in
+ let pr_constr t = Printer.pr_econstr_env (pf_env gl) sigma (Reductionops.nf_beta (project gl) (EConstr.of_constr t)) in
pp(lazy(str"evlist=" ++ pr_list (fun () -> str";")
(fun (k,_) -> str(Evd.string_of_existential k)) evlist));
let evplist =
@@ -959,7 +959,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl =
loop (meta_declare m (EConstr.Unsafe.to_constr ty) sigma) bo ((EConstr.mkMeta m)::args) (n-1)
| _ -> assert false
in loop sigma t [] n in
- pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr t));
+ pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t));
Tacmach.refine_no_check t gl
let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl =
@@ -973,7 +973,7 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl =
compose_lam (let xs,y = List.chop (n-1) l in y @ xs)
(mkApp (compose_lam l c, Array.of_list (mkRel 1 :: mkRels n)))
in
- pp(lazy(str"after: " ++ Printer.pr_constr oc));
+ pp(lazy(str"after: " ++ Printer.pr_constr_env (pf_env gl) (project gl) oc));
try applyn ~with_evars ~with_shelve:true ?beta n (EConstr.of_constr oc) gl
with e when CErrors.noncritical e -> raise dependent_apply_error
@@ -1202,7 +1202,7 @@ let genclrtac cl cs clr =
let gentac ist gen gl =
(* ppdebug(lazy(str"sigma@gentac=" ++ pr_evar_map None (project gl))); *)
let conv, _, cl, c, clr, ucst,gl = pf_interp_gen_aux ist gl false gen in
- ppdebug(lazy(str"c@gentac=" ++ pr_econstr c));
+ ppdebug(lazy(str"c@gentac=" ++ pr_econstr_env (pf_env gl) (project gl) c));
let gl = pf_merge_uc ucst gl in
if conv
then tclTHEN (Proofview.V82.of_tactic (convert_concl cl)) (cleartac clr) gl
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 26b5c5767..4e0b44a44 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -46,7 +46,7 @@ let analyze_eliminator elimty env sigma =
if not (EConstr.eq_constr sigma t t') then loop ctx t' else
errorstrm Pp.(str"The eliminator has the wrong shape."++spc()++
str"A (applied) bound variable was expected as the conclusion of "++
- str"the eliminator's"++Pp.cut()++str"type:"++spc()++pr_econstr elimty) in
+ str"the eliminator's"++Pp.cut()++str"type:"++spc()++pr_econstr_env env' sigma elimty) in
let ctx, pred_id, elim_is_dep, n_pred_args,concl = loop [] elimty in
let n_elim_args = Context.Rel.nhyps ctx in
let is_rec_elim =
@@ -126,7 +126,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) ?ist deps what ?elim eqid elim_intr
ppdebug(lazy Pp.(str"matching: " ++ pr_occ occ ++ pp_pattern p));
let (c,ucst), cl =
fill_occ_pattern ~raise_NoMatch:true env sigma0 (EConstr.Unsafe.to_constr cl) p occ h in
- ppdebug(lazy Pp.(str" got: " ++ pr_constr c));
+ ppdebug(lazy Pp.(str" got: " ++ pr_constr_env env sigma0 c));
c, EConstr.of_constr cl, ucst in
let mkTpat gl t = (* takes a term, refreshes it and makes a T pattern *)
let n, t, _, ucst = pf_abs_evars orig_gl (project gl, fire_subst gl t) in
@@ -239,8 +239,8 @@ let ssrelim ?(ind=ref None) ?(is_case=false) ?ist deps what ?elim eqid elim_intr
| Some (c, _, _,gl) -> true, gl
| None ->
errorstrm Pp.(str"Unable to apply the eliminator to the term"++
- spc()++pr_econstr c++spc()++str"or to unify it's type with"++
- pr_econstr inf_arg_ty) in
+ spc()++pr_econstr_env env (project gl) c++spc()++str"or to unify it's type with"++
+ pr_econstr_env env (project gl) inf_arg_ty) in
ppdebug(lazy Pp.(str"c_is_head_p= " ++ bool c_is_head_p));
let gl, predty = pfe_type_of gl pred in
(* Patterns for the inductive types indexes to be bound in pred are computed
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index e82f222b9..274c7110c 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -77,7 +77,7 @@ let interp_congrarg_at ist gl n rf ty m =
if i + n > m then None else
try
let rt = mkRApp congrn (args1 @ mkRApp rf (mkRHoles i) :: args2) in
- ppdebug(lazy Pp.(str"rt=" ++ Printer.pr_glob_constr rt));
+ ppdebug(lazy Pp.(str"rt=" ++ Printer.pr_glob_constr_env (pf_env gl) rt));
Some (interp_refine ist gl rt)
with _ -> loop (i + 1) in
loop 0
@@ -86,7 +86,7 @@ let pattern_id = mk_internal_id "pattern value"
let congrtac ((n, t), ty) ist gl =
ppdebug(lazy (Pp.str"===congr==="));
- ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr (Tacmach.pf_concl gl)));
+ ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (Tacmach.pf_concl gl)));
let sigma, _ as it = interp_term ist gl t in
let gl = pf_merge_uc_of sigma gl in
let _, f, _, _ucst = pf_abs_evars gl it in
@@ -109,7 +109,7 @@ let congrtac ((n, t), ty) ist gl =
let newssrcongrtac arg ist gl =
ppdebug(lazy Pp.(str"===newcongr==="));
- ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr (pf_concl gl)));
+ ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (pf_concl gl)));
(* utils *)
let fs gl t = Reductionops.nf_evar (project gl) t in
let tclMATCH_GOAL (c, gl_c) proj t_ok t_fail gl =
@@ -247,7 +247,7 @@ let unfoldintac occ rdx t (kt,_) gl =
try find_T env c h ~k:(fun env c _ _ -> EConstr.Unsafe.to_constr (body env t (EConstr.of_constr c)))
with NoMatch when easy -> c
| NoMatch | NoProgress -> errorstrm Pp.(str"No occurrence of "
- ++ pr_constr_pat (EConstr.Unsafe.to_constr t) ++ spc() ++ str "in " ++ Printer.pr_constr c)),
+ ++ pr_constr_pat (EConstr.Unsafe.to_constr t) ++ spc() ++ str "in " ++ Printer.pr_constr_env env sigma c)),
(fun () -> try end_T () with
| NoMatch when easy -> fake_pmatcher_end ()
| NoMatch -> anomaly "unfoldintac")
@@ -267,13 +267,13 @@ let unfoldintac occ rdx t (kt,_) gl =
| Proj _ when same_proj sigma0 c t -> body env t c
| Const f -> aux (body env c c)
| App (f, a) -> aux (EConstr.mkApp (body env f f, a))
- | _ -> errorstrm Pp.(str "The term "++pr_constr orig_c++
- str" contains no " ++ pr_econstr t ++ str" even after unfolding")
+ | _ -> errorstrm Pp.(str "The term "++ pr_constr_env env sigma orig_c++
+ str" contains no " ++ pr_econstr_env env sigma t ++ str" even after unfolding")
in EConstr.Unsafe.to_constr @@ aux (EConstr.of_constr c)
else
try EConstr.Unsafe.to_constr @@ body env t (fs (unify_HO env sigma (EConstr.of_constr c) t) t)
with _ -> errorstrm Pp.(str "The term " ++
- pr_constr c ++spc()++ str "does not unify with " ++ pr_constr_pat (EConstr.Unsafe.to_constr t))),
+ pr_constr_env env sigma c ++spc()++ str "does not unify with " ++ pr_constr_pat (EConstr.Unsafe.to_constr t))),
fake_pmatcher_end in
let concl =
let concl0 = EConstr.Unsafe.to_constr concl0 in
@@ -352,7 +352,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
(* We check the proof is well typed *)
let sigma, proof_ty =
try Typing.type_of env sigma proof with _ -> raise PRtype_error in
- ppdebug(lazy Pp.(str"pirrel_rewrite proof term of type: " ++ pr_econstr proof_ty));
+ ppdebug(lazy Pp.(str"pirrel_rewrite proof term of type: " ++ pr_econstr_env env sigma proof_ty));
try refine_with
~first_goes_last:(not !ssroldreworder) ~with_evars:false (sigma, proof) gl
with _ ->
@@ -374,8 +374,8 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
if open_evs <> [] then Some name else None)
(List.combine (Array.to_list args) names)
| _ -> anomaly "rewrite rule not an application" in
- errorstrm Pp.(Himsg.explain_refiner_error (Logic.UnresolvedBindings miss)++
- (Pp.fnl()++str"Rule's type:" ++ spc() ++ pr_econstr hd_ty))
+ errorstrm Pp.(Himsg.explain_refiner_error env sigma (Logic.UnresolvedBindings miss)++
+ (Pp.fnl()++str"Rule's type:" ++ spc() ++ pr_econstr_env env sigma hd_ty))
;;
let is_construct_ref sigma c r =
@@ -391,12 +391,12 @@ let rwcltac cl rdx dir sr gl =
let gl = pf_unsafe_merge_uc ucst gl in
let rdxt = Retyping.get_type_of (pf_env gl) (fst sr) rdx in
(* ppdebug(lazy(str"sigma@rwcltac=" ++ pr_evar_map None (fst sr))); *)
- ppdebug(lazy Pp.(str"r@rwcltac=" ++ pr_econstr (snd sr)));
+ ppdebug(lazy Pp.(str"r@rwcltac=" ++ pr_econstr_env (pf_env gl) (project gl) (snd sr)));
let cvtac, rwtac, gl =
if EConstr.Vars.closed0 (project gl) r' then
let env, sigma, c, c_eq = pf_env gl, fst sr, snd sr, Coqlib.build_coq_eq () in
let sigma, c_ty = Typing.type_of env sigma c in
- ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr c_ty));
+ ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty));
match EConstr.kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with
| AtomicType(e, a) when is_ind_ref sigma e c_eq ->
let new_rdx = if dir = L2R then a.(2) else a.(1) in
@@ -411,7 +411,7 @@ let rwcltac cl rdx dir sr gl =
let r3, _, r3t =
try EConstr.destCast (project gl) r2 with _ ->
errorstrm Pp.(str "no cast from " ++ pr_constr_pat (EConstr.Unsafe.to_constr (snd sr))
- ++ str " to " ++ pr_econstr r2) in
+ ++ str " to " ++ pr_econstr_env (pf_env gl) (project gl) r2) in
let cl' = EConstr.mkNamedProd rule_id (EConstr.it_mkProd_or_LetIn r3t dc) (EConstr.Vars.lift 1 cl) in
let cl'' = EConstr.mkNamedProd pattern_id rdxt cl' in
let itacs = [introid pattern_id; introid rule_id] in
@@ -605,7 +605,7 @@ let ssrinstancesofrule ist dir arg gl =
sigma, pats @ [pat] in
let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in
mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true sigma0 None ~upats_origin rpats in
- let print env p c _ = Feedback.msg_info Pp.(hov 1 (str"instance:" ++ spc() ++ pr_constr p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr c)); c in
+ let print env p c _ = Feedback.msg_info Pp.(hov 1 (str"instance:" ++ spc() ++ pr_constr_env env r_sigma p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr_env env r_sigma c)); c in
Feedback.msg_info Pp.(str"BEGIN INSTANCES");
try
while true do
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 29e96ec59..a707226cd 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -72,13 +72,14 @@ let examine_abstract id gl =
let gl, tid = pfe_type_of gl id in
let abstract, gl = pf_mkSsrConst "abstract" gl in
let sigma = project gl in
+ let env = pf_env gl in
if not (EConstr.isApp sigma tid) || not (EConstr.eq_constr sigma (fst(EConstr.destApp sigma tid)) abstract) then
- errorstrm(strbrk"not an abstract constant: "++pr_econstr id);
+ errorstrm(strbrk"not an abstract constant: "++ pr_econstr_env env sigma id);
let _, args_id = EConstr.destApp sigma tid in
if Array.length args_id <> 3 then
- errorstrm(strbrk"not a proper abstract constant: "++pr_econstr id);
+ errorstrm(strbrk"not a proper abstract constant: "++ pr_econstr_env env sigma id);
if not (is_Evar_or_CastedMeta sigma args_id.(2)) then
- errorstrm(strbrk"abstract constant "++pr_econstr id++str" already used");
+ errorstrm(strbrk"abstract constant "++ pr_econstr_env env sigma id++str" already used");
tid, args_id
let pf_find_abstract_proof check_lock gl abstract_n =
@@ -94,7 +95,7 @@ let pf_find_abstract_proof check_lock gl abstract_n =
| _ -> l) (project gl) [] in
match l with
| [e] -> e
- | _ -> errorstrm(strbrk"abstract constant "++pr_constr abstract_n++
+ | _ -> errorstrm(strbrk"abstract constant "++ pr_constr_env (pf_env gl) (project gl) abstract_n ++
strbrk" not found in the evar map exactly once. "++
strbrk"Did you tamper with it?")
@@ -205,7 +206,7 @@ let havetac ist
let assert_is_conv gl =
try Proofview.V82.of_tactic (convert_concl (EConstr.it_mkProd_or_LetIn concl ctx)) gl
with _ -> errorstrm (str "Given proof term is not of type " ++
- pr_econstr (EConstr.mkArrow (EConstr.mkVar (Id.of_string "_")) concl)) in
+ pr_econstr_env (pf_env gl) (project gl) (EConstr.mkArrow (EConstr.mkVar (Id.of_string "_")) concl)) in
gl, ty, Tacticals.tclTHEN assert_is_conv (Proofview.V82.of_tactic (Tactics.apply t)), id, itac_c
| FwdHave, false, false ->
let skols = List.flatten (List.map (function
@@ -271,7 +272,7 @@ let ssrabstract ist gens (*last*) gl =
let gl, proof =
let pf_unify_HO gl a b =
try pf_unify_HO gl a b
- with _ -> errorstrm(strbrk"The abstract variable "++pr_econstr id++
+ with _ -> errorstrm(strbrk"The abstract variable "++ pr_econstr_env env (project gl) id++
strbrk" cannot abstract this goal. Did you generalize it?") in
let find_hole p t =
match EConstr.kind (project gl) t with
@@ -290,7 +291,7 @@ let ssrabstract ist gens (*last*) gl =
| App(hd, [|left; right|]) when Term.Constr.equal hd prod ->
find_hole (mkApp (proj1,[|left;right;p|])) left
*)
- | _ -> errorstrm(strbrk"abstract constant "++pr_econstr abstract_n++
+ | _ -> errorstrm(strbrk"abstract constant "++ pr_econstr_env env (project gl) abstract_n++
strbrk" has an unexpected shape. Did you tamper with it?")
in
find_hole
@@ -361,14 +362,14 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
| Sort _, [] -> EConstr.Vars.subst_vars s ct
| LetIn(Name id as n,b,ty,c), _::g -> EConstr.mkLetIn (n,b,ty,var2rel c g (id::s))
| Prod(Name id as n,ty,c), _::g -> EConstr.mkProd (n,ty,var2rel c g (id::s))
- | _ -> CErrors.anomaly(str"SSR: wlog: var2rel: " ++ pr_econstr c) in
+ | _ -> CErrors.anomaly(str"SSR: wlog: var2rel: " ++ pr_econstr_env env sigma c) in
let c = var2rel c gens [] in
let rec pired c = function
| [] -> c
| t::ts as args -> match EConstr.kind sigma c with
| Prod(_,_,c) -> pired (EConstr.Vars.subst1 t c) ts
| LetIn(id,b,ty,c) -> EConstr.mkLetIn (id,b,ty,pired c args)
- | _ -> CErrors.anomaly(str"SSR: wlog: pired: " ++ pr_econstr c) in
+ | _ -> CErrors.anomaly(str"SSR: wlog: pired: " ++ pr_econstr_env env sigma c) in
c, args, pired c args, pf_merge_uc uc gl in
let tacipat pats = introstac ~ist pats in
let tacigens =
@@ -396,8 +397,8 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
| Some id ->
if pats = [] then Tacticals.tclIDTAC else
let args = Array.of_list args in
- ppdebug(lazy(str"specialized="++pr_econstr EConstr.(mkApp (mkVar id,args))));
- ppdebug(lazy(str"specialized_ty="++pr_econstr ct));
+ ppdebug(lazy(str"specialized="++ pr_econstr_env (pf_env gl) (project gl) EConstr.(mkApp (mkVar id,args))));
+ ppdebug(lazy(str"specialized_ty="++ pr_econstr_env (pf_env gl) (project gl) ct));
Tacticals.tclTHENS (basecuttac "ssr_have" ct)
[Proofview.V82.of_tactic (Tactics.apply EConstr.(mkApp (mkVar id,args))); Tacticals.tclIDTAC] in
"ssr_have",
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 023778fdb..6c325cce4 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -272,7 +272,7 @@ let (introstac : ?ist:Tacinterp.interp_sign -> ssripats -> Tacmach.tactic),
let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr gl =
(* Utils of local interest only *)
let iD s ?t gl = let t = match t with None -> pf_concl gl | Some x -> x in
- ppdebug(lazy Pp.(str s ++ pr_econstr t)); Tacticals.tclIDTAC gl in
+ ppdebug(lazy Pp.(str s ++ pr_econstr_env (pf_env gl) (project gl) t)); Tacticals.tclIDTAC gl in
let protectC, gl = pf_mkSsrConst "protect_term" gl in
let eq, gl = pf_fresh_global (Coqlib.build_coq_eq ()) gl in
let eq = EConstr.of_constr eq in
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 7b591fead..46403aef3 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -1131,7 +1131,7 @@ let pr_fwd_guarded prval prval' = function
| (fk, h), (_, (_, Some c)) ->
pr_gen_fwd prval pr_constr_expr prl_constr_expr fk (format_constr_expr h c)
| (fk, h), (_, (c, None)) ->
- pr_gen_fwd prval' pr_glob_constr prl_glob_constr fk (format_glob_constr h c)
+ pr_gen_fwd prval' pr_glob_constr_env prl_glob_constr fk (format_glob_constr h c)
let pr_unguarded prc prlc = prlc
diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml
index e865ef706..4b2fab6d1 100644
--- a/plugins/ssr/ssrprinters.ml
+++ b/plugins/ssr/ssrprinters.ml
@@ -24,7 +24,7 @@ let pp_concat hd ?(sep=str", ") = function [] -> hd | x :: xs ->
hd ++ List.fold_left (fun acc x -> acc ++ sep ++ x) x xs
let pp_term gl t =
- let t = Reductionops.nf_evar (project gl) t in pr_econstr t
+ let t = Reductionops.nf_evar (project gl) t in pr_econstr_env (pf_env gl) (project gl) t
(* FIXME *)
(* terms are pre constr, the kind is parsing/printing flag to distinguish
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 36dce37ae..cd614fee9 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -343,7 +343,7 @@ let coerce_search_pattern_to_sort hpat =
let hpat' = if np = na then hpat else mkPApp hpat (np - na) [||] in
let warn () =
Feedback.msg_warning (str "Listing only lemmas with conclusion matching " ++
- pr_constr_pattern hpat') in
+ pr_constr_pattern_env env sigma hpat') in
if EConstr.isSort sigma ht then begin warn (); true, hpat' end else
let filter_head, coe_path =
try
@@ -359,7 +359,7 @@ let coerce_search_pattern_to_sort hpat =
let n_imps = Option.get (Classops.hide_coercion coe_ref) in
mkPApp (Pattern.PRef coe_ref) n_imps [|hp|]
with _ ->
- errorstrm (str "need explicit coercion " ++ pr_constr coe ++ spc ()
+ errorstrm (str "need explicit coercion " ++ pr_constr_env env sigma coe ++ spc ()
++ str "to interpret head search pattern as type") in
filter_head, List.fold_left coerce hpat' coe_path
@@ -468,10 +468,12 @@ let pr_raw_ssrhintref prc _ _ = let open CAst in function
prc c ++ str "|" ++ int (List.length args)
| c -> prc c
-let pr_rawhintref c = match DAst.get c with
+let pr_rawhintref c =
+ let _, env = Pfedit.get_current_context () in
+ match DAst.get c with
| GApp (f, args) when isRHoles args ->
- pr_glob_constr f ++ str "|" ++ int (List.length args)
- | _ -> pr_glob_constr c
+ pr_glob_constr_env env f ++ str "|" ++ int (List.length args)
+ | _ -> pr_glob_constr_env env c
let pr_glob_ssrhintref _ _ _ (c, _) = pr_rawhintref c
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index d5c9e4988..276b7c8ab 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -100,7 +100,6 @@ let pr_guarded guard prc c =
let s = Pp.string_of_ppcmds (prc c) ^ "$" in
if guard s (skip_wschars s 0) then pr_paren prc c else prc c
(* More sensible names for constr printers *)
-let pr_constr = pr_constr
let prl_glob_constr c = pr_lglob_constr_env (Global.env ()) c
let pr_glob_constr c = pr_glob_constr_env (Global.env ()) c
let prl_constr_expr = pr_lconstr_expr
@@ -427,7 +426,8 @@ let hole_var = mkVar (Id.of_string "_")
let pr_constr_pat c0 =
let rec wipe_evar c =
if isEvar c then hole_var else map wipe_evar c in
- pr_constr (wipe_evar c0)
+ let sigma, env = Pfedit.get_current_context () in
+ pr_constr_env env sigma (wipe_evar c0)
(* Turn (new) evars into metas *)
let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 =
@@ -1215,7 +1215,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst =
let pop_evar sigma e p =
let { Evd.evar_body = e_body } as e_def = Evd.find sigma e in
let e_body = match e_body with Evar_defined c -> c
- | _ -> errorstrm (str "Matching the pattern " ++ pr_constr p ++
+ | _ -> errorstrm (str "Matching the pattern " ++ pr_constr_env env0 sigma0 p ++
str " did not instantiate ?" ++ int (Evar.repr e) ++ spc () ++
str "Does the variable bound by the \"in\" construct occur "++
str "in the pattern?") in
@@ -1417,7 +1417,8 @@ let ssrinstancesof ist arg gl =
let find, conclude =
mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true
sigma None (etpat,[tpat]) in
- let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr c)); c in
+ let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr_env (pf_env gl) (gl.sigma) p ++ spc()
+ ++ str "matches:" ++ spc() ++ pr_constr_env (pf_env gl) (gl.sigma) c)); c in
ppnl (str"BEGIN INSTANCES");
try
while true do
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 19:36:03 +0000