1 files changed, 112 insertions, 95 deletions

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 5e72b867..804548ce 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -1,7 +1,9 @@
 open Printer
 open CErrors
-open Util
 open Term
+open Sorts
+open Util
+open Constr
 open Vars
 open Namegen
 open Names
@@ -11,8 +13,8 @@ open Tactics
 open Context.Rel.Declaration
 open Indfun_common
 open Functional_principles_proofs
-open Misctypes
-open Sigma.Notations
+
+module RelDecl = Context.Rel.Declaration
 
 exception Toberemoved_with_rel of int*constr
 exception Toberemoved
@@ -21,25 +23,28 @@ let observe s =
   if do_observe ()
   then Feedback.msg_debug s
 
+let pop t = Vars.lift (-1) t
+
 (*
    Transform an inductive induction principle into
    a functional one
 *)
 let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
-  let princ_type_info = compute_elim_sig princ_type in
+  let princ_type = EConstr.of_constr princ_type in
+  let princ_type_info = compute_elim_sig Evd.empty princ_type (** FIXME *) in
   let env = Global.env () in
-  let env_with_params = Environ.push_rel_context princ_type_info.params env in
+  let env_with_params = EConstr.push_rel_context princ_type_info.params env in
   let tbl = Hashtbl.create 792 in
-  let rec change_predicates_names (avoid:Id.t list) (predicates:Context.Rel.t)  : Context.Rel.t =
+  let rec change_predicates_names (avoid:Id.t list) (predicates:EConstr.rel_context)  : EConstr.rel_context =
     match predicates with
     | [] -> []
     | decl :: predicates ->
        (match Context.Rel.Declaration.get_name decl with
 	| Name x ->
-	   let id = Namegen.next_ident_away x avoid in
+	   let id = Namegen.next_ident_away x (Id.Set.of_list avoid) in
 	   Hashtbl.add tbl id x;
-	   set_name (Name id) decl :: change_predicates_names (id::avoid) predicates
-	| Anonymous -> anomaly (Pp.str "Anonymous property binder "))
+	   RelDecl.set_name (Name id) decl :: change_predicates_names (id::avoid) predicates
+	| Anonymous -> anomaly (Pp.str "Anonymous property binder."))
   in
   let avoid = (Termops.ids_of_context env_with_params ) in
   let princ_type_info =
@@ -51,14 +56,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 (*   observe (str "princ_infos : " ++ pr_elim_scheme princ_type_info); *)
   let change_predicate_sort i decl =
     let new_sort = sorts.(i) in
-    let args,_ = decompose_prod (get_type decl) in
+    let args,_ = decompose_prod (EConstr.Unsafe.to_constr (RelDecl.get_type decl)) in
     let real_args =
       if princ_type_info.indarg_in_concl
       then List.tl args
       else args
     in
-    Context.Named.Declaration.LocalAssum (Nameops.out_name (Context.Rel.Declaration.get_name decl),
-                                          compose_prod real_args (mkSort new_sort))
+    Context.Named.Declaration.LocalAssum (Nameops.Name.get_id (Context.Rel.Declaration.get_name decl),
+                                          Term.compose_prod real_args (mkSort new_sort))
   in
   let new_predicates =
     List.map_i
@@ -70,18 +75,19 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   let rel_as_kn =
     fst (match princ_type_info.indref with
 	   | Some (Globnames.IndRef ind) -> ind
-	   | _ -> error "Not a valid predicate"
+	   | _ -> user_err Pp.(str "Not a valid predicate")
 	)
   in
   let ptes_vars = List.map Context.Named.Declaration.get_id new_predicates in
   let is_pte =
     let set = List.fold_right Id.Set.add ptes_vars Id.Set.empty in
     fun t ->
-      match kind_of_term t with
+      match Constr.kind t with
 	| Var id -> Id.Set.mem id set
 	| _ -> false
   in
   let pre_princ =
