From 0752f867e7561e7161883c8467a028031e60ac2a Mon Sep 17 00:00:00 2001 From: corbinea Date: Fri, 6 Feb 2004 13:58:34 +0000 Subject: correction de bugs de congruence et firstorder (inductifs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5303 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/first-order/formula.ml | 25 +++++++++++-------------- 1 file changed, 11 insertions(+), 14 deletions(-) (limited to 'contrib/first-order/formula.ml') diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml index 502667184..2561e4937 100644 --- a/contrib/first-order/formula.ml +++ b/contrib/first-order/formula.ml @@ -17,6 +17,7 @@ open Tacmach open Util open Declarations open Libnames +open Inductiveops let qflag=ref true @@ -44,20 +45,16 @@ let rec nb_prod_after n c= 1+(nb_prod_after 0 b) | _ -> 0 -let nhyps mip = - let constr_types = mip.mind_nf_lc in - let hyp = nb_prod_after mip.mind_nparams in +let construct_nhyps ind gls = + let env=pf_env gls in + let nparams = (snd (Global.lookup_inductive ind)).mind_nparams in + let constr_types = Inductive.arities_of_constructors (pf_env gls) ind in + let hyp = nb_prod_after nparams in Array.map hyp constr_types -let construct_nhyps ind= nhyps (snd (Global.lookup_inductive ind)) - (* indhyps builds the array of arrays of constructor hyps for (ind largs)*) -let ind_hyps nevar ind largs= - let (mib,mip) = Global.lookup_inductive ind in - let n = mip.mind_nparams in - (* assert (n=(List.length largs));*) - let lp=Array.length mip.mind_consnames in - let types= mip.mind_nf_lc in +let ind_hyps nevar ind largs gls= + let types= Inductive.arities_of_constructors (pf_env gls) ind in let lp=Array.length types in let myhyps i= let t1=Term.prod_applist types.(i) largs in @@ -146,7 +143,7 @@ let build_atoms gl metagen side cciterm = else negative:= unsigned :: !negative end; - let v = ind_hyps 0 i l in + let v = ind_hyps 0 i l gl in let g i _ (_,_,t) = build_rec env polarity (lift i t) in let f l = @@ -157,7 +154,7 @@ let build_atoms gl metagen side cciterm = Array.iter f v | Exists(i,l)-> let var=mkMeta (metagen true) in - let v =(ind_hyps 1 i l).(0) in + let v =(ind_hyps 1 i l gl).(0) in let g i _ (_,_,t) = build_rec (var::env) polarity (lift i t) in list_fold_left_i g (2-(List.length l)) () v @@ -232,7 +229,7 @@ let build_formula side nam typ gl metagen= | And(_,_,_) -> Rand | Or(_,_,_) -> Ror | Exists (i,l) -> - let (_,_,d)=list_last (ind_hyps 0 i l).(0) in + let (_,_,d)=list_last (ind_hyps 0 i l gl).(0) in Rexists(m,d,trivial) | Forall (_,a) -> Rforall | Arrow (a,b) -> Rarrow in -- cgit v1.2.3