Imported Upstream version 8.1+dfsgupstream/8.1+dfsg

12 files changed, 243 insertions, 86 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 7a170bcf..ff435bfc 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: detyping.ml 8875 2006-05-29 19:59:11Z msozeau $ *)
+(* $Id: detyping.ml 9535 2007-01-26 09:26:08Z jforest $ *)
 
 open Pp
 open Util
@@ -286,9 +286,9 @@ let it_destRLambda_or_LetIn_names n c =
           (* eta-expansion *)
 	  let rec next l =
 	    let x = Nameops.next_ident_away (id_of_string "x") l in
-	    (* Not efficient but unusual and no function to get free rawvars *)
-	    if occur_rawconstr x c then next (x::l) else x in
-	  let x = next [] in 
+	    x
+	  in
+	  let x = next (free_rawvars c) in 
 	  let a = RVar (dl,x) in
 	  aux (n-1) (Name x :: nal) 
             (match c with
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 307c9886..b545bd38 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evarutil.ml 9154 2006-09-20 17:18:18Z corbinea $ *)
+(* $Id: evarutil.ml 9573 2007-01-31 20:18:18Z notin $ *)
 
 open Util
 open Pp
@@ -57,8 +57,8 @@ let tj_nf_evar = Pretype_errors.tj_nf_evar
 
 let nf_evar_info evc info =
   { info with 
-      evar_concl = Reductionops.nf_evar evc info.evar_concl;
-      evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps}
+    evar_concl = Reductionops.nf_evar evc info.evar_concl;
+    evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps}
 
 let nf_evars evm = Evd.fold (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi))
 		     evm Evd.empty