+    let open EConstr in
     it_mkProd_or_LetIn
       (it_mkProd_or_LetIn
 	 (Option.fold_right
@@ -93,28 +99,31 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
       )
       princ_type_info.branches
   in
+  let pre_princ = EConstr.Unsafe.to_constr pre_princ in
   let pre_princ = substl (List.map mkVar ptes_vars) pre_princ in
   let is_dom c =
-    match kind_of_term c with
+    match Constr.kind c with
       | Ind((u,_),_) -> MutInd.equal u rel_as_kn
       | Construct(((u,_),_),_) -> MutInd.equal u rel_as_kn
       | _ -> false
   in
   let get_fun_num c =
-    match kind_of_term c with
+    match Constr.kind c with
       | Ind((_,num),_) -> num
       | Construct(((_,num),_),_) -> num
       | _ -> assert false
   in
   let dummy_var = mkVar (Id.of_string "________") in
   let mk_replacement c i args =
-    let res = mkApp(rel_to_fun.(i), Array.map Termops.pop (array_get_start args)) in
-    observe (str "replacing " ++ pr_lconstr c ++ str " by "  ++ pr_lconstr res);
+    let res = mkApp(rel_to_fun.(i), Array.map pop (array_get_start args)) in
+    observe (str "replacing " ++
+             pr_lconstr_env env Evd.empty c ++ str " by "  ++
+             pr_lconstr_env env Evd.empty res);
     res
   in
   let rec compute_new_princ_type remove env pre_princ : types*(constr list) =
     let (new_princ_type,_) as res =
-      match kind_of_term pre_princ with
+      match Constr.kind pre_princ with
 	| Rel n ->
 	    begin
 	      try match Environ.lookup_rel n env with
@@ -143,13 +152,13 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 		([],[])
 	    in
 	    let new_f,binders_to_remove_from_f = compute_new_princ_type remove env f in
-	    applist(new_f, new_args),
-	    list_union_eq eq_constr binders_to_remove_from_f binders_to_remove
+	    applistc new_f new_args,
+	    list_union_eq Constr.equal binders_to_remove_from_f binders_to_remove
 	| LetIn(x,v,t,b) ->
 	    compute_new_princ_type_for_letin remove env x v t b
 	| _ -> pre_princ,[]
     in
-(*     let _ = match kind_of_term pre_princ with *)
+(*     let _ = match Constr.kind pre_princ with *)
 (* 	| Prod _ -> *)
 (* 	    observe(str "compute_new_princ_type for "++ *)
 (* 	      pr_lconstr_env env pre_princ ++ *)
@@ -165,26 +174,26 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	let new_x : Name.t = get_name (Termops.ids_of_context env) x in
 	let new_env = Environ.push_rel (LocalAssum (x,t)) env in
 	let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
-	 if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
-	 then (Termops.pop new_b), filter_map (eq_constr (mkRel 1)) Termops.pop binders_to_remove_from_b
+	 if List.exists (Constr.equal (mkRel 1)) binders_to_remove_from_b
+	 then (pop new_b), filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b
 	 else
 	   (
 	     bind_fun(new_x,new_t,new_b),
 	     list_union_eq
-	       eq_constr
+	       Constr.equal
 	       binders_to_remove_from_t
-	       (List.map Termops.pop binders_to_remove_from_b)
+	       (List.map pop binders_to_remove_from_b)
 	   )
 
        with
 	 | Toberemoved ->
-(* 	    observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+(* 	    observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *)
 	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b)  in
-	    new_b, List.map Termops.pop binders_to_remove_from_b
+	    new_b, List.map pop binders_to_remove_from_b
 	| Toberemoved_with_rel (n,c) ->
-(* 	    observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+(* 	    observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *)
 	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b)  in
-	    new_b, list_add_set_eq eq_constr (mkRel n) (List.map Termops.pop binders_to_remove_from_b)
+	    new_b, list_add_set_eq Constr.equal (mkRel n) (List.map pop binders_to_remove_from_b)
     end
   and compute_new_princ_type_for_letin remove env x v t b =
     begin
@@ -194,31 +203,31 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	let new_x : Name.t = get_name (Termops.ids_of_context env) x in
 	let new_env = Environ.push_rel (LocalDef (x,v,t)) env in
 	let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
-	if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
-	then (Termops.pop new_b),filter_map (eq_constr (mkRel 1)) Termops.pop binders_to_remove_from_b
+	if List.exists (Constr.equal (mkRel 1)) binders_to_remove_from_b
+	then (pop new_b),filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b
 	else
 	  (
 	    mkLetIn(new_x,new_v,new_t,new_b),
 	    list_union_eq
-	      eq_constr
-	      (list_union_eq eq_constr binders_to_remove_from_t binders_to_remove_from_v)
-	      (List.map Termops.pop binders_to_remove_from_b)
+	      Constr.equal
+	      (list_union_eq Constr.equal binders_to_remove_from_t binders_to_remove_from_v)
+	      (List.map pop binders_to_remove_from_b)
 	  )
 
       with
 	| Toberemoved ->
-(* 	    observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+(* 	    observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *)
 	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b)  in
-	    new_b, List.map Termops.pop binders_to_remove_from_b
+	    new_b, List.map pop binders_to_remove_from_b
 	| Toberemoved_with_rel (n,c) ->
-(* 	    observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+(* 	    observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *)
 	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b)  in
-	    new_b, list_add_set_eq eq_constr (mkRel n) (List.map Termops.pop binders_to_remove_from_b)
+	    new_b, list_add_set_eq Constr.equal (mkRel n) (List.map pop binders_to_remove_from_b)
     end
   and  compute_new_princ_type_with_acc remove env e (c_acc,to_remove_acc)  =
     let new_e,to_remove_from_e = compute_new_princ_type remove env e
     in
-    new_e::c_acc,list_union_eq eq_constr to_remove_from_e to_remove_acc
+    new_e::c_acc,list_union_eq Constr.equal to_remove_from_e to_remove_acc
   in
 (*   observe (str "Computing new principe from " ++ pr_lconstr_env  env_with_params_and_predicates pre_princ); *)
   let pre_res,_ =
@@ -235,20 +244,21 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
                                  | Context.Named.Declaration.LocalDef (id,t,b) -> LocalDef (Name (Hashtbl.find tbl id), t, b))
           	      new_predicates)
     )
