diff options
| author | corbinea | 2003-05-25 19:44:31 +0000 |
|---|---|---|
| committer | corbinea | 2003-05-25 19:44:31 +0000 |
| commit | cb134451453a608cc486c1235fde2e08b7eab254 (patch) | |
| tree | f3b607367167c00f2834c753899527a034d0ae25 /tactics | |
| parent | ea484db49c183ab900a78204e4bb7ec233578bff (diff) | |
Ground and CCsolve updates
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4075 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/hipattern.ml | 16 | ||||
| -rw-r--r-- | tactics/hipattern.mli | 3 |
2 files changed, 19 insertions, 0 deletions
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 |