diff options
| author | Hugo Herbelin | 2020-09-13 14:37:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-09-29 22:24:02 +0200 |
| commit | 5cac24428e448c12ab292265bb2ffd1146b38c25 (patch) | |
| tree | 43713dc6730d53db67fa2a910650154dee1b91a1 /proofs | |
| parent | bee9998b0cde3c86888fcad8c0dccbeebb351032 (diff) | |
Almost fully moving funind to new proof engine.
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 |