@@ -99,7 +99,7 @@ let push_dependent_evars sigma emap =
 	(Evd.add sigma' ev (Evd.find emap' ev),Evd.remove emap' ev))
       (sigma',emap') (collect_evars emap' ccl))
     emap (sigma,emap)
-    
+
 (* replaces a mapping of existentials into a mapping of metas.
    Problem if an evar appears in the type of another one (pops anomaly) *)
 let evars_to_metas sigma (emap, c) =
@@ -165,12 +165,12 @@ let new_untyped_evar =
 (* All ids of sign must be distincts! *)
 let new_evar_instance sign evd typ ?(src=(dummy_loc,InternalHole)) instance =
   let ctxt = named_context_of_val sign in
-  assert (List.length instance = named_context_length ctxt); 
-  if not (list_distinct (ids_of_named_context ctxt)) then 
-    anomaly "new_evar_instance: two vars have the same name";
-  let newev = new_untyped_evar() in
-  (evar_declare sign newev typ ~src:src evd,
-   mkEvar (newev,Array.of_list instance))
+    assert (List.length instance = named_context_length ctxt); 
+    if not (list_distinct (ids_of_named_context ctxt)) then 
+      anomaly "new_evar_instance: two vars have the same name";
+    let newev = new_untyped_evar() in
+      (evar_declare sign newev typ ~src:src evd,
+      mkEvar (newev,Array.of_list instance))
 
 let make_evar_instance_with_rel env =
   let n = rel_context_length (rel_context env) in
@@ -199,7 +199,6 @@ let push_rel_context_to_named_context env =
   let (subst,_,env) =
   Sign.fold_rel_context
     (fun (na,c,t) (subst,avoid,env) ->
-       let na = if na = Anonymous then Name(id_of_string"_") else na in
        let id = next_name_away na avoid in
        ((mkVar id)::subst,
         id::avoid,
@@ -215,11 +214,11 @@ let new_evar evd env ?(src=(dummy_loc,InternalHole)) typ =
   let instance = make_evar_instance_with_rel env in
   new_evar_instance sign evd typ' ~src:src instance
 
-(* The same using side-effect *)
+  (* The same using side-effect *)
 let e_new_evar evd env ?(src=(dummy_loc,InternalHole)) ty =
   let (evd',ev) = new_evar !evd env ~src:src ty in
-  evd := evd';
-  ev
+    evd := evd';
+    ev
 
 (*------------------------------------*
  * operations on the evar constraints *
@@ -315,33 +314,110 @@ let do_restrict_hyps env k evd ev args =
   let evi = Evd.find (evars_of !evd) ev in
   let hyps = evar_context evi in
   let (hyps',ncargs) = list_filter2 (fun _ a -> closedn k a) (hyps,args) in
-  (* No care is taken in case the evar type uses vars filtered out!
-     Assuming that the restriction comes from a well-typed Flex/Flex
-     unification problem (see real_clean), the type of the evar cannot
-     depend on variables that are not in the scope of the other evar,
-     since this other evar has the same type (up to unification).
+    (* No care is taken in case the evar type uses vars filtered out!
+       Assuming that the restriction comes from a well-typed Flex/Flex
+       unification problem (see real_clean), the type of the evar cannot
+       depend on variables that are not in the scope of the other evar,
+       since this other evar has the same type (up to unification).
      Since moreover, the evar contexts uses names only, the
-     restriction raise no de Bruijn reallocation problem *)
+       restriction raise no de Bruijn reallocation problem *)
   let env' =
     Sign.fold_named_context push_named hyps' ~init:(reset_context env) in
   let nc = e_new_evar evd env' ~src:(evar_source ev !evd) evi.evar_concl in
-  evd := Evd.evar_define ev nc !evd;
-  let (evn,_) = destEvar nc in
-  mkEvar(evn,Array.of_list ncargs)
+    evd := Evd.evar_define ev nc !evd;
+    let (evn,_) = destEvar nc in
+      mkEvar(evn,Array.of_list ncargs)
+	
+
+exception Dependency_error of identifier
+	
+let rec check_and_clear_in_constr evd c ids =
+  (* returns a new constr where all the evars have been 'cleaned'
+     (ie the hypotheses ids have been removed from the contexts of
+     evars *)
+  let check id' = 
+    if List.mem id' ids then
+      raise (Dependency_error id')
+  in 
+    match kind_of_term c with
+      | ( Rel _ | Meta _ | Sort _ ) -> c
+      | ( Const _ | Ind _ | Construct _ ) -> 
+	  let vars = Environ.vars_of_global (Global.env()) c in
+	    List.iter check vars; c
+      | Var id' ->  
+	  check id'; mkVar id'
+      | Evar (e,l) -> 
+	  if Evd.is_defined_evar !evd (e,l) then
+	    (* If e is already defined we replace it by its definition *)
+	    let nc = nf_evar (evars_of !evd) c in 
+	      (check_and_clear_in_constr evd nc ids)
+	  else
+	    (* We check for dependencies to elements of ids in the
+	       evar_info corresponding to e and in the instance of
+	       arguments. Concurrently, we build a new evar
+	       corresponding to e where hypotheses of ids have been
+	       removed *)
+	    let evi = Evd.find (evars_of !evd) e in
+	    let nconcl = check_and_clear_in_constr evd (evar_concl evi) ids in
+	    let (nhyps,nargs) = 
+	      List.fold_right2 
+		(fun (id,ob,c) i (hy,ar) ->
+		  if List.mem id ids then
+		    (hy,ar)
+		  else
+		    let d' = (id,
+			     (match ob with 
+				 None -> None
+			       | Some b -> Some (check_and_clear_in_constr evd b ids)),
+			     check_and_clear_in_constr evd c ids) in
+		    let i' = check_and_clear_in_constr evd i ids in
+		      (d'::hy, i'::ar)
+		) 	      
+		(evar_context evi) (Array.to_list l) ([],[]) in
+	    let env = Sign.fold_named_context push_named nhyps ~init:(empty_env) in
+	    let ev'= e_new_evar evd env ~src:(evar_source e !evd) nconcl in
+	      evd := Evd.evar_define e ev' !evd;
+	      let (e',_) = destEvar ev' in
+		mkEvar(e', Array.of_list nargs)
+      | _ -> map_constr (fun c -> check_and_clear_in_constr evd c ids) c
+
+and clear_hyps_in_evi evd evi ids =
+  (* clear_evar_hyps erases hypotheses ids in evi, checking if some
+     hypothesis does not depend on a element of ids, and erases ids in
+     the contexts of the evars occuring in evi *)
+  let nconcl = try check_and_clear_in_constr evd (evar_concl evi) ids 
+    with Dependency_error id' -> error (string_of_id id' ^ " is used in conclusion") in
+  let (nhyps,_) = 
+    let aux (id,ob,c) = 
+      try
+	(id,
+	(match ob with 
+	    None -> None
+	  | Some b -> Some (check_and_clear_in_constr evd b ids)),
+	check_and_clear_in_constr evd c ids)
+      with Dependency_error id' -> error (string_of_id id' ^ " is used in hypothesis "
+					   ^ string_of_id id)
+    in
+      remove_hyps ids aux (evar_hyps evi)
+  in    
+    { evi with
+      evar_concl = nconcl;
+      evar_hyps  = nhyps}
+      
 
 let need_restriction k args = not (array_for_all (closedn k) args)
 
 (* We try to instantiate the evar assuming the body won't depend
  * on arguments that are not Rels or Vars, or appearing several times
-   (i.e. we tackle only Miller-Pfenning patterns unification) 
+ * (i.e. we tackle only Miller-Pfenning patterns unification) 
 
-  1) Let a unification problem "env |- ev[hyps:=args] = rhs"
-  2) We limit it to a patterns unification problem "env |- ev[subst] = rhs"
-     where only Rel's and Var's are relevant in subst
-  3) We recur on rhs, "imitating" the term failing if some Rel/Var not in scope
+ * 1) Let a unification problem "env |- ev[hyps:=args] = rhs"
+ * 2) We limit it to a patterns unification problem "env |- ev[subst] = rhs"
+ * where only Rel's and Var's are relevant in subst
+ * 3) We recur on rhs, "imitating" the term failing if some Rel/Var not in scope
 
-  Note: we don't assume rhs in normal form, it may fail while it would
-  have succeeded after some reductions
+ * Note: we don't assume rhs in normal form, it may fail while it would
+ * have succeeded after some reductions
  *)
 (* Note: error_not_clean should not be an error: it simply means that the
  * conversion test that lead to the faulty call to [real_clean] should return
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 3ac05481..896bf26c 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: evarutil.mli 9141 2006-09-15 10:07:01Z herbelin $ i*)
+(*i $Id: evarutil.mli 9573 2007-01-31 20:18:18Z notin $ i*)
 
 (*i*)
 open Util
@@ -158,3 +158,8 @@ val whd_castappevar :  evar_map -> constr -> constr
 
 val pr_tycon_type : env -> type_constraint_type -> Pp.std_ppcmds
 val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
+
+
+(**********************************)
+(* Removing hyps in evars'context *)
+val clear_hyps_in_evi : evar_defs ref -> evar_info -> identifier list -> evar_info
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 030983e1..c68a7a73 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evd.ml 9154 2006-09-20 17:18:18Z corbinea $ *)
+(* $Id: evd.ml 9573 2007-01-31 20:18:18Z notin $ *)
 
 open Pp
 open Util
@@ -77,6 +77,8 @@ let is_defined sigma ev =
   let info = find sigma ev in 
   not (info.evar_body = Evar_empty)
 
+let evar_concl ev = ev.evar_concl
+let evar_hyps ev = ev.evar_hyps
 let evar_body ev = ev.evar_body
 let evar_env evd = Global.env_of_context evd.evar_hyps
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 876c34d2..e1fc425b 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: evd.mli 9154 2006-09-20 17:18:18Z corbinea $ i*)
+(*i $Id: evd.mli 9573 2007-01-31 20:18:18Z notin $ i*)
 
 (*i*)
 open Util
