Added the Ground tactic.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3955 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 3 deletions

diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index c11fd1699..ff735c9cd 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -176,10 +176,19 @@ let match_with_nottype t =
 
 let is_nottype t = op2bool (match_with_nottype t)
 		     
-let is_imp_term c = 
+let match_with_forall_term c=
   match kind_of_term c with
-    | Prod (_,_,b) -> not (dependent (mkRel 1) b)
-    | _              -> false
+    | Prod (nam,a,b) -> Some (nam,a,b)
+    | _            -> None
+
+let is_forall_term c = op2bool (match_with_forall_term c) 
+
+let match_with_imp_term c=
+  match kind_of_term c with
+    | Prod (_,a,b) when not (dependent (mkRel 1) b) ->Some (a,b)
+    | _              -> None
+
+let is_imp_term c = op2bool (match_with_imp_term c) 
 
 let rec has_nodep_prod_after n c =
   match kind_of_term c with