diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index cce83cba06..b171aab6b7 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -280,7 +280,7 @@ let print_no_goal () = let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in assert (gls = []); let sigma = Tacmach.project (Tacmach.top_goal_of_pftreestate pfts) in - msg (Proof_trees.pr_subgoals_existential sigma gls) + msg (Printer.pr_subgoals sigma gls) type word_class = Normal | Kwd | Reserved |