1 files changed, 194 insertions, 205 deletions

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index b9e0e62a..a2577e2b 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -2,26 +2,30 @@ open Printer
 open Pp
 open Names
 open Term
+open Vars
 open Glob_term
-open Libnames
+open Glob_ops
+open Globnames
 open Indfun_common
+open Errors
 open Util
 open Glob_termops
+open Misctypes
 
 let observe strm =
   if do_observe ()
-  then Pp.msgnl strm
+  then Pp.msg_debug strm
   else ()
-let observennl strm =
+(*let observennl strm =
   if do_observe ()
   then Pp.msg strm
-  else ()
+  else ()*)
 
 
 type binder_type =
-  | Lambda of name
-  | Prod of name
-  | LetIn of name
+  | Lambda of Name.t
+  | Prod of Name.t
+  | LetIn of Name.t
 
 type glob_context = (binder_type*glob_constr) list
 
@@ -54,7 +58,7 @@ type 'a build_entry_pre_return =
 type 'a build_entry_return =
     {
       result : 'a build_entry_pre_return list;
-      to_avoid : identifier list
+      to_avoid : Id.t list
     }
 
 (*
@@ -86,7 +90,7 @@ let combine_results
   in (* and then we flatten the map *)
   {
     result = List.concat pre_result;
-    to_avoid = list_union res1.to_avoid res2.to_avoid
+    to_avoid = List.union Id.equal res1.to_avoid res2.to_avoid
   }
 
 
@@ -111,9 +115,9 @@ let ids_of_binder =  function
 let rec change_vars_in_binder mapping = function
     [] -> []
   | (bt,t)::l ->
-      let new_mapping = List.fold_right Idmap.remove (ids_of_binder bt) mapping in
+      let new_mapping = List.fold_right Id.Map.remove (ids_of_binder bt) mapping in
       (bt,change_vars mapping t)::
-	(if idmap_is_empty new_mapping
+	(if Id.Map.is_empty new_mapping
 	 then l
 	 else change_vars_in_binder new_mapping l
 	)
@@ -122,7 +126,7 @@ let rec replace_var_by_term_in_binder x_id term = function
   | [] -> []
   | (bt,t)::l ->
       (bt,replace_var_by_term x_id term t)::
-	if List.mem x_id (ids_of_binder bt)
+	if Id.List.mem x_id (ids_of_binder bt)
 	then l
 	else replace_var_by_term_in_binder x_id term l
 
@@ -130,28 +134,28 @@ let add_bt_names bt = List.append (ids_of_binder bt)
 
 let apply_args ctxt body args =
   let need_convert_id avoid id =
-    List.exists (is_free_in id) args || List.mem id avoid
+    List.exists (is_free_in id) args || Id.List.mem id avoid
   in
   let need_convert avoid  bt =
     List.exists (need_convert_id avoid) (ids_of_binder bt)
   in
-  let next_name_away (na:name) (mapping: identifier Idmap.t) (avoid: identifier list) =
+  let next_name_away (na:Name.t) (mapping: Id.t Id.Map.t) (avoid: Id.t list) =
     match na with
-       | Name id when List.mem id avoid ->
+       | Name id when Id.List.mem id avoid ->
 	   let new_id = Namegen.next_ident_away id avoid in
-	   Name new_id,Idmap.add id new_id mapping,new_id::avoid
+	   Name new_id,Id.Map.add id new_id mapping,new_id::avoid
        | _ -> na,mapping,avoid
   in
-  let next_bt_away bt (avoid:identifier list) =
+  let next_bt_away bt (avoid:Id.t list) =
     match bt with
       | LetIn na ->
-	  let new_na,mapping,new_avoid = next_name_away na Idmap.empty avoid  in
+	  let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid  in
 	  LetIn new_na,mapping,new_avoid
       | Prod na ->
-	  let new_na,mapping,new_avoid = next_name_away na Idmap.empty avoid  in
+	  let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid  in
 	  Prod new_na,mapping,new_avoid
       | Lambda na ->
-	  let new_na,mapping,new_avoid = next_name_away na Idmap.empty avoid  in
+	  let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid  in
 	  Lambda new_na,mapping,new_avoid
   in
   let rec do_apply avoid ctxt body args =
@@ -170,7 +174,7 @@ let apply_args ctxt body args =
 	      let new_avoid =  id::avoid in
 	      let new_id = Namegen.next_ident_away id new_avoid in
 	      let new_avoid' = new_id :: new_avoid in
-	      let mapping = Idmap.add id new_id Idmap.empty in
+	      let mapping = Id.Map.add id new_id Id.Map.empty in
 	      let new_ctxt' = change_vars_in_binder mapping ctxt' in
 	      let new_body = change_vars mapping body in
 	      new_avoid',new_ctxt',new_body,new_id
@@ -266,11 +270,11 @@ let make_discr_match_el  =
   end
 *)
 let make_discr_match_brl i =
-  list_map_i
+  List.map_i
     (fun j (_,idl,patl,_) ->
-       if j=i
-       then (dummy_loc,idl,patl, mkGRef (Lazy.force coq_True_ref))
-       else (dummy_loc,idl,patl, mkGRef (Lazy.force coq_False_ref))
+       if Int.equal j i
+       then (Loc.ghost,idl,patl, mkGRef (Lazy.force coq_True_ref))
+       else (Loc.ghost,idl,patl, mkGRef (Lazy.force coq_False_ref))
     )
     0
 (*
@@ -285,10 +289,6 @@ let make_discr_match brl =
 	   make_discr_match_el el,
 	   make_discr_match_brl i brl)
 
-let pr_name = function
-  | Name id -> Ppconstr.pr_id id
-  | Anonymous -> str "_"
-
 (**********************************************************************)
 (*  functions used to build case expression from lettuple and if ones *)
 (**********************************************************************)
@@ -304,18 +304,17 @@ let build_constructors_of_type ind' argl =
 		  Impargs.implicits_of_global constructref
 		in
 		let cst_narg =
-		  Inductiveops.mis_constructor_nargs_env
+		  Inductiveops.constructor_nallargs_env
 		    (Global.env ())
 		    construct
 		in
-		let argl = match argl with
-                | None ->
+		let argl =
+		  if List.is_empty argl
+		  then
  		    Array.to_list
-		      (Array.init cst_narg (fun _ -> mkGHole ())
+		      (Array.init (cst_narg - npar) (fun _ -> mkGHole ())
 		      )
-                | Some l ->
-	            Array.to_list
-		      (Array.init npar (fun _ -> mkGHole ()))@l
+		  else argl
 		in
 		let pat_as_term =
 		  mkGApp(mkGRef (ConstructRef(ind',i+1)),argl)
@@ -324,40 +323,6 @@ let build_constructors_of_type ind' argl =
 	     )
     ind.Declarations.mind_consnames
 
-(* [find_type_of] very naive attempts to discover the type of an if or a letin *)
-let rec find_type_of nb b =
-  let f,_ = glob_decompose_app b in
-  match f with
-    | GRef(_,ref) ->
-	begin
-	  let ind_type  =
-	    match ref with
-	      | VarRef _ | ConstRef _ ->
-		  let constr_of_ref = constr_of_global ref in
-		  let type_of_ref = Typing.type_of (Global.env ()) Evd.empty constr_of_ref in
-		  let (_,ret_type) = Reduction.dest_prod (Global.env ()) type_of_ref in
-		  let ret_type,_ = decompose_app ret_type in
-		  if not (isInd ret_type) then
-		    begin
-(* 		      Pp.msgnl (str "not an inductive" ++ pr_lconstr ret_type); *)
-		      raise (Invalid_argument "not an inductive")
-		    end;
-		  destInd ret_type
-	      | IndRef ind -> ind
-	      | ConstructRef c -> fst c
-	  in
-	  let _,ind_type_info = Inductive.lookup_mind_specif (Global.env()) ind_type in
-	  if not (Array.length ind_type_info.Declarations.mind_consnames = nb )
-	  then raise (Invalid_argument "find_type_of : not a valid inductive");
-	  ind_type
-	end
-    | GCast(_,b,_) -> find_type_of nb b
-    | GApp _ -> assert false (* we have decomposed any application via glob_decompose_app *)
-    | _ -> raise (Invalid_argument "not a ref")
-
-
-
-
 (******************)
 (* Main functions *)
 (******************)
@@ -368,14 +333,14 @@ let raw_push_named (na,raw_value,raw_typ) env =
   match na with
     | Anonymous -> env
     | Name id ->
-	let value = Option.map (Pretyping.Default.understand Evd.empty env) raw_value in
-	let typ = Pretyping.Default.understand_type Evd.empty env raw_typ in
+	let value = Option.map (fun x-> fst (Pretyping.understand env Evd.empty x)) raw_value in
+	let typ,ctx = Pretyping.understand env Evd.empty ~expected_type:Pretyping.IsType raw_typ in
 	Environ.push_named (id,value,typ) env
 
 
 let add_pat_variables pat typ env : Environ.env =
   let rec add_pat_variables env pat typ  : Environ.env =
-    observe (str "new rel env := " ++ Printer.pr_rel_context_of env);
+    observe (str "new rel env := " ++ Printer.pr_rel_context_of env Evd.empty);
 
     match pat with
       | PatVar(_,na) -> Environ.push_rel (na,None,typ) env
@@ -385,14 +350,14 @@ let add_pat_variables pat typ env : Environ.env =
 	    with Not_found -> assert false
 	  in
 	  let constructors = Inductiveops.get_constructors env indf in
-	  let constructor : Inductiveops.constructor_summary = List.find (fun cs -> cs.Inductiveops.cs_cstr = c) (Array.to_list constructors) in
+	  let constructor : Inductiveops.constructor_summary = List.find (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr)) (Array.to_list constructors) in
 	  let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in
 	  List.fold_left2 add_pat_variables env patl (List.rev cs_args_types)
   in
   let new_env = add_pat_variables  env pat typ in
   let res =
     fst (
-      Sign.fold_rel_context
+      Context.fold_rel_context
 	(fun (na,v,t) (env,ctxt) ->
 	 match na with
 	   | Anonymous -> assert false
@@ -411,7 +376,7 @@ let add_pat_variables pat typ env : Environ.env =
 	~init:(env,[])
     )
   in
-  observe (str "new var env := " ++ Printer.pr_named_context_of res);
+  observe (str "new var env := " ++ Printer.pr_named_context_of res Evd.empty);
   res
 
 
@@ -423,7 +388,7 @@ let rec pattern_to_term_and_type env typ  = function
 	mkGVar id
   | PatCstr(loc,constr,patternl,_) ->
       let cst_narg =
-	Inductiveops.mis_constructor_nargs_env
+	Inductiveops.constructor_nallargs_env
 	  (Global.env ())
 	  constr
       in
@@ -432,7 +397,7 @@ let rec pattern_to_term_and_type env typ  = function
 	with Not_found -> assert false
       in
       let constructors = Inductiveops.get_constructors env indf in
-      let constructor  = List.find (fun cs -> cs.Inductiveops.cs_cstr = constr) (Array.to_list constructors) in
+      let constructor  = List.find (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr) (Array.to_list constructors) in
       let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in
       let _,cstl = Inductiveops.dest_ind_family indf in
       let csta = Array.of_list cstl in
@@ -440,7 +405,7 @@ let rec pattern_to_term_and_type env typ  = function
 	Array.to_list
 	  (Array.init
 	     (cst_narg - List.length patternl)
-	     (fun i -> Detyping.detype false [] (Termops.names_of_rel_context env) csta.(i))
+	     (fun i -> Detyping.detype false [] env Evd.empty csta.(i))
 	  )
       in
       let patl_as_term =
@@ -508,12 +473,12 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 		    | u::l -> 
 			match t with 
 			  | GLambda(loc,na,_,nat,b) -> 
-			      GLetIn(dummy_loc,na,u,aux b l)
+			      GLetIn(Loc.ghost,na,u,aux b l)
 			  | _ -> 
-			      GApp(dummy_loc,t,l)
+			      GApp(Loc.ghost,t,l)
 		in
 		build_entry_lc env funnames avoid (aux f args)
-	    | GVar(_,id) when Idset.mem id funnames ->
+	    | GVar(_,id) when Id.Set.mem id funnames ->
 		(* if we have [f t1 ... tn] with [f]$\in$[fnames]
 		   then we create a fresh variable [res],
 		   add [res] and its "value" (i.e. [res v1 ... vn]) to each
@@ -521,10 +486,10 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 		   a pseudo value "v1 ... vn".
 		   The "value" of this branch is then simply [res]
 		*)
-		let rt_as_constr = Pretyping.Default.understand Evd.empty env rt in
+		let rt_as_constr,ctx = Pretyping.understand env Evd.empty rt in
 		let rt_typ = Typing.type_of env Evd.empty rt_as_constr in
-		let res_raw_type = Detyping.detype false [] (Termops.names_of_rel_context env) rt_typ in
-		let res = fresh_id args_res.to_avoid "res" in
+		let res_raw_type = Detyping.detype false [] env Evd.empty rt_typ in
+		let res = fresh_id args_res.to_avoid "_res" in
 		let new_avoid = res::args_res.to_avoid in
 		let res_rt = mkGVar res in
 		let new_result =
@@ -568,7 +533,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 			let new_b =
 			  replace_var_by_term
 			    id
-			    (GVar(dummy_loc,id))
+			    (GVar(Loc.ghost,id))
 			    b
 			in
 			(Name new_id,new_b,new_avoid)
@@ -629,7 +594,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	   and combine the two result
 	*)
 	let v_res = build_entry_lc env funnames avoid v in
-	let v_as_constr = Pretyping.Default.understand Evd.empty env v in
+	let v_as_constr,ctx = Pretyping.understand env Evd.empty v in
 	let v_type = Typing.type_of env Evd.empty v_as_constr in
 	let new_env =
 	  match n with
@@ -645,7 +610,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	let make_discr = make_discr_match brl in
 	build_entry_lc_from_case env funnames make_discr el brl avoid
     | GIf(_,b,(na,e_option),lhs,rhs) ->
-	let b_as_constr = Pretyping.Default.understand Evd.empty env b in
+	let b_as_constr,ctx = Pretyping.understand env Evd.empty b in
 	let b_typ = Typing.type_of env Evd.empty b_as_constr in
 	let (ind,_) =
 	  try Inductiveops.find_inductive env Evd.empty b_typ
@@ -654,11 +619,11 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 			       Printer.pr_glob_constr b ++ str " in " ++
 			       Printer.pr_glob_constr rt ++ str ". try again with a cast")
 	in
-	let case_pats = build_constructors_of_type ind None in
-	assert (Array.length case_pats = 2);
+	let case_pats = build_constructors_of_type (fst ind) [] in
+	assert (Int.equal (Array.length case_pats) 2);
 	let brl =
-	  list_map_i
-	    (fun i x -> (dummy_loc,[],[case_pats.(i)],x))
+	  List.map_i
+	    (fun i x -> (Loc.ghost,[],[case_pats.(i)],x))
 	    0
 	    [lhs;rhs]
 	in
@@ -670,14 +635,14 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
     | GLetTuple(_,nal,_,b,e) ->
 	begin
 	  let nal_as_glob_constr =
-	    Some (List.map
+	    List.map
 	      (function
 		   Name id -> mkGVar id
 		 | Anonymous -> mkGHole ()
 	      )
-	      nal)
+	      nal
 	  in
-	  let b_as_constr = Pretyping.Default.understand Evd.empty env b in
+	  let b_as_constr,ctx = Pretyping.understand env Evd.empty b in
 	  let b_typ = Typing.type_of env Evd.empty b_as_constr in
 	  let (ind,_) =
 	    try Inductiveops.find_inductive env Evd.empty b_typ
@@ -686,10 +651,10 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 				 Printer.pr_glob_constr b ++ str " in " ++
 				 Printer.pr_glob_constr rt ++ str ". try again with a cast")
 	  in
-	  let case_pats = build_constructors_of_type ind nal_as_glob_constr in
-	  assert (Array.length case_pats = 1);
+	  let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in
+	  assert (Int.equal (Array.length case_pats) 1);
 	  let br =
-	    (dummy_loc,[],[case_pats.(0)],e)
+	    (Loc.ghost,[],[case_pats.(0)],e)
 	  in
 	  let match_expr = mkGCases(None,[b,(Anonymous,None)],[br]) in
 	  build_entry_lc env funnames avoid match_expr
@@ -724,7 +689,7 @@ and build_entry_lc_from_case env funname make_discr
 	in
 	let types =
 	  List.map (fun (case_arg,_) ->
-		      let case_arg_as_constr = Pretyping.Default.understand Evd.empty env case_arg in
+		      let case_arg_as_constr,ctx = Pretyping.understand env Evd.empty case_arg in
 		      Typing.type_of env Evd.empty case_arg_as_constr
 		   ) el
 	in
@@ -746,7 +711,8 @@ and build_entry_lc_from_case env funname make_discr
 	{
 	  result = List.concat (List.map (fun r -> r.result) results);
 	  to_avoid =
-	    List.fold_left (fun acc r -> list_union acc r.to_avoid) [] results
+	    List.fold_left (fun acc r -> List.union Id.equal acc r.to_avoid)
+              [] results
 	}
 
 and build_entry_lc_from_case_term env types funname make_discr patterns_to_prevent brl avoid
@@ -761,7 +727,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 	   (will be used in the following recursive calls)
 	*)
 	let new_env = List.fold_right2 add_pat_variables patl types env in
