From f0b1770c437df210bed1579aa6922141a4f4fd82 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 25 Dec 2000 21:12:46 +0000
Subject: Command -> Constr

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

diff --git a/tactics/inv.ml b/tactics/inv.ml
index 328d3bebd0..da43bd0eb2 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -458,11 +458,13 @@ let (half_dinv_with, dinv_with, dinv_clear_with) =
              fun gls -> 
 	       inv false (com_of_id ic)
 		 (Dep (Some (pf_interp_constr gls com))) id gls
+	 | [ic; Identifier id; Constr c] ->
+             fun gls -> inv false (com_of_id ic) (Dep (Some c)) id gls
 	 | _ -> anomaly "DInvWith called with bad args")
   in
-  ((fun id com -> gentac [hinv_kind; Identifier id; Command com]),
-   (fun id com -> gentac [inv_kind; Identifier id; Command com]),
-   (fun id com -> gentac [invclr_kind; Identifier id; Command com]))
+  ((fun id c -> gentac [hinv_kind; Identifier id; Constr c]),
+   (fun id c -> gentac [inv_kind; Identifier id; Constr c]),
+   (fun id c -> gentac [invclr_kind; Identifier id; Constr c]))
 
 (* InvIn will bring the specified clauses into the conclusion, and then
  * perform inversion on the named hypothesis.  After, it will intro them
-- 
cgit v1.2.3