diff options
| author |  corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-07-04 11:45:32 +0000 |
|---|---|---|
| committer | corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-07-04 11:45:32 +0000 |
| commit | 9f522aa25cb212c71008ba960ff5c7620bb08fd8 (patch) | |
| tree | b446aec50f67765776c91b374a1686c83ddde030 /contrib | |
| parent | b4f100cb9fa0d57834f17526325bb996efe60249 (diff) | |
Ground bugfix
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4220 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/first-order/formula.ml | 30 |
1 files changed, 17 insertions, 13 deletions
diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml index 4a76a4dcd..1715658dc 100644 --- a/contrib/first-order/formula.ml +++ b/contrib/first-order/formula.ml @@ -97,21 +97,25 @@ let rec kind_of_formula gl term = match match_with_nodep_ind cciterm with Some (i,l,n)-> let ind=destInd i in - let has_realargs=(n>0) in let (mib,mip) = Global.lookup_inductive ind in - let is_trivial= - let is_constant c = - nb_prod c = mip.mind_nparams in - array_exists is_constant mip.mind_nf_lc in - if Inductiveops.mis_is_recursive (ind,mib,mip) || - (has_realargs && not is_trivial) - then - Atom cciterm + let nconstr=Array.length mip.mind_consnames in + if nconstr=0 then + False(ind,l) else - (match Array.length mip.mind_consnames with - 0->False(ind,l) - | 1->And(ind,l,is_trivial) - | _->Or(ind,l,is_trivial)) + let has_realargs=(n>0) in + let is_trivial= + let is_constant c = + nb_prod c = mip.mind_nparams in + array_exists is_constant mip.mind_nf_lc in + if Inductiveops.mis_is_recursive (ind,mib,mip) || + (has_realargs && not is_trivial) + then + Atom cciterm + else + if nconstr=1 then + And(ind,l,is_trivial) + else + Or(ind,l,is_trivial) | _ -> match match_with_sigma_type cciterm with Some (i,l)-> Exists((destInd i),l) |