@@ -56,6 +56,8 @@ val is_evar : evar_map -> evar -> bool
 
 val is_defined : evar_map -> evar -> bool
 
+val evar_concl : evar_info -> constr
+val evar_hyps : evar_info -> Environ.named_context_val
 val evar_body : evar_info -> evar_body
 val evar_env :  evar_info -> Environ.env
 
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 07ca5d83..eeddcb64 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: indrec.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
+(* $Id: indrec.ml 9519 2007-01-22 18:13:29Z notin $ *)
 
 open Pp
 open Util
@@ -422,16 +422,15 @@ let mis_make_indrec env sigma listdepkind mib =
 
       (* Body on make_one_rec *)
     let (indi,mibi,mipi,dep,kind) = List.nth listdepkind p in
-
-    if mis_is_recursive_subset
-      (List.map (fun (indi,_,_,_,_) -> snd indi) listdepkind)
-      mipi.mind_recargs
-    then 
-    let env' = push_rel_context lnamesparrec env in
-      it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind) 
-	lnamesparrec
-    else 
-      mis_make_case_com (Some dep) env sigma indi (mibi,mipi) kind 
+      if (mis_is_recursive_subset
+	     (List.map (fun (indi,_,_,_,_) -> snd indi) listdepkind)
+	     mipi.mind_recargs) 
+      then 
+	let env' = push_rel_context lnamesparrec env in
+	  it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind) 
+	    lnamesparrec
+      else 
+	mis_make_case_com (Some dep) env sigma indi (mibi,mipi) kind 
   in 
       (* Body of mis_make_indrec *)
   list_tabulate make_one_rec nrec
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 00dd034d..d7e3ac77 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: rawterm.ml 9226 2006-10-09 16:11:01Z herbelin $ *)
+(* $Id: rawterm.ml 9535 2007-01-26 09:26:08Z jforest $ *)
 
 (*i*)
 open Util
