From f40dc2a07fa9e4a600c8032ccf5d05e8ad68dba4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 25 Dec 2000 23:49:23 +0000
Subject: Command -> Constr

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1216 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/inv.mli | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/tactics/inv.mli b/tactics/inv.mli
index 39254c7637..f09744c566 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -3,6 +3,7 @@
 
 (*i*)
 open Names
+open Term
 open Tacmach
 (*i*)
 
@@ -12,8 +13,8 @@ val inv_clear_tac : identifier -> tactic
 val half_dinv_tac : identifier -> tactic
 val dinv_tac : identifier -> tactic
 val dinv_clear_tac : identifier -> tactic
-val half_dinv_with : identifier -> Coqast.t -> tactic
-val dinv_with : identifier -> Coqast.t -> tactic
-val dinv_clear_with : identifier -> Coqast.t -> tactic
+val half_dinv_with : identifier -> constr -> tactic
+val dinv_with : identifier -> constr -> tactic
+val dinv_clear_with : identifier -> constr -> tactic
 
 val invIn_tac : string -> identifier -> identifier list -> tactic
-- 
cgit v1.2.3