-    princ_type_info.params
+    (List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) princ_type_info.params)
 
 
 
 let change_property_sort evd toSort princ princName =
   let open Context.Rel.Declaration in
-  let princ_info = compute_elim_sig princ in
+  let princ = EConstr.of_constr princ in
+  let princ_info = compute_elim_sig evd princ in
   let change_sort_in_predicate decl =
     LocalAssum
     (get_name decl,
-     let args,ty = decompose_prod (get_type decl) in
+     let args,ty = decompose_prod (EConstr.Unsafe.to_constr (get_type decl)) in
      let s = destSort ty in
        Global.add_constraints (Univ.enforce_leq (univ_of_sort toSort) (univ_of_sort s) Univ.Constraint.empty);
-       compose_prod args (mkSort toSort)
+       Term.compose_prod args (mkSort toSort)
     )
   in
   let evd,princName_as_constr =
@@ -264,11 +274,11 @@ let change_property_sort evd toSort princ princName =
     (it_mkLambda_or_LetIn init
        (List.map change_sort_in_predicate princ_info.predicates)
     )
-    princ_info.params
+    (List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) princ_info.params)
 
 let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_princ_type sorts funs i proof_tac hook =
   (* First we get the type of the old graph principle *)
-  let mutr_nparams = (compute_elim_sig old_princ_type).nparams in
+  let mutr_nparams = (compute_elim_sig !evd (EConstr.of_constr old_princ_type)).nparams in
   (*   let time1 = System.get_time ()  in *)
   let new_principle_type =
     compute_new_princ_type_from_rel
