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/cc/ccalgo.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 978969bf59..5066c3931d 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -255,5 +255,3 @@ val find_contradiction : UF.t ->
   (Names.Id.t * (int * int)) list ->
   (Names.Id.t * (int * int))
 *)
-
-
-- 
cgit v1.2.3