@@ -201,6 +201,70 @@ let occur_rawconstr id =
 
   in occur
 
+
+let add_name_to_ids set na = 
+  match na with 
+    | Anonymous -> set 
+    | Name id -> Idset.add id set 
+
+let free_rawvars  =
+  let rec vars bounded vs = function
+    | RVar (loc,id') -> if Idset.mem id' bounded then vs else Idset.add id' vs
+    | RApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args)
+    | RLambda (loc,na,ty,c) | RProd (loc,na,ty,c) | RLetIn (loc,na,ty,c) -> 
+	let vs' = vars bounded vs ty in 
+	let bounded' = add_name_to_ids bounded na in 
+	vars bounded' vs' c
+    | RCases (loc,rtntypopt,tml,pl) ->
+	let vs1 = vars_option bounded vs rtntypopt in 
+	let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in 
+	List.fold_left (vars_pattern bounded) vs2 pl
+    | RLetTuple (loc,nal,rtntyp,b,c) ->
+	let vs1 = vars_return_type bounded vs rtntyp in 
+	let vs2 = vars bounded vs1 b in 
+	let bounded' = List.fold_left add_name_to_ids bounded nal in
+	vars bounded' vs2 c
+    | RIf (loc,c,rtntyp,b1,b2) -> 
+	let vs1 = vars_return_type bounded vs rtntyp in 
+	let vs2 = vars bounded vs1 c in 
+	let vs3 = vars bounded vs2 b1 in 
+	vars bounded vs3 b2
+    | RRec (loc,fk,idl,bl,tyl,bv) ->
+	let bounded' = Array.fold_right Idset.add idl bounded in 
+	let vars_fix i vs fid = 
+	  let vs1,bounded1 = 
+	    List.fold_left 
+	      (fun (vs,bounded) (na,bbd,bty) -> 
+		 let vs' = vars_option bounded vs bbd in 
+		 let vs'' = vars bounded vs' bty in
+		 let bounded' = add_name_to_ids bounded na in 
+		 (vs'',bounded')
+	      )
+	      (vs,bounded')
+	      bl.(i)
+	  in
+	  let vs2 = vars bounded1 vs1 tyl.(i) in 
+	  vars bounded1 vs2 bv.(i)
+	in
+	array_fold_left_i vars_fix vs idl
+    | RCast (loc,c,_,t) -> vars bounded (vars bounded vs c) t
+    | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> vs
+
+  and vars_pattern bounded vs (loc,idl,p,c) = 
+    let bounded' = List.fold_right Idset.add idl bounded  in 
+    vars bounded' vs c
+
+  and vars_option bounded vs = function None -> vs | Some p -> vars bounded vs p
+
+  and vars_return_type bounded vs (na,tyopt) = 
+    let bounded' = add_name_to_ids bounded na in 
+    vars_option bounded' vs tyopt
+  in 
+  fun rt -> 
+    let vs = vars Idset.empty Idset.empty rt in 
+    Idset.elements vs
+
+
 let loc_of_rawconstr = function
   | RRef (loc,_) -> loc
   | RVar (loc,_) -> loc
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 6c2276d7..e5601705 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: rawterm.mli 9226 2006-10-09 16:11:01Z herbelin $ i*)
+(*i $Id: rawterm.mli 9535 2007-01-26 09:26:08Z jforest $ i*)
 
 (*i*)
 open Util
@@ -113,7 +113,7 @@ val map_rawconstr_with_binders_loc : loc ->
 i*)
 
 val occur_rawconstr : identifier -> rawconstr -> bool