@@ -279,20 +289,21 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   (*    let time2 = System.get_time ()  in *)
   (*    Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *)
   let new_princ_name =
-    next_ident_away_in_goal (Id.of_string "___________princ_________") []
+    next_ident_away_in_goal (Id.of_string "___________princ_________") Id.Set.empty
   in
-  let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd new_principle_type in
+  let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr new_principle_type) in
   let hook = Lemmas.mk_hook (hook new_principle_type) in
   begin
     Lemmas.start_proof
       new_princ_name
       (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem))
       !evd
-      new_principle_type
+      (EConstr.of_constr new_principle_type)
       hook
   ;
     (*       let _tim1 = System.get_time ()  in *)
-      ignore (Pfedit.by  (Proofview.V82.tactic (proof_tac (Array.map mkConstU funs) mutr_nparams)));
+      let map (c, u) = EConstr.mkConstU (c, EConstr.EInstance.make u) in
+      ignore (Pfedit.by  (Proofview.V82.tactic (proof_tac (Array.map map funs) mutr_nparams)));
     (*       let _tim2 =  System.get_time ()  in *)
     (* 	begin *)
     (* 	  let dur1 = System.time_difference tim1 tim2 in *)
@@ -321,8 +332,8 @@ let generate_functional_principle (evd: Evd.evar_map ref)
     match new_princ_name with
       | Some (id) -> id,id
       | None ->
-	  let id_of_f = Label.to_id (con_label (fst f)) in
-	  id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort)
+	  let id_of_f = Label.to_id (Constant.label (fst f)) in
+	  id_of_f,Indrec.make_elimination_ident id_of_f (Sorts.family type_sort)
   in
   let names = ref [new_princ_name] in
   let hook =
@@ -331,13 +342,17 @@ let generate_functional_principle (evd: Evd.evar_map ref)
     then
       (*     let id_of_f = Label.to_id (con_label f) in *)
       let register_with_sort fam_sort =
