Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeurs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@480 85f007b7-540e-0410-9357-904b9bb8a0f7

12 files changed, 97 insertions, 107 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 7f45aae57..d97bb916b 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -44,10 +44,10 @@ type recarg =
   | Mrec of int 
   | Imbr of inductive_path * recarg list
 
-type mutual_inductive_packet = {
+type one_inductive_body = {
   mind_consnames : identifier array;
   mind_typename : identifier;
-  mind_lc : constr;
+  mind_lc : constr array;
   mind_arity : typed_type;
   mind_sort : sorts;
   mind_nrealargs : int;
@@ -59,7 +59,7 @@ type mutual_inductive_body = {
   mind_kind : path_kind;
   mind_ntypes : int;
   mind_hyps : typed_type signature;
-  mind_packets : mutual_inductive_packet array;
+  mind_packets : one_inductive_body array;
   mind_constraints : constraints;
   mind_singl : constr option;
   mind_nparams : int }
@@ -71,6 +71,6 @@ let mind_type_finite mib i = mib.mind_packets.(i).mind_finite
 type mutual_inductive_entry = {
   mind_entry_nparams : int;
   mind_entry_finite : bool;
-  mind_entry_inds : (identifier * constr * identifier list * constr) list }
+  mind_entry_inds : (identifier * constr * identifier list * constr list) list}
 
 let mind_nth_type_packet mib n = mib.mind_packets.(n)
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 47f0993e9..d05c07f14 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -44,10 +44,16 @@ type recarg =
   | Mrec of int 
   | Imbr of inductive_path * (recarg list)
 
-type mutual_inductive_packet = {
+(* [mind_typename] is the name of the inductive; [mind_arity] is
+   the arity generalized over global parameters; [mind_lc] is the list
+   of types of constructors generalized over global parameters and
+   relative to the global context enriched with the arities of the
+   inductives *) 
+
+type one_inductive_body = {
   mind_consnames : identifier array;
   mind_typename : identifier;
-  mind_lc : constr;
+  mind_lc : constr array;
   mind_arity : typed_type;
   mind_sort : sorts;
   mind_nrealargs : int;
@@ -59,7 +65,7 @@ type mutual_inductive_body = {
   mind_kind : path_kind;
   mind_ntypes : int;
   mind_hyps : typed_type signature;
-  mind_packets : mutual_inductive_packet array;
+  mind_packets : one_inductive_body array;
   mind_constraints : constraints;
   mind_singl : constr option;
   mind_nparams : int }
@@ -67,12 +73,12 @@ type mutual_inductive_body = {
 val mind_type_finite : mutual_inductive_body -> int -> bool
 
 val mind_nth_type_packet : 
-  mutual_inductive_body -> int -> mutual_inductive_packet
+  mutual_inductive_body -> int -> one_inductive_body
 
 (*s Declaration of inductive types. *)
 
 type mutual_inductive_entry = {
   mind_entry_nparams : int;
   mind_entry_finite : bool;
-  mind_entry_inds : (identifier * constr * identifier list * constr) list }
+  mind_entry_inds : (identifier * constr * identifier list * constr list) list}
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index ea8b77570..5cedd542c 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -100,14 +100,17 @@ let mind_extract_and_check_params mie =
 	List.iter (fun (_,c,_,_) -> check_params nparams params c) l;
 	params
 
+let decomp_all_DLAMV_name constr = 
+  let rec decomprec lna = function 
+    | DLAM(na,lc)  -> decomprec (na::lna) lc
+    | DLAMV(na,lc) -> (na::lna,lc)
+    | _ -> assert false
+  in 
+  decomprec [] constr
+
 let mind_check_lc params mie =
-  let ntypes = List.length mie.mind_entry_inds in
   let nparams = List.length params in
-  let check_lc (_,_,_,lc) =
-    let (lna,c) = decomp_all_DLAMV_name lc in
-    Array.iter (check_params nparams params) c;
-    if not (List.length lna = ntypes) then raise (InductiveError BadEntry)
-  in
+  let check_lc (_,_,_,lc) = List.iter (check_params nparams params) lc in
   List.iter check_lc mie.mind_entry_inds
 
 let mind_check_arities env mie =
@@ -169,20 +172,19 @@ let check_correct_par env nparams ntypes n l largs =
     if not ((Rel (n-k-1))= whd_betadeltaiotaeta env Evd.empty lpar.(k)) then
       raise (IllFormedInd (LocalNonPar (k+1,l)))
   done;
-  if not (array_for_all (noccur_bet n ntypes) largs') then 
+  if not (array_for_all (noccur_between n ntypes) largs') then 
     failwith_non_pos_vect n ntypes largs'
 
 (* This removes global parameters of the inductive types in lc *)
 let abstract_mind_lc env ntyps npars lc = 
-  let lC = decomp_DLAMV ntyps lc in
   if npars = 0 then 
-    lC 
+    lc
   else 
     let make_abs = 
       list_tabulate
 	(function i -> lambda_implicit_lift npars (Rel (i+1))) ntyps 
     in 
-    Array.map (compose (nf_beta env Evd.empty) (substl make_abs)) lC
+    Array.map (compose (nf_beta env Evd.empty) (substl make_abs)) lc
 
 let decomp_par n c = snd (mind_extract_params n c)
       
@@ -191,7 +193,7 @@ let listrec_mconstr env ntypes nparams i indlc =
   let rec check_pos n c = 
     match whd_betadeltaiota env Evd.empty c with 
       | DOP2(Prod,b,DLAM(na,d)) -> 
-          if not (noccur_bet n ntypes b) then raise (IllFormedInd (LocalNonPos n));
+          if not (noccur_between n ntypes b) then raise (IllFormedInd (LocalNonPos n));
 	  check_pos (n+1) d
       | x -> 
 	  let hd,largs = destApplication (ensure_appl x) in
@@ -200,24 +202,24 @@ let listrec_mconstr env ntypes nparams i indlc =
                 if k >= n && k<n+ntypes then begin
 		  check_correct_par env nparams ntypes n (k-n+1) largs;
 		  Mrec(n+ntypes-k-1)
-                end else if noccur_bet n ntypes x then 
+                end else if noccur_between n ntypes x then 
 		  if (n-nparams) <= k & k <= (n-1) 
 		  then Param(n-1-k)
                   else Norec
 		else
 		  raise (IllFormedInd (LocalNonPos n))
             | DOPN(MutInd ind_sp,a) -> 
-                if (noccur_bet n ntypes x) then Norec
+                if (noccur_between n ntypes x) then Norec
                 else Imbr(ind_sp,imbr_positive n (ind_sp,a) largs)
             | err -> 
-		if noccur_bet n ntypes x then Norec
+		if noccur_between n ntypes x then Norec
 		else raise (IllFormedInd (LocalNonPos n))
 
   and imbr_positive n mi largs =
     let mispeci = lookup_mind_specif mi env in
     let auxnpar = mis_nparams mispeci in
     let (lpar,auxlargs) = array_chop auxnpar largs in 
-    if not (array_for_all (noccur_bet n ntypes) auxlargs) then
+    if not (array_for_all (noccur_between n ntypes) auxlargs) then
       raise (IllFormedInd (LocalNonPos n));
     let auxlc = mis_lc mispeci 
     and auxntyp = mis_ntypes mispeci in 
@@ -259,7 +261,7 @@ let listrec_mconstr env ntypes nparams i indlc =
     match whd_betadeltaiota env Evd.empty c with 
       (* The extra case *)
       | DOP2(Lambda,b,DLAM(na,d)) -> 
-          if noccur_bet n ntypes b
+          if noccur_between n ntypes b
           then check_weak_pos (n+1) d
           else raise (IllFormedInd (LocalNonPos n))
       (******************)
@@ -283,19 +285,19 @@ let listrec_mconstr env ntypes nparams i indlc =
 		    check_correct_par env nparams ntypes n (k-n+1) largs
                 | _ -> raise (IllFormedInd LocalNotConstructor)
 	    else
-	      if not (array_for_all (noccur_bet n ntypes) largs)
+	      if not (array_for_all (noccur_between n ntypes) largs)
               then raise (IllFormedInd (LocalNonPos n));
 	    List.rev lrec
     in check_constr_rec []
   in
-  let (lna,lC) = decomp_DLAMV_name ntypes indlc in
+  let lna = it_dbenv (fun l na t -> na::l) [] (context env) in
   Array.map
     (fun c ->
        try
 	 check_construct true (1+nparams) (decomp_par nparams c)
        with IllFormedInd err -> 
 	 explain_ind_err (ntypes-i+1) lna nparams c err)
-    lC
+    indlc
     
 let is_recursive listind =
   let rec one_is_rec rvec = 
@@ -326,8 +328,11 @@ let cci_inductive env env_ar kind nparams finite inds cst =
   let ids = 
     List.fold_left 
       (fun acc (_,ar,_,_,_,lc) -> 
-	 Idset.union (global_vars_set (body_of_type ar)) 
-	   (Idset.union (global_vars_set lc) acc))
+	 Idset.union (global_vars_set (body_of_type ar))
+	   (Array.fold_left
+	      (fun acc c -> Idset.union (global_vars_set c) acc)
+	      acc
+	      lc))
       Idset.empty inds
   in
   let packets = Array.of_list (list_map_i one_packet 1 inds) in
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index e73d5779a..c35459454 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -60,6 +60,7 @@ val mind_check_arities : env -> mutual_inductive_entry -> unit
 
 val cci_inductive : 
   env -> env -> path_kind -> int -> bool -> 
-    (identifier * typed_type * identifier list * bool * bool * constr) list ->
+    (identifier * typed_type * identifier list * bool * bool * constr array)
+      list ->
       constraints ->
       	mutual_inductive_body
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index c096008db..85ea816e6 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -16,7 +16,7 @@ type inductive_instance = {
   mis_mib : mutual_inductive_body;
   mis_tyi : int;
   mis_args : constr array;
-  mis_mip : mutual_inductive_packet }
+  mis_mip : one_inductive_body }
 
 let mis_ntypes mis = mis.mis_mib.mind_ntypes
 let mis_nparams mis = mis.mis_mib.mind_nparams
@@ -36,17 +36,10 @@ let mis_consnames mis = mis.mis_mip.mind_consnames
 let mis_inductive mis = ((mis.mis_sp,mis.mis_tyi),mis.mis_args)
 
 let mis_lc mis =
-  Instantiate.instantiate_constr
-    (ids_of_sign mis.mis_mib.mind_hyps) mis.mis_mip.mind_lc
-    (Array.to_list mis.mis_args)
-
-let mis_lc_without_abstractions mis = 
-  let rec strip_DLAM = function
-    | (DLAM (n,c1)) -> strip_DLAM c1 
-    | (DLAMV (n,v)) -> v
-    | _ -> assert false
-  in 
-  strip_DLAM (mis_lc mis)
+  let ids = ids_of_sign mis.mis_mib.mind_hyps in
+  let args = Array.to_list mis.mis_args in
+  Array.map (fun t -> Instantiate.instantiate_constr ids t args)
+    mis.mis_mip.mind_lc
 
 (* gives the vector of constructors and of 
    types of constructors of an inductive definition 
@@ -56,20 +49,20 @@ let mis_type_mconstructs mispec =
   let specif = mis_lc mispec
   and ntypes = mis_ntypes mispec
   and nconstr = mis_nconstr mispec in
-  let make_Ik k = mkMutInd ((mispec.mis_sp,k),mispec.mis_args) 
+  let make_Ik k = mkMutInd ((mispec.mis_sp,ntypes-k-1),mispec.mis_args) 
   and make_Ck k = mkMutConstruct
 		    (((mispec.mis_sp,mispec.mis_tyi),k+1),
 		       mispec.mis_args) in
   (Array.init nconstr make_Ck, 
-   sAPPVList specif (list_tabulate make_Ik ntypes))
+   Array.map (substl (list_tabulate make_Ik ntypes)) specif)
 
 let mis_type_mconstruct i mispec =
   let specif = mis_lc mispec
   and ntypes = mis_ntypes mispec
   and nconstr = mis_nconstr mispec in
-  let make_Ik k = DOPN(MutInd(mispec.mis_sp,k),mispec.mis_args) in 
+  let make_Ik k = DOPN(MutInd(mispec.mis_sp,ntypes-k-1),mispec.mis_args) in 
   if i > nconstr then error "Not enough constructors in the type";
-  sAPPViList (i-1) specif (list_tabulate make_Ik ntypes)
+  substl (list_tabulate make_Ik ntypes) specif.(i-1)
 
 let mis_typed_arity mis =
   let idhyps = ids_of_sign mis.mis_mib.mind_hyps 
@@ -96,11 +89,11 @@ let liftn_inductive_instance n depth mis = {
 
 let lift_inductive_instance n = liftn_inductive_instance n 1
 
-let substn_many_ind_instance cv depth mis = {
+let substnl_ind_instance l n mis = {
   mis_sp = mis.mis_sp;
   mis_mib = mis.mis_mib;
   mis_tyi = mis.mis_tyi;
-  mis_args = Array.map (substn_many cv depth) mis.mis_args;
+  mis_args = Array.map (substnl l n) mis.mis_args;
   mis_mip = mis.mis_mip
 }
 
@@ -117,13 +110,11 @@ let liftn_inductive_type n d (IndType (indf, realargs)) =
   IndType (liftn_inductive_family n d indf, List.map (liftn n d) realargs)
 let lift_inductive_type n = liftn_inductive_type n 1
 
-let substn_many_ind_family cv depth (IndFamily (mis,params)) =
-  IndFamily (substn_many_ind_instance cv depth mis,
-	     List.map (substn_many cv depth) params)
+let substnl_ind_family l n (IndFamily (mis,params)) =
+  IndFamily (substnl_ind_instance l n mis, List.map (substnl l n) params)
 
-let substn_many_ind_type cv depth (IndType (indf,realargs)) =
-  IndType (substn_many_ind_family cv depth indf,
-	   List.map (substn_many cv depth) realargs)
+let substnl_ind_type l n (IndType (indf,realargs)) =
+  IndType (substnl_ind_family l n indf, List.map (substnl l n) realargs)
 
 let make_ind_family (mis, params) = IndFamily (mis,params)
 let dest_ind_family (IndFamily (mis,params)) = (mis,params)
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index b603fbf1e..fa989110c 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -43,8 +43,7 @@ val mis_consnames : inductive_instance -> identifier array
 val mis_typed_arity : inductive_instance -> typed_type
 val mis_inductive : inductive_instance -> inductive
 val mis_arity : inductive_instance -> constr
-val mis_lc : inductive_instance -> constr
-val mis_lc_without_abstractions : inductive_instance -> constr array
+val mis_lc : inductive_instance -> constr array
 val mis_type_mconstructs : inductive_instance -> constr array * constr array
 val mis_type_mconstruct : int -> inductive_instance -> constr
 val mis_params_ctxt : inductive_instance -> (name * constr) list
@@ -58,8 +57,8 @@ val dest_ind_family : inductive_family -> inductive_instance * constr list
 
 val liftn_inductive_family : int -> int -> inductive_family -> inductive_family
 val lift_inductive_family : int -> inductive_family -> inductive_family
-val substn_many_ind_family : constr Generic.substituend array -> int
-  -> inductive_family -> inductive_family
+val substnl_ind_family : constr list -> int -> inductive_family 
+  -> inductive_family
 
 (*s [inductive_type] = [inductive_family] applied to ``real'' parameters *)
 type inductive_type = IndType of inductive_family * constr list
@@ -71,8 +70,7 @@ val mkAppliedInd : inductive_type -> constr
 
 val liftn_inductive_type : int -> int -> inductive_type -> inductive_type
 val lift_inductive_type : int -> inductive_type -> inductive_type
-val substn_many_ind_type : constr Generic.substituend array -> int
- -> inductive_type -> inductive_type
+val substnl_ind_type : constr list -> int -> inductive_type -> inductive_type
 
 (*s A [constructor] is an [inductive] + an index; the following functions
     destructs and builds [constructor] *)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 1cf6c6eca..19bf52c84 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -78,19 +78,21 @@ let rec execute mf env cstr =
 	let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
         (type_of_case env Evd.empty ci pj cj lfj, cst)
   
-    | IsFix (vn,i,lar,lfi,vdef) ->
+    | IsFix ((vn,i as vni),(lar,lfi,vdef)) ->
         if (not mf.fix) && array_exists (fun n -> n < 0) vn then
           error "General Fixpoints not allowed";
-        let (larv,vdefv,cst) = execute_fix mf env lar lfi vdef in
-        let fix = mkFix vn i larv lfi vdefv in
+        let (larjv,vdefv,cst) = execute_fix mf env lar lfi vdef in
+	let larv = Array.map body_of_type larjv in
+        let fix = (vni,(larv,lfi,vdefv)) in
         check_fix env Evd.empty fix;
-	(make_judge fix larv.(i), cst)
+	(make_judge (mkFix fix) larjv.(i), cst)
 	  
-    | IsCoFix (i,lar,lfi,vdef) ->
-        let (larv,vdefv,cst) = execute_fix mf env lar lfi vdef in
-        let cofix = mkCoFix i larv lfi vdefv in
+    | IsCoFix (i,(lar,lfi,vdef)) ->
+        let (larjv,vdefv,cst) = execute_fix mf env lar lfi vdef in
+	let larv = Array.map body_of_type larjv in
+        let cofix = (i,(larv,lfi,vdefv)) in
         check_cofix env Evd.empty cofix;
-	(make_judge cofix larv.(i), cst)
+	(make_judge (mkCoFix cofix) larjv.(i), cst)
 	  
     | IsSort (Prop c) -> 
 	(judge_of_prop_contents c, cst0)
@@ -400,22 +402,20 @@ let type_one_constructor env_ar nparams arsort c =
   let cst3 =enforce_type_constructor arsort max (Constraint.union cst1 cst2) in
   (infos, j, cst3)
 
-let type_one_inductive i env_ar env_par nparams ninds (id,ar,cnames,spec) =
-  let (lna,vc) = decomp_all_DLAMV_name spec in
+let type_one_inductive i env_ar env_par nparams ninds (id,ar,cnames,vc) =
   let arsort = sort_of_arity env_ar ar in
   let (constrsinfos,jlc,cst') = 
     List.fold_right
       (fun c (infosl,jl,cst) -> 
 	 let (infos,jc,cst') = type_one_constructor env_ar nparams arsort c in
 	 (infos::infosl,jc::jl, Constraint.union cst cst'))
-      (Array.to_list vc) 
+      vc
       ([],[],Constraint.empty)
   in
-  let castlc = List.map incast_type jlc in
-  let spec' = put_DLAMSV lna (Array.of_list castlc) in
+  let vc' = Array.of_list (List.map incast_type jlc) in
   let issmall,isunit = small_unit constrsinfos (env_par,nparams,ar) in
   let (_,tyar) = lookup_rel (ninds+1-i) env_ar in
-  ((id,tyar,cnames,issmall,isunit,spec'), cst')
+  ((id,tyar,cnames,issmall,isunit,vc'), cst')
 
 let add_mind sp mie env =
   mind_check_names mie;
diff --git a/library/global.ml b/library/global.ml
index 093aaab27..cf3d88ca9 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -61,8 +61,6 @@ let mind_is_recursive =
 let mind_nconstr = Util.compose Inductive.mis_nconstr lookup_mind_specif
 let mind_nparams = Util.compose Inductive.mis_nparams lookup_mind_specif
 let mind_arity = Util.compose Inductive.mis_arity lookup_mind_specif
-
-let mind_lc_without_abstractions = 
-  Util.compose Inductive.mis_lc_without_abstractions lookup_mind_specif
+let mind_lc = Util.compose Inductive.mis_lc lookup_mind_specif
 
 
diff --git a/library/global.mli b/library/global.mli
index 99bb478fd..19d516625 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -52,6 +52,5 @@ val mind_is_recursive : inductive -> bool
 val mind_nconstr : inductive -> int
 val mind_nparams : inductive -> int
 val mind_arity : inductive -> constr
-
-val mind_lc_without_abstractions : inductive -> constr array
+val mind_lc : inductive -> constr array
 
diff --git a/library/impargs.ml b/library/impargs.ml
index fbdb17847..b334092b9 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -68,8 +68,7 @@ let declare_inductive_implicits sp =
   let mib = Global.lookup_mind sp in
   let imps_one_inductive mip =
     (auto_implicits (body_of_type mip.mind_arity),
-     let (_,lc) = decomp_all_DLAMV_name mip.mind_lc in
-     Array.map auto_implicits lc)
+     Array.map auto_implicits mip.mind_lc)
   in
   let imps = Array.map imps_one_inductive mib.mind_packets in
   inductives_table := Spmap.add sp imps !inductives_table
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 00b598646..55664cf1e 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -105,17 +105,6 @@ let assumptions_for_print lna =
   List.fold_right (fun na env -> add_rel (na,()) env) lna
     (ENVIRON(nil_sign,nil_dbsign))
 
-let print_constructors_with_sep pk fsep mip = 
-  let pterm,pterminenv = pkprinters pk in
-  let (lna,lC) = decomp_all_DLAMV_name mip.mind_lc in
-  let ass_name = assumptions_for_print lna in
-  let lidC = Array.to_list 
-               (array_map2 (fun id c -> (id,c)) mip.mind_consnames lC) in
-  let prass (id,c) =
-    let pc = pterminenv ass_name c in [< print_id id; 'sTR " : "; pc >]
-  in
-  prlist_with_sep fsep prass lidC
-
 let implicit_args_id id l = 
   if l = [] then 
     [<>]
@@ -143,13 +132,14 @@ let print_mutual sp mib =
   let {mind_packets=mipv; mind_nparams=nparams} = mib in 
   let (lpars,_) = decomp_n_prod env evd nparams (body_of_type mipv.(0).mind_arity) in
   let lparsname = List.map fst lpars in
+  let lna = Array.map (fun mip -> Name mip.mind_typename) mipv in
   let lparsprint = assumptions_for_print lparsname in
   let prass ass_name (id,c) =
     let pc = pterminenv ass_name c in [< print_id id; 'sTR " : "; pc >] 
   in
-  let print_constructors mip = 
-    let (lna,lC) = decomp_all_DLAMV_name mip.mind_lc in
-    let ass_name = assumptions_for_print (lparsname@lna) in
+  let print_constructors mip =
+    let lC = mip.mind_lc in
+    let ass_name = assumptions_for_print (lparsname@(Array.to_list lna)) in
     let lidC =
       Array.to_list 
         (array_map2 (fun id c -> (id,snd (decomp_n_prod env evd nparams c)))
@@ -343,8 +333,8 @@ let list_filter_vec f vec =
    and the constr term that represent its type. *)
 
 let print_constructors_head 
-  (fn : string -> unit assumptions -> constr -> unit) c mip = 
-  let (lna,lC) = decomp_all_DLAMV_name mip.mind_lc in
+  (fn : string -> unit assumptions -> constr -> unit) c lna mip = 
+  let lC = mip.mind_lc in
   let ass_name = assumptions_for_print lna in
   let lidC = array_map2 (fun id c_0 -> (id,c_0)) mip.mind_consnames lC in
   let flid = list_filter_vec (fun (_,c_0) -> head_const c_0 = c) lidC in
@@ -353,13 +343,14 @@ let print_constructors_head
     
 let print_all_constructors_head fn c mib = 
   let mipvec = mib.mind_packets 
-  and n = mib.mind_ntypes in 
+  and n = mib.mind_ntypes in
+  let lna = array_map_to_list (fun mip -> Name mip.mind_typename) mipvec in
   for i = 0 to n-1 do
-    print_constructors_head fn c mipvec.(i)
+    print_constructors_head fn c lna mipvec.(i)
   done
 
-let print_constructors_rel fn mip = 
-  let (lna,lC) = decomp_all_DLAMV_name mip.mind_lc in
+let print_constructors_rel fn lna mip = 
+  let lC = mip.mind_lc in
   let ass_name = assumptions_for_print lna in
   let lidC = array_map2 (fun id c -> (id,c)) mip.mind_consnames lC in
   let flid = list_filter_vec (fun (_,c) -> isRel (head_const c)) lidC in
@@ -384,9 +375,12 @@ let crible (fn : string -> unit assumptions -> constr -> unit) name =
                crible_rec rest
 	   | (sp,"INDUCTIVE") -> 
                let mib = Global.lookup_mind sp in 
+	       let lna =
+		 array_map_to_list
+		   (fun mip -> Name mip.mind_typename) mib.mind_packets in
                (match const with 
 		  | (DOPN(MutInd(sp',tyi),_)) -> 
-		      if sp = objsp_of sp' then print_constructors_rel fn
+		      if sp = objsp_of sp' then print_constructors_rel fn lna
 			(mind_nth_type_packet mib tyi) 
 		  | _ -> print_all_constructors_head fn const mib); 
                crible_rec rest
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index d31a71845..61d8c4fe7 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -153,7 +153,7 @@ let match_with_disjunction t =
   match kind_of_term hdapp with
     | IsMutInd ind  ->
 	let mispec = Global.lookup_mind_specif ind in
-        let constr_types = mis_lc_without_abstractions mispec in
+        let constr_types = mis_lc mispec in
         let only_one_arg c =
 	  ((nb_prod c) - (mis_nparams mispec)) = 1 in 
 	if (array_for_all only_one_arg constr_types) &&
@@ -180,8 +180,7 @@ let match_with_unit_type t =
   let (hdapp,args) = decomp_app t in
   match (kind_of_term hdapp) with
     | IsMutInd ind  -> 
-        let constr_types = 
-	  Global.mind_lc_without_abstractions ind in 
+        let constr_types = Global.mind_lc ind in 
         let nconstr = Global.mind_nconstr ind in
         let zero_args c = ((nb_prod c) - (Global.mind_nparams ind)) = 0 in  
 	if nconstr = 1 && (array_for_all zero_args constr_types) then 
@@ -204,7 +203,7 @@ let match_with_equation  t =
   let (hdapp,args) = decomp_app t in
   match (kind_of_term hdapp) with
     | IsMutInd ind -> 
-        let constr_types = Global.mind_lc_without_abstractions ind in 
+        let constr_types = Global.mind_lc ind in 
         let nconstr = Global.mind_nconstr ind in
 	if nconstr = 1 &&
            (is_matching (get_pat refl_rel_pat1) constr_types.(0) ||