-
+val free_rawvars : rawconstr -> identifier list
 val loc_of_rawconstr : rawconstr -> loc
 
 (**********************************************************************)
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 9b8764f2..6b7e1fb7 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: termops.ml 9314 2006-10-29 20:11:08Z herbelin $ *)
+(* $Id: termops.ml 9429 2006-12-12 08:01:03Z herbelin $ *)
 
 open Pp
 open Util
@@ -912,7 +912,7 @@ let next_name_not_occuring is_goal_ccl name l env_names t =
         (* Normally, an anonymous name is not dependent and will not be *)
         (* taken into account by the function concrete_name; just in case *)
         (* invent a valid name *)
-        id_of_string "H"
+        next (id_of_string "H")
 
 (* On reduit une serie d'eta-redex de tete ou rien du tout  *)
 (* [x1:c1;...;xn:cn]@(f;a1...an;x1;...;xn) --> @(f;a1...an) *)
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 63fdd6d5..6fa05fa5 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: typing.ml 9310 2006-10-28 19:35:09Z herbelin $ *)
+(* $Id: typing.ml 9511 2007-01-22 08:27:31Z herbelin $ *)
 
 open Util
 open Names
@@ -29,6 +29,15 @@ let meta_type env mv =
 let vect_lift = Array.mapi lift
 let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t)
 
+let constant_type_knowing_parameters env cst jl =
+  let paramstyp = Array.map (fun j -> j.uj_type) jl in
+  type_of_constant_knowing_parameters env (constant_type env cst) paramstyp
+
+let inductive_type_knowing_parameters env ind jl =
+  let (mib,mip) = lookup_mind_specif env ind in
+  let paramstyp = Array.map (fun j -> j.uj_type) jl in
+  Inductive.type_of_inductive_knowing_parameters env mip paramstyp
+
 (* The typing machine without information, without universes but with
    existential variables. *)
 
@@ -93,12 +102,14 @@ let rec execute env evd cstr =
 	  match kind_of_term f with
 	    | Ind ind ->
 		(* Sort-polymorphism of inductive types *)
-		judge_of_inductive_knowing_parameters env ind
-		  (jv_nf_evar (evars_of evd) jl)
+		make_judge f
+		  (inductive_type_knowing_parameters env ind
+		    (jv_nf_evar (evars_of evd) jl))
 	    | Const cst -> 
 		(* Sort-polymorphism of inductive types *)
-		judge_of_constant_knowing_parameters env cst
-		  (jv_nf_evar (evars_of evd) jl)
+		make_judge f
+		  (constant_type_knowing_parameters env cst
+		    (jv_nf_evar (evars_of evd) jl))
 	    | _ -> 
 		execute env evd f
 	in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index fabe24ef..5fb8054f 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: unification.ml 9217 2006-10-05 17:31:23Z notin $ *)
+(* $Id: unification.ml 9517 2007-01-22 17:37:58Z herbelin $ *)
 
 open Pp
 open Util