-	let evd' = Evd.from_env (Global.env ()) in
-	let evd',s = Evd.fresh_sort_in_family env evd' fam_sort in
-	let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
-	let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
-	let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' value) in
-	(* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
-	let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(snd (Evd.universe_context evd')) value in
+        let evd' = Evd.from_env (Global.env ()) in
+        let evd',s = Evd.fresh_sort_in_family env evd' fam_sort in
+        let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
+        let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
+        let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in
+        (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
+        let univs =
+          let poly = Flags.is_universe_polymorphism () in
+          Evd.const_univ_entry ~poly evd'
+        in
+        let ce = Declare.definition_entry ~univs value in
 	ignore(
 	  Declare.declare_constant
 	    name
@@ -362,12 +377,12 @@ let generate_functional_principle (evd: Evd.evar_map ref)
     begin
       begin
 	try
-	  let id = Pfedit.get_current_proof_name () in
+	  let id = Proof_global.get_current_proof_name () in
 	  let s = Id.to_string id in
 	  let n = String.length "___________princ_________" in
 	  if String.length s >= n
 	  then if String.equal (String.sub s 0 n) "___________princ_________"
-	  then Pfedit.delete_current_proof ()
+	  then Proof_global.discard_current ()
 	  else ()
 	  else ()
 	with e when CErrors.noncritical e -> ()
@@ -380,17 +395,17 @@ let generate_functional_principle (evd: Evd.evar_map ref)
 exception Not_Rec
 
 let get_funs_constant mp dp =
-  let get_funs_constant const e : (Names.constant*int) array =
-    match kind_of_term ((strip_lam e)) with
+  let get_funs_constant const e : (Names.Constant.t*int) array =
+    match Constr.kind ((strip_lam e)) with
       | Fix((_,(na,_,_))) ->
 	  Array.mapi
 	    (fun i na ->
 	       match na with
 		 | Name id ->
-		     let const = make_con mp dp (Label.of_id id) in
+		     let const = Constant.make3 mp dp (Label.of_id id) in
 		     const,i
 		 | Anonymous ->
-		     anomaly (Pp.str "Anonymous fix")
+		     anomaly (Pp.str "Anonymous fix.")
 	    )
 	    na
       | _ -> [|const,0|]
@@ -398,15 +413,16 @@ let get_funs_constant mp dp =
   function const ->
     let find_constant_body const =
       match Global.body_of_constant const with
-	| Some body ->
+	| Some (body, _) ->
 	    let body = Tacred.cbv_norm_flags
 	      (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
 	      (Global.env ())
 	      (Evd.from_env (Global.env ()))
-	      body
+	      (EConstr.of_constr body)
 	    in
+	    let body = EConstr.Unsafe.to_constr body in
 	    body
-	| None -> error ( "Cannot define a principle over an axiom ")
+	| None -> user_err Pp.(str ( "Cannot define a principle over an axiom "))
     in
     let f = find_constant_body const in
     let l_const = get_funs_constant const f in
@@ -421,8 +437,8 @@ let get_funs_constant mp dp =
       let first_params = List.hd l_params  in
       List.iter
 	(fun params ->
-	   if not (List.equal (fun (n1, c1) (n2, c2) -> Name.equal n1 n2 && eq_constr c1 c2) first_params params)
-	   then error "Not a mutal recursive block"
+	   if not (List.equal (fun (n1, c1) (n2, c2) -> Name.equal n1 n2 && Constr.equal c1 c2) first_params params)
+	   then user_err Pp.(str "Not a mutal recursive block")
 	)
 	l_params
     in
@@ -430,21 +446,21 @@ let get_funs_constant mp dp =
     let _check_bodies =
       try
 	let extract_info is_first body =
-	  match kind_of_term body with
+	  match Constr.kind body with
 	    | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca)
 	    | _ ->
 		if is_first && Int.equal (List.length l_bodies) 1
 		then raise Not_Rec
-		else error "Not a mutal recursive block"
+		else user_err Pp.(str "Not a mutal recursive block")
 	in
 	let first_infos = extract_info true (List.hd l_bodies) in
 	let check body  = (* Hope this is correct *)
 	  let eq_infos (ia1, na1, ta1, ca1) (ia2, na2, ta2, ca2) =
             Array.equal Int.equal ia1 ia2 && Array.equal Name.equal na1 na2 &&
-            Array.equal eq_constr ta1 ta2 && Array.equal eq_constr ca1 ca2
+            Array.equal Constr.equal ta1 ta2 && Array.equal Constr.equal ca1 ca2
 	  in
 	  if not (eq_infos first_infos (extract_info false body))
-	  then  error "Not a mutal recursive block"
+	  then  user_err Pp.(str "Not a mutal recursive block")
 	in
 	List.iter check l_bodies
       with Not_Rec -> ()
@@ -454,7 +470,7 @@ let get_funs_constant mp dp =
 exception No_graph_found
 exception Found_type of int
 
-let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_constants definition_entry list =
+let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_constants definition_entry list =
   let env = Global.env () in
   let funs = List.map fst fas in
   let first_fun = List.hd funs in
@@ -486,12 +502,12 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con
   in
   let _ = evd := sigma in 
   let l_schemes =
-    List.map (Typing.unsafe_type_of env sigma) schemes
+    List.map (EConstr.of_constr %> Typing.unsafe_type_of env sigma %> EConstr.Unsafe.to_constr) schemes
   in
   let i = ref (-1) in
   let sorts =
     List.rev_map (fun (_,x) ->
-		  Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd (Pretyping.interp_elimination_sort x)
+		  Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd x
 	     )
       fas
   in
@@ -514,12 +530,12 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con
        begin
 	 begin
 	   try
-	     let id = Pfedit.get_current_proof_name () in
+	     let id = Proof_global.get_current_proof_name () in
 	     let s = Id.to_string id in
 	     let n = String.length "___________princ_________" in
 	     if String.length s >= n
 	     then if String.equal (String.sub s 0 n) "___________princ_________"
-		  then Pfedit.delete_current_proof ()
+		  then Proof_global.discard_current ()
 		  else ()
 	     else ()
 	   with e when CErrors.noncritical e -> ()
@@ -555,7 +571,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con
       List.map (* we can now compute the other principles *)
 	(fun scheme_type ->
 	   incr i;
-	   observe (Printer.pr_lconstr scheme_type);
+           observe (Printer.pr_lconstr_env env sigma scheme_type);
 	   let type_concl = (strip_prod_assum scheme_type) in
 	   let applied_f = List.hd (List.rev (snd (decompose_app type_concl))) in
 	   let f = fst (decompose_app applied_f) in
@@ -565,10 +581,10 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con
 		let t =  (strip_prod_assum t) in
 		let applied_g = List.hd (List.rev (snd (decompose_app t))) in
 		let g = fst (decompose_app applied_g) in
-		if eq_constr f g
+		if Constr.equal f g
 		then raise (Found_type j);
-		observe (Printer.pr_lconstr f ++ str " <> " ++
-			   Printer.pr_lconstr g)
+                observe (Printer.pr_lconstr_env env sigma f ++ str " <> " ++
+                         Printer.pr_lconstr_env env sigma g)
 
 	     )
 	     ta;
@@ -609,19 +625,22 @@ let build_scheme fas =
 	      try
 		Smartlocate.global_with_alias f
 	      with Not_found ->
-                errorlabstrm "FunInd.build_scheme"
+                user_err ~hdr:"FunInd.build_scheme"
                   (str "Cannot find " ++ Libnames.pr_reference f)
 	    in
-	    let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in
+            let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in
             let _ = evd := evd' in 
-	    let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd f in 
-	    (destConst f,sort)
+	    let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr f) in 
+            if isConst f
+            then (destConst f,sort)
+            else user_err Pp.(pr_constr_env (Global.env ()) !evd f ++spc () ++ str "should be the named of a globally defined function")
 	 )
 	 fas
 		   ) in
   let bodies_types =
     make_scheme evd pconstants      
   in
+
   List.iter2
     (fun (princ_id,_,_) def_entry ->
        ignore
@@ -641,12 +660,12 @@ let build_case_scheme fa =
 (*   in  *)
   let funs =
     let (_,f,_) = fa in
-    try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f))
+    try fst (Global.constr_of_global_in_context (Global.env ()) (Smartlocate.global_with_alias f))
     with Not_found ->
-      errorlabstrm "FunInd.build_case_scheme"
+      user_err ~hdr:"FunInd.build_case_scheme"
         (str "Cannot find " ++ Libnames.pr_reference f) in
   let first_fun,u = destConst  funs in
-  let funs_mp,funs_dp,_ = Names.repr_con first_fun in
+  let funs_mp,funs_dp,_ = Constant.repr3 first_fun in
   let first_fun_kn = try fst (find_Function_infos  first_fun).graph_ind with Not_found -> raise No_graph_found in
   let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in
   let this_block_funs = Array.map (fun (c,_) -> (c,u)) this_block_funs_indexes in
@@ -659,15 +678,13 @@ let build_case_scheme fa =
 	 let ind = first_fun_kn,funs_indexes in
 	   (ind,Univ.Instance.empty)(*FIXME*),prop_sort
   in
-  let sigma = Sigma.Unsafe.of_evar_map sigma in
-  let Sigma (scheme, sigma, _) = 
+  let (sigma, scheme) = 
       Indrec.build_case_analysis_scheme_default env sigma ind sf
   in
-  let sigma = Sigma.to_evar_map sigma in
-  let scheme_type =  (Typing.unsafe_type_of env sigma ) scheme in
+  let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in
   let sorts =
     (fun (_,_,x) ->
-       Universes.new_sort_in_family (Pretyping.interp_elimination_sort x)
+       Universes.new_sort_in_family x
     )
       fa
   in