From bd5689d4e9294d66b3eb4ecdc0af3ad7d65fe52d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 26 Oct 2018 10:05:58 +0200
Subject: [coqpp] [ltac] Adapt to removal of imperative proof state.

We add state handling to tactics.

TODO:

- [rewrite] `add_morphism_infer` creates problems as it opens a proof.
- [g_obligations] with_tac
---
 plugins/ltac/pptactic.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'plugins/ltac/pptactic.ml')

diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 1bdba699f7..80070a7493 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1307,7 +1307,6 @@ let lift_top f a = Genprint.TopPrinterBasic (fun () -> f a)
 let register_basic_print0 wit f g h =
   Genprint.register_print0 wit (lift f) (lift g) (lift_top h)
 
-
 let pr_glob_constr_pptac env sigma c =
   pr_glob_constr_env env c
 
-- 
cgit v1.2.3