@@ -113,16 +113,15 @@ let unify_0 env sigma cv_pb mod_delta m n =
 	| LetIn (_,b,_,c), _ -> unirec_rec curenv  pb substn (subst1 b c) cN
 	| _, LetIn (_,b,_,c) -> unirec_rec curenv  pb substn cM (subst1 b c)
 	    
-	| App (f1,l1), App (f2,l2) ->
-	    if
-	      isMeta f1 & is_unification_pattern f1 l1 & not (dependent f1 cN)
-	    then
+	| App (f1,l1), _ when
+	    isMeta f1 & is_unification_pattern f1 l1 & not (dependent f1 cN) ->
 	      solve_pattern_eqn_array curenv f1 l1 cN substn
-	    else if
-		isMeta f2 & is_unification_pattern f2 l2 & not (dependent f2 cM)
-	    then
+
+	| _, App (f2,l2) when
+	    isMeta f2 & is_unification_pattern f2 l2 & not (dependent f2 cM) ->
 	      solve_pattern_eqn_array curenv f2 l2 cM substn
-	    else
+
+	| App (f1,l1), App (f2,l2) ->
 	      let len1 = Array.length l1
 	      and len2 = Array.length l2 in
               let (f1,l1,f2,l2) =
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 55f798de..46d67406 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -42,31 +42,30 @@ let find_rectype_a env c =
   | _ -> raise Not_found
 
 (* Instantiate inductives and parameters in constructor type *)
-let build_type_constructor mind mib params ctyp =
-  let si = ind_subst mind mib in
-  let ctyp1 = substl si ctyp in
+
+let type_constructor mind mib typ params = 
+  let s = ind_subst mind mib in
+  let ctyp = substl s typ in
   let nparams = Array.length params in
-  if nparams = 0 then ctyp1
+  if nparams = 0 then ctyp
   else
-    let _,ctyp2 = decompose_prod_n nparams ctyp1 in
-    let sp = List.rev (Array.to_list params) in substl sp ctyp2
-   
-let construct_of_constr_const env tag typ =
-  let ind,params = find_rectype env typ in
-  let (_,mip) = lookup_mind_specif env ind in
-  let i = invert_tag true tag mip.mind_reloc_tbl in
-  applistc (mkConstruct(ind,i)) params
+    let _,ctyp = decompose_prod_n nparams ctyp in   
+    substl (List.rev (Array.to_list params)) ctyp
 
-let construct_of_constr_block env tag typ =
+let construct_of_constr const env tag typ =
   let (mind,_ as ind), allargs = find_rectype_a env typ in
-  let (mib,mip) = lookup_mind_specif env ind in
+  let mib,mip = lookup_mind_specif env ind in
   let nparams = mib.mind_nparams in
-  let i = invert_tag false tag mip.mind_reloc_tbl in
+  let i = invert_tag const tag mip.mind_reloc_tbl in
   let params = Array.sub allargs 0 nparams in
-  let specif = mip.mind_nf_lc in
-  let ctyp = build_type_constructor mind mib params specif.(i-1) in
+  let ctyp = type_constructor mind mib (mip.mind_nf_lc.(i-1)) params in
   (mkApp(mkConstruct(ind,i), params), ctyp)
-  	
+
+let construct_of_constr_const env tag typ = 
+  fst (construct_of_constr true env tag typ)
+
+let construct_of_constr_block = construct_of_constr false
+
 let constr_type_of_idkey env idkey =
   match idkey with
   | ConstKey cst ->
@@ -87,7 +86,7 @@ let build_branches_type env (mind,_ as _ind) mib mip params dep p =
   (* [build_one_branch i cty] construit le type de la ieme branche (commence
      a 0) et les lambda correspondant aux realargs *)
   let build_one_branch i cty =
-    let typi = build_type_constructor mind mib params cty in
+    let typi = type_constructor mind mib cty params in
     let decl,indapp = Term.decompose_prod typi in
     let ind,cargs = find_rectype_a env indapp in
     let nparams = Array.length params in