diff options
| author |  corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-07 12:59:01 +0000 |
|---|---|---|
| committer | corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-07 12:59:01 +0000 |
| commit | 0980569e174509e6718c96675c1aea1f82ce79ae (patch) | |
| tree | 93e9355a3989972144280328c2e2aa168a196dc7 /tactics/hipattern.ml | |
| parent | f3b55488ec289e06c6926396a4049f53a422ae0c (diff) | |
Enhancement of the Ground tactic, addition of GTauto and GIntuition.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3991 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/hipattern.ml')
| -rw-r--r-- | tactics/hipattern.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index ff735c9cd..98976a91c 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -204,12 +204,13 @@ let match_with_nodep_ind t = match (kind_of_term hdapp) with | Ind ind -> let (mib,mip) = Global.lookup_inductive ind in - let constr_types = mip.mind_nf_lc in - let nodep_constr = has_nodep_prod_after mip.mind_nparams in - if array_for_all nodep_constr constr_types then - Some (hdapp,args) - else - None + if mip.mind_nrealargs>0 then None else + let constr_types = mip.mind_nf_lc in + let nodep_constr = has_nodep_prod_after mip.mind_nparams in + if array_for_all nodep_constr constr_types then + Some (hdapp,args) + else + None | _ -> None let is_nodep_ind t=op2bool (match_with_nodep_ind t) |