diff options
| author |  mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-11-02 22:12:16 +0000 |
|---|---|---|
| committer | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-11-02 22:12:16 +0000 |
| commit | 2f5c0f8880cd4ccc27cef4980768d35c9ebd26ea (patch) | |
| tree | fb1f33855c930c0f5c46a67529e6df6e24652c9f /tactics/hipattern.ml | |
| parent | 30ef31fd8e01d39fb7ce909167dcc1e4a29d7f80 (diff) | |
Types inductifs parametriques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7493 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/hipattern.ml')
| -rw-r--r-- | tactics/hipattern.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index dfdacbb99..c3735b2c8 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -120,7 +120,7 @@ let match_with_unit_type t = let constr_types = mip.mind_nf_lc in let nconstr = Array.length mip.mind_consnames in let zero_args c = - nb_prod c = mip.mind_nparams in + nb_prod c = mib.mind_nparams in if nconstr = 1 && array_for_all zero_args constr_types then Some hdapp else @@ -213,11 +213,11 @@ let match_with_nodep_ind t = | Ind ind -> let (mib,mip) = Global.lookup_inductive ind in if Array.length (mib.mind_packets)>1 then None else - let nodep_constr = has_nodep_prod_after mip.mind_nparams in + let nodep_constr = has_nodep_prod_after mib.mind_nparams in if array_for_all nodep_constr mip.mind_nf_lc then let params= if mip.mind_nrealargs=0 then args else - fst (list_chop mip.mind_nparams args) in + fst (list_chop mib.mind_nparams args) in Some (hdapp,params,mip.mind_nrealargs) else None @@ -233,7 +233,7 @@ let match_with_sigma_type t= if (Array.length (mib.mind_packets)=1) && (mip.mind_nrealargs=0) && (Array.length mip.mind_consnames=1) && - has_nodep_prod_after (mip.mind_nparams+1) mip.mind_nf_lc.(0) then + has_nodep_prod_after (mib.mind_nparams+1) mip.mind_nf_lc.(0) then (*allowing only 1 existential*) Some (hdapp,args) else |