diff options
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 |