From cb134451453a608cc486c1235fde2e08b7eab254 Mon Sep 17 00:00:00 2001
From: corbinea
Date: Sun, 25 May 2003 19:44:31 +0000
Subject: Ground and CCsolve updates

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4075 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/hipattern.ml  | 16 ++++++++++++++++
 tactics/hipattern.mli |  3 +++
 2 files changed, 19 insertions(+)

(limited to 'tactics')

diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index a9a8e432ab..6c4a01f262 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -223,6 +223,22 @@ let match_with_nodep_ind t =
 	  
 let is_nodep_ind t=op2bool (match_with_nodep_ind t)
 
+let match_with_sigma_type t=
+  let (hdapp,args) = decompose_app t in
+  match (kind_of_term hdapp) with
+    | Ind ind  -> 
+        let (mib,mip) = Global.lookup_inductive ind in
+          if (mip.mind_nrealargs=0) &&
+	    (Array.length mip.mind_consnames=1) &&
+	    has_nodep_prod_after (mip.mind_nparams+1) mip.mind_nf_lc.(0) then
+	      (*allowing only 1 existential*) 
+	      Some (hdapp,args)
+	  else 
+	    None
+    | _ -> None
+
+let is_sigma_type t=op2bool (match_with_sigma_type t)
+
 (***** Destructing patterns bound to some theory *)
 
 let rec first_match matcher = function
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index cfe3f40279..3dd6a420f4 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -91,6 +91,9 @@ val has_nodep_prod         : testing_function
 val match_with_nodep_ind   : (constr * constr list) matching_function	  
 val is_nodep_ind           : testing_function 
 
+val match_with_sigma_type   : (constr * constr list) matching_function	  
+val is_sigma_type           : testing_function 
+
 (***** Destructing patterns bound to some theory *)
 
 open Coqlib
-- 
cgit v1.2.3