diff options
| author | Pierre-Marie Pédrot | 2020-09-30 14:05:08 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-30 14:05:08 +0200 |
| commit | 1c919ed6fa476f0f7a16d69e58989f3d75104910 (patch) | |
| tree | 3fd1b2452b9af72f0dc2cd1929683ec544372874 /proofs | |
| parent | c63f7c8407ae151e61e5490803bb19169ad37a5c (diff) | |
| parent | be3a5ac947cb57499b668a3745439b15ff8c48a8 (diff) | |
Merge PR #13021: Almost fully moving funind to new proof engine
Reviewed-by: ppedrot
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/tacmach.ml | 5 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 1 |
2 files changed, 5 insertions, 1 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index ecdbfa5118..1207e0e599 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -99,7 +99,7 @@ let db_pr_goal sigma g = str" " ++ pc) ++ fnl () let pr_gls gls = - hov 0 (pr_evar_map (Some 2) (pf_env gls) (sig_sig gls) ++ fnl () ++ db_pr_goal (project gls) (sig_it gls)) + hov 0 (pr_evar_map (Some 2) (pf_env gls) (project gls) ++ fnl () ++ db_pr_goal (project gls) (sig_it gls)) (* Variants of [Tacmach] functions built with the new proof engine *) module New = struct @@ -183,6 +183,9 @@ module New = struct let pf_unsafe_type_of gl t = pf_apply (unsafe_type_of[@warning "-3"]) gl t + let pr_gls gl = + hov 0 (pr_evar_map (Some 2) (pf_env gl) (project gl) ++ fnl () ++ db_pr_goal (project gl) (Proofview.Goal.goal gl)) + end (* deprecated *) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index d8f7b7eed8..08f88d46c1 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -126,4 +126,5 @@ module New : sig val pf_nf_evar : Proofview.Goal.t -> constr -> constr + val pr_gls : Proofview.Goal.t -> Pp.t end |