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

4 files changed, 30 insertions, 34 deletions

diff --git a/contrib/cc/cctac.ml4 b/contrib/cc/cctac.ml4
index 9de5e3a2d..69e2be12c 100644
--- a/contrib/cc/cctac.ml4
+++ b/contrib/cc/cctac.ml4
@@ -80,7 +80,8 @@ let read_eq env term=
 let rec make_term=function
     Symb s->s
   | Constructor(c,_,_)->mkConstruct c 
-  | Appli (s1,s2)->make_app [(make_term s2)] s1
+  | Appli (s1,s2)->
+      make_app [(make_term s2)] s1
 and make_app l=function
     Symb s->applistc s l
   | Constructor(c,_,_)->applistc (mkConstruct c) l
@@ -105,15 +106,13 @@ let make_prb gl=
 (* indhyps builds the array of arrays of constructor hyps for (ind largs) *)
 
 let build_projection intype outtype (cstr:constructor) special default gls=
+  let env=pf_env gls in 
   let (h,argv) = 
     try destApplication intype with 
 	Invalid_argument _ -> (intype,[||])  in
   let ind=destInd h in 
-  let (mib,mip) = Global.lookup_inductive ind in
-  let n = mip.mind_nparams in
-    (* assert (n=(Array.length argv));*)
-  let lp=Array.length mip.mind_consnames in
-  let types=mip.mind_nf_lc in   
+  let types=Inductive.arities_of_constructors env ind in
+  let lp=Array.length types in
   let ci=(snd cstr)-1 in
   let branch i=
     let ti=Term.prod_appvect types.(i) argv in
@@ -124,12 +123,11 @@ let build_projection intype outtype (cstr:constructor) special default gls=
   let branches=Array.init lp branch in
   let casee=mkRel 1 in
   let pred=mkLambda(Anonymous,intype,outtype) in
-  let env=pf_env gls in 
   let case_info=make_default_case_info (pf_env gls) RegularStyle ind in
   let body= mkCase(case_info, pred, casee, branches) in
   let id=pf_get_new_id (id_of_string "t") gls in     
     mkLambda(Name id,intype,body)
-
+  
 (* generate an adhoc tactic following the proof tree  *)
 
 let rec proof_tac axioms=function
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
diff --git a/contrib/first-order/formula.mli b/contrib/first-order/formula.mli
index 9e027e240..5fa1323c8 100644
--- a/contrib/first-order/formula.mli
+++ b/contrib/first-order/formula.mli
@@ -26,9 +26,10 @@ type ('a,'b) sum = Left of 'a | Right of 'b
 
 type counter = bool -> metavariable
 
-val construct_nhyps : inductive -> int array
+val construct_nhyps : inductive -> Proof_type.goal Tacmach.sigma -> int array
 
-val ind_hyps : int -> inductive -> constr list -> Sign.rel_context array
+val ind_hyps : int -> inductive -> constr list -> 
+  Proof_type.goal Tacmach.sigma -> Sign.rel_context array
 
 type atoms = {positive:constr list;negative:constr list}
 
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index e0756ca5b..2c44581e8 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -88,18 +88,18 @@ let arrow_tac backtrack continue seq=
        backtrack)
 (* left connectives rules *)
 
-let left_and_tac ind backtrack id continue seq=
- let n=(construct_nhyps ind).(0) in  
+let left_and_tac ind backtrack id continue seq gls=
+ let n=(construct_nhyps ind gls).(0) in  
    tclIFTHENELSE
      (tclTHENLIST 
       [simplest_elim (constr_of_reference id);
        clear_global id; 
        tclDO n intro])
      (wrap n false continue seq)
-     backtrack
+     backtrack gls
 
-let left_or_tac ind backtrack id continue seq=
-  let v=construct_nhyps ind in  
+let left_or_tac ind backtrack id continue seq gls=
+  let v=construct_nhyps ind gls in  
   let f n=
     tclTHENLIST
       [clear_global id;
@@ -108,7 +108,7 @@ let left_or_tac ind backtrack id continue seq=
     tclIFTHENSVELSE
       (simplest_elim (constr_of_reference id))
       (Array.map f v)
-      backtrack
+      backtrack gls
 
 let left_false_tac id=
   simplest_elim (constr_of_reference id)
@@ -118,7 +118,7 @@ let left_false_tac id=
 (* We use this function for false, and, or, exists *)
 
 let ll_ind_tac ind largs backtrack id continue seq gl= 
-     let rcs=ind_hyps 0 ind largs in
+     let rcs=ind_hyps 0 ind largs gl in
      let vargs=Array.of_list largs in
 	     (* construire le terme  H->B, le generaliser etc *)   
      let myterm i=
@@ -172,13 +172,13 @@ let forall_tac backtrack continue seq=
      else
        backtrack)
 
-let left_exists_tac ind id continue seq=
-  let n=(construct_nhyps ind).(0) in  
+let left_exists_tac ind id continue seq gls=
+  let n=(construct_nhyps ind gls).(0) in  
     tclTHENLIST
       [simplest_elim (constr_of_reference id);
        clear_global id;
        tclDO n intro;
-       (wrap (n-1) false continue seq)]
+       (wrap (n-1) false continue seq)] gls
 	
 let ll_forall_tac prod backtrack id continue seq=
   tclORELSE