-	let not_those_patterns : (identifier list -> glob_constr -> glob_constr) list =
+	let not_those_patterns : (Id.t list -> glob_constr -> glob_constr) list =
 	  List.map2
 	    (fun pat typ ->
 	       fun avoid pat'_as_term ->
@@ -775,7 +741,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 			in
 			let raw_typ_of_id =
 			  Detyping.detype false []
-			    (Termops.names_of_rel_context env_with_pat_ids) typ_of_id
+			    env_with_pat_ids Evd.empty typ_of_id
 			in
 			mkGProd (Name id,raw_typ_of_id,acc))
 		     pat_ids
@@ -816,18 +782,18 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
       	let those_pattern_preconds =
 	  (List.flatten
 	    (
-	      list_map3
+	      List.map3
 	      (fun pat e typ_as_constr ->
 		 let this_pat_ids = ids_of_pat pat in
-		 let typ = Detyping.detype false [] (Termops.names_of_rel_context new_env) typ_as_constr in
+		 let typ = Detyping.detype false [] new_env Evd.empty typ_as_constr in
 		 let pat_as_term = pattern_to_term pat in
 		 List.fold_right
 		   (fun id  acc ->
-		      if Idset.mem id this_pat_ids
+		      if Id.Set.mem id this_pat_ids
 		      then (Prod (Name id),
 		      let typ_of_id = Typing.type_of new_env Evd.empty (mkVar id) in
 		      let raw_typ_of_id =
-			Detyping.detype false [] (Termops.names_of_rel_context new_env) typ_of_id
+			Detyping.detype false [] new_env Evd.empty typ_of_id
 		      in
 		      raw_typ_of_id
 			   )::acc
@@ -871,14 +837,14 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 
 let is_res id =
   try
-    String.sub (string_of_id id) 0 3 = "res"
+    String.equal (String.sub (Id.to_string id) 0 4) "_res"
   with Invalid_argument _ -> false
 
 
 
 let same_raw_term rt1 rt2 = 
   match rt1,rt2 with 
-    | GRef(_,r1), GRef (_,r2) -> r1=r2
+    | GRef(_,r1,_), GRef (_,r2,_) -> Globnames.eq_gr r1 r2
     | GHole _, GHole _ -> true
     | _ -> false
 let decompose_raw_eq lhs rhs = 
@@ -892,7 +858,7 @@ let decompose_raw_eq lhs rhs =
     observe (str "lrhs := " ++ int (List.length lrhs));
     let sllhs = List.length llhs in 
     let slrhs = List.length lrhs in 
-    if same_raw_term lhd rhd && sllhs = slrhs 
+    if same_raw_term lhd rhd && Int.equal sllhs slrhs 
     then
       (* let _ = assert false in  *)
       List.fold_right2 decompose_raw_eq	llhs lrhs acc
@@ -928,7 +894,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 			let new_t =
 			  mkGApp(mkGVar(mk_rel_id this_relname),args'@[res_rt])
 			in
-			let t' = Pretyping.Default.understand Evd.empty env new_t in
+			let t',ctx = Pretyping.understand env Evd.empty new_t in
 			let new_env = Environ.push_rel (n,None,t') env in
 			let new_b,id_to_exclude =
 			  rebuild_cons new_env
@@ -937,18 +903,18 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 			    (depth + 1) b
 			in
 			mkGProd(n,new_t,new_b),
-			Idset.filter not_free_in_t id_to_exclude
+			Id.Set.filter not_free_in_t id_to_exclude
 		    | _ -> (* the first args is the name of the function! *)
 			assert false
 		end
-	    | GApp(loc1,GRef(loc2,eq_as_ref),[ty;GVar(loc3,id);rt])
-		when  eq_as_ref = Lazy.force Coqlib.coq_eq_ref  && n = Anonymous
+	    | GApp(loc1,GRef(loc2,eq_as_ref,_),[ty;GVar(loc3,id);rt])
+		when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref)  && n == Anonymous
 		  ->
 		begin
 		  try
 		    observe (str "computing new type for eq : " ++ pr_glob_constr rt);
 		    let t' =
-		      try Pretyping.Default.understand Evd.empty env t
+		      try fst (Pretyping.understand env Evd.empty t)(*FIXME*)
                       with e when Errors.noncritical e -> raise Continue
 		    in
 		    let is_in_b = is_free_in id b in
@@ -970,36 +936,36 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    in
 		    mkGProd(n,t,new_b),id_to_exclude
 		  with Continue ->
-		    let jmeq = Libnames.IndRef (destInd (jmeq ())) in
-		    let ty' = Pretyping.Default.understand Evd.empty env ty in
+		    let jmeq = Globnames.IndRef (fst (destInd (jmeq ()))) in
+		    let ty',ctx = Pretyping.understand env Evd.empty ty in
 		    let ind,args' = Inductive.find_inductive env ty' in
-		    let mib,_ = Global.lookup_inductive ind in
+		    let mib,_ = Global.lookup_inductive (fst ind) in
 		    let nparam = mib.Declarations.mind_nparams in
 		    let params,arg' =
-		      ((Util.list_chop nparam args'))
+		      ((Util.List.chop nparam args'))
 		    in
 		    let rt_typ =
-		       GApp(Util.dummy_loc,
-			    GRef (Util.dummy_loc,Libnames.IndRef ind),
+		       GApp(Loc.ghost,
+			    GRef (Loc.ghost,Globnames.IndRef (fst ind),None),
 			    (List.map
 			      (fun p -> Detyping.detype false []
-				 (Termops.names_of_rel_context env)
+				 env Evd.empty
 				 p) params)@(Array.to_list
 				      (Array.make
 					 (List.length args' - nparam)
 					 (mkGHole ()))))
 		    in
 		    let eq' =
-		      GApp(loc1,GRef(loc2,jmeq),[ty;GVar(loc3,id);rt_typ;rt])
+		      GApp(loc1,GRef(loc2,jmeq,None),[ty;GVar(loc3,id);rt_typ;rt])
 		    in
 		    observe (str "computing new type for jmeq : " ++ pr_glob_constr eq');
-		    let eq'_as_constr = Pretyping.Default.understand Evd.empty env eq' in
+		    let eq'_as_constr,ctx = Pretyping.understand env Evd.empty eq' in
 		    observe (str " computing new type for jmeq : done") ;
 		    let new_args =
 		      match kind_of_term eq'_as_constr with
 			| App(_,[|_;_;ty;_|]) ->
 			    let ty = Array.to_list (snd (destApp ty)) in
-			    let ty' = snd (Util.list_chop nparam ty) in
+			    let ty' = snd (Util.List.chop nparam ty) in
 			    List.fold_left2
 			      (fun acc var_as_constr arg ->
 				 if isRel var_as_constr
@@ -1011,11 +977,13 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 				     | Anonymous -> acc
 				     | Name id' ->
 					 (id',Detyping.detype false []
-					    (Termops.names_of_rel_context env)
+					    env
+                                            Evd.empty
 					    arg)::acc
 				 else if isVar var_as_constr
 				 then (destVar var_as_constr,Detyping.detype false []
-					 (Termops.names_of_rel_context env)
+					 env
+                                         Evd.empty
 					 arg)::acc
 				 else acc
 			      )
@@ -1041,7 +1009,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		     if is_in_b then b else  replace_var_by_term id rt b
 		    in
 		    let new_env =
-		      let t' = Pretyping.Default.understand Evd.empty env eq' in
+		      let t',ctx = Pretyping.understand env Evd.empty eq' in
 		      Environ.push_rel (n,None,t') env
 		    in
 		    let new_b,id_to_exclude =
@@ -1056,10 +1024,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		  (* J.F:. keep this comment  it explain how to remove some meaningless equalities
 		     if keep_eq then
 		     mkGProd(n,t,new_b),id_to_exclude
-		     else new_b, Idset.add id id_to_exclude
+		     else new_b, Id.Set.add id id_to_exclude
 		  *)
-	    | GApp(loc1,GRef(loc2,eq_as_ref),[ty;rt1;rt2])
-		when  eq_as_ref = Lazy.force Coqlib.coq_eq_ref  && n = Anonymous
+	    | GApp(loc1,GRef(loc2,eq_as_ref,_),[ty;rt1;rt2])
+		when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous
 		  ->
 	      begin
 		try 
@@ -1079,7 +1047,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		  else raise Continue
 	      with Continue -> 
 		observe (str "computing new type for prod : " ++ pr_glob_constr rt);
-		let t' = Pretyping.Default.understand Evd.empty env t in
+		let t',ctx = Pretyping.understand env Evd.empty t in
 		let new_env = Environ.push_rel (n,None,t') env in
 		let new_b,id_to_exclude =
 		  rebuild_cons new_env
@@ -1088,14 +1056,14 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    (depth + 1) b
 		in
 		match n with
-		  | Name id when Idset.mem id id_to_exclude && depth >= nb_args ->
-		      new_b,Idset.remove id
-			(Idset.filter not_free_in_t id_to_exclude)
-		  | _ -> mkGProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude
+		  | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args ->
+		      new_b,Id.Set.remove id
+			(Id.Set.filter not_free_in_t id_to_exclude)
+		  | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
 	      end
 	    | _ ->
 		observe (str "computing new type for prod : " ++ pr_glob_constr rt);
-		let t' = Pretyping.Default.understand Evd.empty env t in
+		let t',ctx = Pretyping.understand env Evd.empty t in
 		let new_env = Environ.push_rel (n,None,t') env in
 		let new_b,id_to_exclude =
 		  rebuild_cons new_env
@@ -1104,17 +1072,17 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    (depth + 1) b
 		in
 		match n with
-		  | Name id when Idset.mem id id_to_exclude && depth >= nb_args ->
-		      new_b,Idset.remove id
-			(Idset.filter not_free_in_t id_to_exclude)
-		  | _ -> mkGProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude
+		  | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args ->
+		      new_b,Id.Set.remove id
+			(Id.Set.filter not_free_in_t id_to_exclude)
+		  | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
 	end
     | GLambda(_,n,k,t,b) ->
 	begin
 	  let not_free_in_t id = not (is_free_in id t) in
 	  let new_crossed_types = t :: crossed_types in
 	  observe (str "computing new type for lambda : " ++ pr_glob_constr rt);
-	  let t' = Pretyping.Default.understand Evd.empty env t in
+	  let t',ctx = Pretyping.understand env Evd.empty t in
 	  match n with
 	    | Name id ->
 		let new_env = Environ.push_rel (n,None,t') env in
@@ -1124,19 +1092,19 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    (args@[mkGVar id])new_crossed_types
 		    (depth + 1 ) b
 		in
-		if Idset.mem id id_to_exclude && depth >= nb_args
+		if Id.Set.mem id id_to_exclude && depth >= nb_args
 		then
-		  new_b, Idset.remove id (Idset.filter not_free_in_t id_to_exclude)
+		  new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
 		else
-		  GProd(dummy_loc,n,k,t,new_b),Idset.filter not_free_in_t id_to_exclude
-	    | _ -> anomaly "Should not have an anonymous function here"
+		  GProd(Loc.ghost,n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
+	    | _ -> anomaly (Pp.str "Should not have an anonymous function here")
 		(* We have renamed all the anonymous functions during alpha_renaming phase *)
 
 	end
     | GLetIn(_,n,t,b) ->
 	begin
 	  let not_free_in_t id = not (is_free_in id t) in
-	  let t' = Pretyping.Default.understand Evd.empty env t in
+	  let t',ctx = Pretyping.understand env Evd.empty t in
 	  let type_t' = Typing.type_of env Evd.empty t' in
 	  let new_env = Environ.push_rel (n,Some t',type_t') env in
 	  let new_b,id_to_exclude =
@@ -1145,13 +1113,13 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	      args (t::crossed_types)
 	      (depth + 1 ) b in
 	  match n with
-	    | Name id when Idset.mem id id_to_exclude && depth >= nb_args  ->
-		new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude)
-	    | _ -> GLetIn(dummy_loc,n,t,new_b),
-		Idset.filter not_free_in_t id_to_exclude
+	    | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args  ->
+		new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
+	    | _ -> GLetIn(Loc.ghost,n,t,new_b),
+		Id.Set.filter not_free_in_t id_to_exclude
 	end
     | GLetTuple(_,nal,(na,rto),t,b) ->
-	assert (rto=None);
+	assert (Option.is_empty rto);
 	begin
 	  let not_free_in_t id = not (is_free_in id t) in
 	  let new_t,id_to_exclude' =
@@ -1161,7 +1129,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	      args (crossed_types)
 	      depth t
 	  in
-	  let t' = Pretyping.Default.understand Evd.empty env new_t in
+	  let t',ctx = Pretyping.understand env Evd.empty new_t in
 	  let new_env = Environ.push_rel (na,None,t') env in
 	  let new_b,id_to_exclude =
 	    rebuild_cons new_env
@@ -1170,15 +1138,15 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	      (depth + 1) b
 	  in
 (* 	  match n with  *)
-(* 	    | Name id when Idset.mem id id_to_exclude ->  *)
-(* 		new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude) *)
+(* 	    | Name id when Id.Set.mem id id_to_exclude ->  *)
+(* 		new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) *)
 (* 	    | _ -> *)
-	  GLetTuple(dummy_loc,nal,(na,None),t,new_b),
-		Idset.filter not_free_in_t (Idset.union id_to_exclude id_to_exclude')
+	  GLetTuple(Loc.ghost,nal,(na,None),t,new_b),
+		Id.Set.filter not_free_in_t (Id.Set.union id_to_exclude id_to_exclude')
 
 	end
 
-    | _ -> mkGApp(mkGVar  relname,args@[rt]),Idset.empty
+    | _ -> mkGApp(mkGVar  relname,args@[rt]),Id.Set.empty
 
 
 (* debuging wrapper *)
@@ -1201,7 +1169,7 @@ let rebuild_cons env nb_args relname args crossed_types rt =
 *)
 let rec compute_cst_params relnames params = function
   | GRef _ | GVar _ | GEvar _ | GPatVar _ -> params
-  | GApp(_,GVar(_,relname'),rtl) when Idset.mem relname' relnames ->
+  | GApp(_,GVar(_,relname'),rtl) when Id.Set.mem relname' relnames ->
       compute_cst_params_from_app [] (params,rtl)
   | GApp(_,f,args) ->
       List.fold_left (compute_cst_params relnames) params (f::args)
@@ -1219,11 +1187,11 @@ and compute_cst_params_from_app acc (params,rtl) =
   match params,rtl with
     | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *)
     | ((Name id,_,is_defined) as param)::params',(GVar(_,id'))::rtl'
-	when id_ord id id' == 0 && not is_defined ->
+	when Id.compare id id' == 0 && not is_defined ->
 	compute_cst_params_from_app (param::acc) (params',rtl')
     | _  -> List.rev acc
 
-let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * bool) list array) csts =
+let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool) list array) csts =
   let rels_params =
     Array.mapi
       (fun i args ->
@@ -1237,12 +1205,12 @@ let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * b
   let l = ref [] in
   let _ =
     try
-      list_iter_i
+      List.iteri
 	(fun i ((n,nt,is_defined) as param) ->
-	   if array_for_all
+	   if Array.for_all
 	     (fun l ->
 		let (n',nt',is_defined') = List.nth l i in
-		n = n' && Topconstr.eq_glob_constr nt nt' && is_defined = is_defined')
+		Name.equal n n' && Notation_ops.eq_glob_constr nt nt' && (is_defined : bool) == is_defined')
 	     rels_params
 	   then
 	     l := param::!l
@@ -1255,22 +1223,23 @@ let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * b
 
 let rec rebuild_return_type rt =
   match rt with
-    | Topconstr.CProdN(loc,n,t') ->
-	Topconstr.CProdN(loc,n,rebuild_return_type t')
-    | Topconstr.CArrow(loc,t,t') ->
-	Topconstr.CArrow(loc,t,rebuild_return_type t')
-    | Topconstr.CLetIn(loc,na,t,t') ->
-	Topconstr.CLetIn(loc,na,t,rebuild_return_type t')
-    | _ -> Topconstr.CArrow(dummy_loc,rt,Topconstr.CSort(dummy_loc,GType None))
+    | Constrexpr.CProdN(loc,n,t') ->
+	Constrexpr.CProdN(loc,n,rebuild_return_type t')
+    | Constrexpr.CLetIn(loc,na,t,t') ->
+	Constrexpr.CLetIn(loc,na,t,rebuild_return_type t')
+    | _ -> Constrexpr.CProdN(Loc.ghost,[[Loc.ghost,Anonymous],
+				       Constrexpr.Default Decl_kinds.Explicit,rt],
+			    Constrexpr.CSort(Loc.ghost,GType []))
 
 
 let do_build_inductive
-    funnames (funsargs: (Names.name * glob_constr * bool) list list)
-    returned_types
-    (rtl:glob_constr list) =
+      mp_dp
+      funnames (funsargs: (Name.t * glob_constr * bool) list list)
+      returned_types
+      (rtl:glob_constr list) =
   let _time1 = System.get_time () in
-(*   Pp.msgnl (prlist_with_sep fnl Printer.pr_glob_constr rtl); *)
-  let funnames_as_set = List.fold_right Idset.add funnames Idset.empty in
+  (*   Pp.msgnl (prlist_with_sep fnl Printer.pr_glob_constr rtl); *)
+  let funnames_as_set = List.fold_right Id.Set.add funnames Id.Set.empty in
   let funnames = Array.of_list funnames in
   let funsargs = Array.of_list funsargs in
   let returned_types = Array.of_list returned_types in
@@ -1281,12 +1250,22 @@ let do_build_inductive
     Ensures by: obvious
     i*)
   let relnames = Array.map mk_rel_id funnames in
-  let relnames_as_set = Array.fold_right Idset.add relnames Idset.empty in
+  let relnames_as_set = Array.fold_right Id.Set.add relnames Id.Set.empty in
   (* Construction of the pseudo constructors *)
   let env =
     Array.fold_right
       (fun id env ->
-	 Environ.push_named (id,None,Typing.type_of env Evd.empty (Constrintern.global_reference id))  env
+       let c =
+	 match mp_dp with
+	 | None -> (Constrintern.global_reference id)
+	 | Some(mp,dp) -> mkConst (make_con mp dp (Label.of_id id))
+       in
+       Environ.push_named (id,None,
+			   try
+			     Typing.type_of env Evd.empty c
+			   with Not_found ->
+			     raise (UserError("do_build_inductive", str "Cannot handle partial fixpoint"))
+			  )  env
       )
       funnames
       (Global.env ())
@@ -1294,19 +1273,19 @@ let do_build_inductive
   let resa = Array.map (build_entry_lc env  funnames_as_set []) rta in
   let env_with_graphs =
     let rel_arity i funargs =  (* Reduilding arities (with parameters) *)
-      let rel_first_args :(Names.name * Glob_term.glob_constr * bool ) list  =
+      let rel_first_args :(Name.t * Glob_term.glob_constr * bool ) list  =
 	funargs
       in
       List.fold_right
 	(fun (n,t,is_defined) acc ->
 	   if is_defined
 	   then
-	     Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t,
+	     Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
 			      acc)
 	   else
-	     Topconstr.CProdN
-	       (dummy_loc,
-		[[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t],
+	     Constrexpr.CProdN
+	       (Loc.ghost,
+		[[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
 		acc
 	       )
 	)
@@ -1318,8 +1297,9 @@ let do_build_inductive
        Then save the graphs and reset Printing options to their primitive values
     *)
     let rel_arities = Array.mapi rel_arity funsargs in
-    Util.array_fold_left2 (fun env rel_name rel_ar ->
-			     Environ.push_named (rel_name,None, Constrintern.interp_constr Evd.empty env rel_ar) env) env relnames rel_arities
+    Util.Array.fold_left2 (fun env rel_name rel_ar ->
+			     Environ.push_named (rel_name,None, 
+						 fst (with_full_print (Constrintern.interp_constr env Evd.empty) rel_ar)) env) env relnames rel_arities
   in
   (* and of the real constructors*)
   let constr i res =
@@ -1344,9 +1324,9 @@ let do_build_inductive
     (*i The next call to mk_rel_id is valid since we are constructing the graph
       Ensures by: obvious
       i*)
-    id_of_string ((string_of_id (mk_rel_id funnames.(i)))^"_"^(string_of_int !next_constructor_id))
+    Id.of_string ((Id.to_string (mk_rel_id funnames.(i)))^"_"^(string_of_int !next_constructor_id))
   in
-  let rel_constructors i rt : (identifier*glob_constr) list =
+  let rel_constructors i rt : (Id.t*glob_constr) list =
     next_constructor_id := (-1);
     List.map (fun constr -> (mk_constructor_id i),constr) (constr i rt)
   in
@@ -1360,19 +1340,19 @@ let do_build_inductive
     rel_constructors
   in
   let rel_arity i funargs =  (* Reduilding arities (with parameters) *)
-    let rel_first_args :(Names.name * Glob_term.glob_constr * bool ) list  =
-      (snd (list_chop nrel_params funargs))
+    let rel_first_args :(Name.t * Glob_term.glob_constr * bool ) list  =
+      (snd (List.chop nrel_params funargs))
     in
     List.fold_right
       (fun (n,t,is_defined) acc ->
 	 if is_defined
 	 then
-	   Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t,
+	   Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
 			    acc)
 	 else
-	   Topconstr.CProdN
-	   (dummy_loc,
-	   [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t],
+	   Constrexpr.CProdN
+	   (Loc.ghost,
+	   [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
 	    acc
 	   )
       )
@@ -1384,31 +1364,40 @@ let do_build_inductive
      Then save the graphs and reset Printing options to their primitive values
   *)
   let rel_arities = Array.mapi rel_arity funsargs in
+  let rel_params_ids =
+    List.fold_left
+      (fun  acc (na,_,_) ->
+       match na with
+	 Anonymous -> acc
+       | Name id -> id::acc
+      )
+      []
+      rels_params
+  in
   let rel_params =
     List.map
       (fun (n,t,is_defined) ->
 	 if is_defined
 	 then
-	   Topconstr.LocalRawDef((dummy_loc,n), Constrextern.extern_glob_constr Idset.empty t)
+	   Constrexpr.LocalRawDef((Loc.ghost,n), Constrextern.extern_glob_constr Id.Set.empty t)
 	 else
-	 Topconstr.LocalRawAssum
-	   ([(dummy_loc,n)], Topconstr.default_binder_kind, Constrextern.extern_glob_constr Idset.empty t)
+	 Constrexpr.LocalRawAssum
+	   ([(Loc.ghost,n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t)
       )
       rels_params
   in
   let ext_rels_constructors =
     Array.map (List.map
       (fun (id,t) ->
-	 false,((dummy_loc,id),
-		Flags.with_option
-		  Flags.raw_print
-		  (Constrextern.extern_glob_type Idset.empty) ((* zeta_normalize *) t)
+	 false,((Loc.ghost,id),
+		with_full_print
+		  (Constrextern.extern_glob_type Id.Set.empty) ((* zeta_normalize *) (alpha_rt rel_params_ids t))
 	       )
       ))
       (rel_constructors)
   in
   let rel_ind i ext_rel_constructors =
-    ((dummy_loc,relnames.(i)),
+    ((Loc.ghost,relnames.(i)),
     rel_params,
     Some rel_arities.(i),
     ext_rel_constructors),[]
@@ -1437,7 +1426,7 @@ let do_build_inductive
 (*   in *)
   let _time2 = System.get_time () in
   try
-    with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds)) true
+    with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds false false)) Decl_kinds.Finite
   with
     | UserError(s,msg) as e ->
 	let _time3 = System.get_time () in
@@ -1448,7 +1437,7 @@ let do_build_inductive
 	in
 	let msg =
 	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds))
+	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds))
 	    ++ fnl () ++
 	    msg
 	in
@@ -1463,7 +1452,7 @@ let do_build_inductive
 	in
 	let msg =
 	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds))
+	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds))
 	    ++ fnl () ++
 	    Errors.print reraise
 	in
@@ -1472,9 +1461,9 @@ let do_build_inductive
 
 
 
-let build_inductive funnames funsargs returned_types rtl =
+let build_inductive mp_dp funnames funsargs returned_types rtl =
   try
-    do_build_inductive funnames funsargs returned_types rtl
+    do_build_inductive mp_dp funnames funsargs returned_types rtl
   with e when Errors.noncritical e -> raise (Building_graph e)