1 files changed, 155 insertions, 138 deletions

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 18817f504c..d12aa7f425 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -1,8 +1,9 @@
-open Context.Rel.Declaration
+open API
 open CErrors
 open Util
 open Names
 open Term
+open EConstr
 open Pp
 open Indfun_common
 open Libnames
@@ -11,39 +12,42 @@ open Glob_term
 open Declarations
 open Misctypes
 open Decl_kinds
-open Sigma.Notations
 
-let is_rec_info scheme_info =
+module RelDecl = Context.Rel.Declaration
+
+let is_rec_info sigma scheme_info =
   let test_branche min acc decl =
     acc || (
       let new_branche =
-	it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum (get_type decl))) in
-      let free_rels_in_br = Termops.free_rels new_branche in
+	it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum sigma (RelDecl.get_type decl))) in
+      let free_rels_in_br = Termops.free_rels sigma new_branche in
       let max = min + scheme_info.Tactics.npredicates in
       Int.Set.exists (fun i -> i >= min && i< max) free_rels_in_br
     )
   in
   List.fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches)
 
-let choose_dest_or_ind scheme_info =
-  Tactics.induction_destruct (is_rec_info scheme_info) false
+let choose_dest_or_ind scheme_info args =
+  Proofview.tclBIND Proofview.tclEVARMAP (fun sigma ->
+  Tactics.induction_destruct (is_rec_info sigma scheme_info) false args)
 
 let functional_induction with_clean c princl pat =
   let res =
-    let f,args = decompose_app c in
     fun g ->
+    let sigma = Tacmach.project g in
+    let f,args = decompose_app sigma c in
     let princ,bindings, princ_type,g' =
       match princl with
       | None -> (* No principle is given let's find the good one *)
 	 begin
-	   match kind_of_term f with
+	   match EConstr.kind sigma f with
 	   | Const (c',u) ->
 	      let princ_option =
 		let finfo = (* we first try to find out a graph on f *)
 		  try find_Function_infos c'
 		  with Not_found ->
-		    errorlabstrm "" (str "Cannot find induction information on "++
-				       Printer.pr_lconstr (mkConst c') )
+		    user_err  (str "Cannot find induction information on "++
+				       Printer.pr_leconstr (mkConst c') )
 		in
 		match Tacticals.elimination_sort_of_goal g with
 		| InProp -> finfo.prop_lemma
@@ -61,7 +65,7 @@ let functional_induction with_clean c princl pat =
 			  (or f_rec, f_rect) i*)
 		  let princ_name =
 		    Indrec.make_elimination_ident
-		      (Label.to_id (con_label c'))
+		      (Label.to_id (Constant.label c'))
 		      (Tacticals.elimination_sort_of_goal g)
 		  in
 		  try
@@ -70,16 +74,18 @@ let functional_induction with_clean c princl pat =
 		    (b,a)
 		    (* mkConst(const_of_id princ_name ),g (\* FIXME *\) *)
 		  with Not_found -> (* This one is neither defined ! *)
-		    errorlabstrm "" (str "Cannot find induction principle for "
-				     ++Printer.pr_lconstr (mkConst c') )
+		    user_err  (str "Cannot find induction principle for "
+				     ++Printer.pr_leconstr (mkConst c') )
 	      in
-	      (princ,NoBindings, Tacmach.pf_unsafe_type_of g' princ,g')
-	   | _ -> raise (UserError("",str "functional induction must be used with a function" ))
+	      let princ = EConstr.of_constr princ in
+	      (princ,NoBindings,Tacmach.pf_unsafe_type_of g' princ,g')
+	   | _ -> raise (UserError(None,str "functional induction must be used with a function" ))
 	 end
       | Some ((princ,binding)) ->
 	 princ,binding,Tacmach.pf_unsafe_type_of g princ,g
     in
-    let princ_infos = Tactics.compute_elim_sig princ_type in
+    let sigma = Tacmach.project g' in
+    let princ_infos = Tactics.compute_elim_sig (Tacmach.project g') princ_type in
     let args_as_induction_constr =
       let c_list =
 	if princ_infos.Tactics.farg_in_concl
@@ -87,13 +93,13 @@ let functional_induction with_clean c princl pat =
       in
       let encoded_pat_as_patlist =
         List.make (List.length args + List.length c_list - 1) None @ [pat] in
-      List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr ({ Tacexpr.delayed = fun env sigma -> Sigma ((c,NoBindings), sigma, Sigma.refl) })),(None,pat),None))
+      List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr (fun env sigma -> (sigma,(c,NoBindings)) )),(None,pat),None))
         (args@c_list) encoded_pat_as_patlist
     in
     let princ' = Some (princ,bindings) in
     let princ_vars =
       List.fold_right
-	(fun a acc -> try Id.Set.add (destVar a) acc with DestKO -> acc)
+	(fun a acc -> try Id.Set.add (destVar sigma a) acc with DestKO -> acc)
 	args
 	Id.Set.empty
     in
@@ -128,15 +134,15 @@ let functional_induction with_clean c princl pat =
 
 let rec abstract_glob_constr c = function
   | [] -> c
-  | Constrexpr.LocalRawDef (x,b)::bl -> Constrexpr_ops.mkLetInC(x,b,abstract_glob_constr c bl)
-  | Constrexpr.LocalRawAssum (idl,k,t)::bl ->
+  | Constrexpr.CLocalDef (x,b,t)::bl -> Constrexpr_ops.mkLetInC(x,b,t,abstract_glob_constr c bl)
+  | Constrexpr.CLocalAssum (idl,k,t)::bl ->
       List.fold_right (fun x b -> Constrexpr_ops.mkLambdaC([x],k,t,b)) idl
         (abstract_glob_constr c bl)
-  | Constrexpr.LocalPattern _::bl -> assert false
+  | Constrexpr.CLocalPattern _::bl -> assert false
 
 let interp_casted_constr_with_implicits env sigma impls c  =
   Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls
-    ~allow_patvar:false c
+    c
 
 (*
    Construct a fixpoint as a Glob_term
@@ -150,7 +156,7 @@ let build_newrecursive
   let (rec_sign,rec_impls) =
     List.fold_left
       (fun (env,impls) (((_,recname),_),bl,arityc,_) ->
-        let arityc = Constrexpr_ops.prod_constr_expr arityc bl in
+        let arityc = Constrexpr_ops.mkCProdN bl arityc in
         let arity,ctx = Constrintern.interp_type env0 sigma arityc in
 	let evdref = ref (Evd.from_env env0) in
 	let _, (_, impls') = Constrintern.interp_context_evars env evdref bl in
@@ -175,37 +181,41 @@ let build_newrecursive l =
        match body_opt with 
 	 | Some body -> 
 	     (fixna,bll,ar,body)
-	 | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given")
+	 | None -> user_err ~hdr:"Function" (str "Body of Function must be given")
     ) l
   in
   build_newrecursive l'
 
+let error msg = user_err Pp.(str msg)
+
 (* Checks whether or not the mutual bloc is recursive *)
 let is_rec names =
   let names = List.fold_right Id.Set.add names Id.Set.empty in
   let check_id id names =  Id.Set.mem id names in
-  let rec lookup names = function
-    | GVar(_,id) -> check_id id names
+  let rec lookup names gt = match gt.CAst.v with
+    | GVar(id) -> check_id id names
     | GRef _ | GEvar _ | GPatVar _ | GSort _ |  GHole _ -> false
-    | GCast(_,b,_) -> lookup names b
+    | GCast(b,_) -> lookup names b
     | GRec _ -> error "GRec not handled"
-    | GIf(_,b,_,lhs,rhs) ->
+    | GIf(b,_,lhs,rhs) ->
 	(lookup names b) || (lookup names lhs) || (lookup names rhs)
-    | GLetIn(_,na,t,b) | GLambda(_,na,_,t,b) | GProd(_,na,_,t,b)  ->
-	lookup names t || lookup (Nameops.name_fold Id.Set.remove na names) b
-    | GLetTuple(_,nal,_,t,b) -> lookup names t ||
+    | GProd(na,_,t,b) | GLambda(na,_,t,b) ->
+	lookup names t || lookup (Nameops.Name.fold_right Id.Set.remove na names) b
+    | GLetIn(na,b,t,c) ->
+	lookup names b || Option.cata (lookup names) true t || lookup (Nameops.Name.fold_right Id.Set.remove na names) c
+    | GLetTuple(nal,_,t,b) -> lookup names t ||
 	lookup
 	  (List.fold_left
-	     (fun acc na -> Nameops.name_fold Id.Set.remove na acc)
+	     (fun acc na -> Nameops.Name.fold_right Id.Set.remove na acc)
 	     names
 	     nal
 	  )
 	  b
-    | GApp(_,f,args) -> List.exists (lookup names) (f::args)
-    | GCases(_,_,_,el,brl) ->
+    | GApp(f,args) -> List.exists (lookup names) (f::args)
+    | GCases(_,_,el,brl) ->
 	List.exists (fun (e,_) -> lookup names e) el ||
 	  List.exists (lookup_br names) brl
-  and lookup_br names (_,idl,_,rt) =
+  and lookup_br names (_,(idl,_,rt)) =
     let new_names = List.fold_right Id.Set.remove idl names in
     lookup new_names rt
   in
@@ -214,9 +224,9 @@ let is_rec names =
 let rec local_binders_length = function
   (* Assume that no `{ ... } contexts occur *)
   | [] -> 0
-  | Constrexpr.LocalRawDef _::bl -> 1 + local_binders_length bl
-  | Constrexpr.LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl
-  | Constrexpr.LocalPattern _::bl -> assert false
+  | Constrexpr.CLocalDef _::bl -> 1 + local_binders_length bl
+  | Constrexpr.CLocalAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl
+  | Constrexpr.CLocalPattern _::bl -> assert false
 
 let prepare_body ((name,_,args,types,_),_) rt =
   let n = local_binders_length args in
@@ -242,7 +252,9 @@ let derive_inversion fix_names =
 	 let evd,c =
 	   Evd.fresh_global
 	     (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident id)) in 
-	 evd, destConst c::l
+        let c = EConstr.of_constr c in
+        let (cst, u) = destConst evd c in
+	 evd, (cst, EInstance.kind evd u) :: l
 	)
 	fix_names
 	(evd',[])
@@ -262,7 +274,8 @@ let derive_inversion fix_names =
 	       (Global.env ()) evd
 	       (Constrintern.locate_reference (Libnames.qualid_of_ident (mk_rel_id id)))
 	   in 
-	   evd,(fst (destInd id))::l
+	   let id = EConstr.of_constr id in
+	   evd,(fst (destInd evd id))::l
 	  )
 	  fix_names
 	  (evd',[])
@@ -321,7 +334,7 @@ let error_error names e =
   in
   match e with
     | Building_graph e ->
-	errorlabstrm ""
+	user_err 
 	  (str "Cannot define graph(s) for " ++
 	     h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
 	     e_explain e)
@@ -329,8 +342,8 @@ let error_error names e =
 
 let generate_principle (evd:Evd.evar_map ref) pconstants on_error
     is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs  interactive_proof
-    (continue_proof : int -> Names.constant array -> Term.constr array -> int ->
-      Tacmach.tactic) : unit =
+    (continue_proof : int -> Names.Constant.t array -> EConstr.constr array -> int ->
+      Proof_type.tactic) : unit =
   let names = List.map (function (((_, name),_),_,_,_,_),_ -> name) fix_rec_l in
   let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in
   let funs_args = List.map fst fun_bodies in
@@ -344,7 +357,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
 	(*i The next call to mk_rel_id is valid since we have just construct the graph
 	   Ensures by : do_built
 	i*)
-	let f_R_mut = Ident (Loc.ghost,mk_rel_id (List.nth names 0)) in
+	let f_R_mut = Ident (Loc.tag @@ mk_rel_id (List.nth names 0)) in
 	let ind_kn =
 	  fst (locate_with_msg
 		 (pr_reference f_R_mut++str ": Not an inductive type!")
@@ -367,7 +380,8 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
 	     let evd = ref (Evd.from_env env) in
 	     let evd',uprinc = Evd.fresh_global env !evd princ in
              let _ = evd := evd' in 
-	     let princ_type = Typing.e_type_of ~refresh:true env evd uprinc in
+	     let princ_type = Typing.e_type_of ~refresh:true env evd (EConstr.of_constr uprinc) in
+	     let princ_type = EConstr.Unsafe.to_constr princ_type in
     	     Functional_principles_types.generate_functional_principle
 	       evd
 		 interactive_proof
@@ -391,7 +405,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
 let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
   match fixpoint_exprl with
     | [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec ->
-      let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in 
+      let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in 
       Command.do_definition
 	fname
 	(Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl
@@ -402,7 +416,10 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
 	    let evd,c =
 	      Evd.fresh_global
 		(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
-	    evd,((destConst c)::l)
+            let c = EConstr.of_constr c in
+            let (cst, u) = destConst evd c in
+            let u = EInstance.kind evd u in
+            evd,((cst, u) :: l)
 	   )
 	   (Evd.from_env (Global.env ()),[])
 	   fixpoint_exprl
@@ -416,7 +433,10 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
 	    let evd,c =
 	      Evd.fresh_global
 		(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
-	    evd,((destConst c)::l)
+            let c = EConstr.of_constr c in
+            let (cst, u) = destConst evd c in
+            let u = EInstance.kind evd u in
+            evd,((cst, u) :: l)
 	   )
 	   (Evd.from_env (Global.env ()),[])
 	   fixpoint_exprl
@@ -426,7 +446,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
 
 let generate_correction_proof_wf f_ref tcc_lemma_ref
     is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
-    (_: int) (_:Names.constant array) (_:Term.constr array) (_:int) : Tacmach.tactic =
+    (_: int) (_:Names.Constant.t array) (_:EConstr.constr array) (_:int) : Proof_type.tactic =
   Functional_principles_proofs.prove_principle_for_gen
     (f_ref,functional_ref,eq_ref)
     tcc_lemma_ref is_mes  rec_arg_num rec_arg_type relation
@@ -435,7 +455,7 @@ let generate_correction_proof_wf f_ref tcc_lemma_ref
 let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body
     pre_hook
     =
-  let type_of_f = Constrexpr_ops.prod_constr_expr ret_type args in
+  let type_of_f = Constrexpr_ops.mkCProdN args ret_type in
   let rec_arg_num =
     let names =
       List.map
@@ -451,9 +471,8 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
   in
   let unbounded_eq =
     let f_app_args =
-      Constrexpr.CAppExpl
-	(Loc.ghost,
-	 (None,(Ident (Loc.ghost,fname)),None) ,
+      CAst.make @@ Constrexpr.CAppExpl(
+	 (None,(Ident (Loc.tag fname)),None) ,
 	 (List.map
 	    (function
 	       | _,Anonymous -> assert false
@@ -463,10 +482,10 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
 	 )
 	)
     in
-    Constrexpr.CApp (Loc.ghost,(None,Constrexpr_ops.mkRefC (Qualid (Loc.ghost,(qualid_of_string "Logic.eq")))),
+    CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (Qualid (Loc.tag (qualid_of_string "Logic.eq")))),
 		    [(f_app_args,None);(body,None)])
   in
-  let eq = Constrexpr_ops.prod_constr_expr unbounded_eq args in
+  let eq = Constrexpr_ops.mkCProdN args unbounded_eq in
   let hook ((f_ref,_) as fconst) tcc_lemma_ref (functional_ref,_) (eq_ref,_) rec_arg_num rec_arg_type
       nb_args relation =
     try
@@ -495,7 +514,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
       | None ->
 	  begin
 	    match args with
-	      | [Constrexpr.LocalRawAssum ([(_,Name x)],k,t)] -> t,x
+	      | [Constrexpr.CLocalAssum ([(_,Name x)],k,t)] -> t,x
 	      | _ -> error "Recursive argument must be specified"
 	  end
       | Some wf_args ->
@@ -503,7 +522,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
 	    match
 	      List.find
 		(function
-		   | Constrexpr.LocalRawAssum(l,k,t) ->
+		   | Constrexpr.CLocalAssum(l,k,t) ->
 		       List.exists
 			 (function (_,Name id) -> Id.equal id wf_args | _ -> false)
 			 l
@@ -511,7 +530,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
 		)
 		args
 	    with
-	      | Constrexpr.LocalRawAssum(_,k,t)  ->	    t,wf_args
+	      | Constrexpr.CLocalAssum(_,k,t)  ->	    t,wf_args
 	      | _ -> assert false
 	  with Not_found -> assert false
   in
@@ -520,13 +539,13 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
       | None ->
 	  let ltof =
 	    let make_dir l = DirPath.make (List.rev_map Id.of_string l) in
-	    Libnames.Qualid (Loc.ghost,Libnames.qualid_of_path
+	    Libnames.Qualid (Loc.tag @@ Libnames.qualid_of_path
 			       (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof")))
 	  in
 	  let fun_from_mes =
 	    let applied_mes =
 	      Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC wf_arg])    in
-	    Constrexpr_ops.mkLambdaC ([(Loc.ghost,Name wf_arg)],Constrexpr_ops.default_binder_kind,wf_arg_type,applied_mes)
+	    Constrexpr_ops.mkLambdaC ([(Loc.tag @@ Name wf_arg)],Constrexpr_ops.default_binder_kind,wf_arg_type,applied_mes)
 	  in
 	  let wf_rel_from_mes =
 	    Constrexpr_ops.mkAppC(Constrexpr_ops.mkRefC  ltof,[wf_arg_type;fun_from_mes])
@@ -537,7 +556,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
 	    let a = Names.Id.of_string "___a" in 
 	    let b = Names.Id.of_string "___b" in 
 	    Constrexpr_ops.mkLambdaC(
-	      [Loc.ghost,Name a;Loc.ghost,Name b],
+	      [Loc.tag @@ Name a;Loc.tag @@ Name b],
 	      Constrexpr.Default Explicit,
 	      wf_arg_type,
 	      Constrexpr_ops.mkAppC(wf_rel_expr,
@@ -569,35 +588,35 @@ let make_assoc assoc l1 l2 =
 let rec rebuild_bl (aux,assoc) bl typ = 
 	match bl,typ with 
 	  | [], _ -> (List.rev aux,replace_vars_constr_expr assoc typ,assoc)
-	  | (Constrexpr.LocalRawAssum(nal,bk,_))::bl',typ ->
+	  | (Constrexpr.CLocalAssum(nal,bk,_))::bl',typ ->
 	     rebuild_nal (aux,assoc) bk bl' nal (List.length nal) typ
-	  | (Constrexpr.LocalRawDef(na,_))::bl',Constrexpr.CLetIn(_,_,nat,typ') ->
-	    rebuild_bl ((Constrexpr.LocalRawDef(na,replace_vars_constr_expr assoc nat)::aux),assoc)
+	  | (Constrexpr.CLocalDef(na,_,_))::bl',{ CAst.v = Constrexpr.CLetIn(_,nat,ty,typ') } ->
+	    rebuild_bl ((Constrexpr.CLocalDef(na,replace_vars_constr_expr assoc nat,Option.map (replace_vars_constr_expr assoc) ty (* ??? *))::aux),assoc)
 	      bl' typ'
 	  | _ -> assert false
       and rebuild_nal (aux,assoc) bk bl' nal lnal typ = 
-	match nal,typ with 
+	match nal, typ.CAst.v with 
 	  | [], _ -> rebuild_bl (aux,assoc) bl' typ
-	  | _,CProdN(_,[],typ) -> rebuild_nal (aux,assoc) bk bl' nal lnal typ
-	  | _,CProdN(_,(nal',bk',nal't)::rest,typ') -> 
+	  | _,CProdN([],typ) -> rebuild_nal (aux,assoc) bk bl' nal lnal typ
+	  | _,CProdN((nal',bk',nal't)::rest,typ') -> 
 	    let lnal' = List.length nal' in 
 	    if lnal' >= lnal 
 	    then 
 	      let old_nal',new_nal' = List.chop lnal nal' in
 	      let nassoc = make_assoc assoc old_nal' nal in
-	      let assum = LocalRawAssum(nal,bk,replace_vars_constr_expr assoc nal't) in
+	      let assum = CLocalAssum(nal,bk,replace_vars_constr_expr assoc nal't) in
 	      rebuild_bl ((assum :: aux), nassoc) bl' 
 		(if List.is_empty new_nal' && List.is_empty rest
 		 then typ'
-		 else if List.is_empty new_nal'
-		 then CProdN(Loc.ghost,rest,typ')
-		 else CProdN(Loc.ghost,((new_nal',bk',nal't)::rest),typ'))
+		 else CAst.make @@ if List.is_empty new_nal'
+		 then CProdN(rest,typ')
+		 else CProdN(((new_nal',bk',nal't)::rest),typ'))
 	    else 
 	      let captured_nal,non_captured_nal = List.chop lnal' nal in
 	      let nassoc = make_assoc assoc nal' captured_nal in
-	      let assum = LocalRawAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't) in
+	      let assum = CLocalAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't) in
 	      rebuild_nal ((assum :: aux), nassoc)
-		bk bl' non_captured_nal (lnal - lnal') (CProdN(Loc.ghost,rest,typ'))
+		bk bl' non_captured_nal (lnal - lnal') (CAst.make @@ CProdN(rest,typ'))
 	  | _ -> assert false
 
 let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ
@@ -630,7 +649,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
 	      | _ -> assert false
 	  in 
 	  let fixpoint_exprl = [fixpoint_expr] in 
-	  let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in 
+	  let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in 
 	  let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
 	  let using_lemmas = [] in 
 	  let pre_hook pconstants =
@@ -656,7 +675,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
 	  let fixpoint_exprl = [fixpoint_expr] in 
 	  let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
 	  let using_lemmas = [] in
-	  let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in 
+	  let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in 
 	  let pre_hook pconstants =
 	    generate_principle
 	      (ref (Evd.from_env (Global.env ())))
@@ -708,67 +727,65 @@ let do_generate_principle pconstants on_error register_built interactive_proof
   in
   ()
 
-let rec add_args id new_args b =
-  match b with
-  | CRef (r,_) ->
-      begin      match r with
+let rec add_args id new_args = CAst.map (function
+  | CRef (r,_) as b ->
+      begin match r with
 	| Libnames.Ident(loc,fname) when Id.equal fname id ->
-	    CAppExpl(Loc.ghost,(None,r,None),new_args)
+	    CAppExpl((None,r,None),new_args)
 	| _ -> b
       end
-  | CFix  _  | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo")
-  | CProdN(loc,nal,b1) ->
-      CProdN(loc,
-	     List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal,
+  | CFix  _  | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo.")
+  | CProdN(nal,b1) ->
+        CProdN(List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal,
 	     add_args id new_args  b1)
-  | CLambdaN(loc,nal,b1) ->
-      CLambdaN(loc,
-	       List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args  b2)) nal,
+  | CLambdaN(nal,b1) ->
+      CLambdaN(List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args  b2)) nal,
 	       add_args id new_args  b1)
-  | CLetIn(loc,na,b1,b2) ->
-      CLetIn(loc,na,add_args id new_args b1,add_args id new_args b2)
-  | CAppExpl(loc,(pf,r,us),exprl) ->
+  | CLetIn(na,b1,t,b2) ->
+      CLetIn(na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2)
+  | CAppExpl((pf,r,us),exprl) ->
       begin
 	match r with
 	| Libnames.Ident(loc,fname) when Id.equal fname id ->
-	    CAppExpl(loc,(pf,r,us),new_args@(List.map (add_args id new_args) exprl))
-	| _ -> CAppExpl(loc,(pf,r,us),List.map (add_args id new_args) exprl)
+	    CAppExpl((pf,r,us),new_args@(List.map (add_args id new_args) exprl))
+	| _ -> CAppExpl((pf,r,us),List.map (add_args id new_args) exprl)
       end
-  | CApp(loc,(pf,b),bl) ->
-      CApp(loc,(pf,add_args id new_args b),
+  | CApp((pf,b),bl) ->
+      CApp((pf,add_args id new_args b),
 	   List.map (fun (e,o) -> add_args id new_args e,o) bl)
-  | CCases(loc,sty,b_option,cel,cal) ->
-      CCases(loc,sty,Option.map (add_args id new_args) b_option,
+  | CCases(sty,b_option,cel,cal) ->
+      CCases(sty,Option.map (add_args id new_args) b_option,
 	     List.map (fun (b,na,b_option) ->
 			 add_args id new_args b,
 			 na, b_option) cel,
-	     List.map (fun (loc,cpl,e) -> (loc,cpl,add_args id new_args e)) cal
+	     List.map (fun (loc,(cpl,e)) -> Loc.tag ?loc @@ (cpl,add_args id new_args e)) cal
 	    )
-  | CLetTuple(loc,nal,(na,b_option),b1,b2) ->
-      CLetTuple(loc,nal,(na,Option.map (add_args id new_args) b_option),
+  | CLetTuple(nal,(na,b_option),b1,b2) ->
+      CLetTuple(nal,(na,Option.map (add_args id new_args) b_option),
 		add_args id new_args b1,
 		add_args id new_args b2
 	       )
 
-  | CIf(loc,b1,(na,b_option),b2,b3) ->
-      CIf(loc,add_args id new_args b1,
+  | CIf(b1,(na,b_option),b2,b3) ->
+      CIf(add_args id new_args b1,
 	  (na,Option.map (add_args id new_args) b_option),
 	  add_args id new_args b2,
 	  add_args id new_args b3
 	 )
-  | CHole _ -> b
-  | CPatVar _ -> b
-  | CEvar _ -> b
-  | CSort _ -> b
-  | CCast(loc,b1,b2)  ->
-      CCast(loc,add_args id new_args b1,
+  | CHole _
+  | CPatVar _
+  | CEvar _
+  | CPrim _
+  | CSort _ as b -> b
+  | CCast(b1,b2)  ->
+      CCast(add_args id new_args b1,
 	    Miscops.map_cast_type (add_args id new_args) b2)
-  | CRecord (loc, pars) ->
-      CRecord (loc, List.map (fun (e,o) -> e, add_args id new_args o) pars)
-  | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation")
-  | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization")
-  | CPrim _ -> b
-  | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters")
+  | CRecord pars ->
+      CRecord (List.map (fun (e,o) -> e, add_args id new_args o) pars)
+  | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.")
+  | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization.")
+  | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters.")
+  )
 exception Stop of  Constrexpr.constr_expr
 
 
@@ -779,8 +796,8 @@ let rec chop_n_arrow n t =
   if n <= 0
   then t (* If we have already removed all the arrows then return the type *)
   else (* If not we check the form of [t] *)
-    match t with
-      | Constrexpr.CProdN(_,nal_ta',t') -> (* If we have a forall, to result are possible :
+    match t.CAst.v with
+      | Constrexpr.CProdN(nal_ta',t') -> (* If we have a forall, to result are possible :
 					     either we need to discard more than the number of arrows contained
 					     in this product declaration then we just recall [chop_n_arrow] on
 					     the remaining number of arrow to chop and [t'] we discard it and
@@ -798,8 +815,8 @@ let rec chop_n_arrow n t =
 		    then
 		      aux (n - nal_l) nal_ta'
 		    else
-		      let new_t' =
-			Constrexpr.CProdN(Loc.ghost,
+		      let new_t' = CAst.make @@
+			Constrexpr.CProdN(
 					((snd (List.chop n nal)),k,t'')::nal_ta',t')
 		      in
 		      raise (Stop new_t')
@@ -809,13 +826,13 @@ let rec chop_n_arrow n t =
 	      chop_n_arrow new_n t'
 	    with Stop t -> t
 	  end
-      | _ -> anomaly (Pp.str "Not enough products")
+      | _ -> anomaly (Pp.str "Not enough products.")
 
 
-let rec get_args b t : Constrexpr.local_binder list *
+let rec get_args b t : Constrexpr.local_binder_expr list *
     Constrexpr.constr_expr * Constrexpr.constr_expr =
-  match b with
-    | Constrexpr.CLambdaN (loc, (nal_ta), b') ->
+  match b.CAst.v with
+    | Constrexpr.CLambdaN ((nal_ta), b') ->
 	begin
 	  let n =
 	    (List.fold_left (fun n (nal,_,_) ->
@@ -823,7 +840,7 @@ let rec get_args b t : Constrexpr.local_binder list *
 	  in
 	  let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in
 	  (List.map (fun (nal,k,ta) ->
-		       (Constrexpr.LocalRawAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t''
+		       (Constrexpr.CLocalAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t''
 	end
     | _ -> [],b,t
 
@@ -834,12 +851,12 @@ let make_graph (f_ref:global_reference) =
       | ConstRef c ->
 	  begin try c,Global.lookup_constant c
 	  with Not_found ->
-	    raise (UserError ("",str "Cannot find " ++ Printer.pr_lconstr (mkConst c)) )
+	    raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr (mkConst c)) )
 	  end
-      | _ -> raise (UserError ("", str "Not a function reference") )
+      | _ -> raise (UserError (None, str "Not a function reference") )
   in
   (match Global.body_of_constant_body c_body with
-     | None -> error "Cannot build a graph over an axiom !"
+     | None -> error "Cannot build a graph over an axiom!"
      | Some body ->
 	 let env = Global.env () in
 	 let sigma = Evd.from_env env in
@@ -854,8 +871,8 @@ let make_graph (f_ref:global_reference) =
 	 in
 	 let (nal_tas,b,t)  = get_args extern_body extern_type in
 	 let expr_list =
-	   match b with
-	     | Constrexpr.CFix(loc,l_id,fixexprl) ->
+	   match b.CAst.v with
+	     | Constrexpr.CFix(l_id,fixexprl) ->
 		 let l =
 		   List.map
 		     (fun (id,(n,recexp),bl,t,b) ->
@@ -864,32 +881,32 @@ let make_graph (f_ref:global_reference) =
 			  List.flatten
 			    (List.map
 			       (function
-				  | Constrexpr.LocalRawDef (na,_)-> []
-				  | Constrexpr.LocalRawAssum (nal,_,_) ->
+				  | Constrexpr.CLocalDef (na,_,_)-> []
+				  | Constrexpr.CLocalAssum (nal,_,_) ->
 				      List.map
-					(fun (loc,n) ->
-					   CRef(Libnames.Ident(loc, Nameops.out_name n),None))
+					(fun (loc,n) -> CAst.make ?loc @@ 
+					   CRef(Libnames.Ident(loc, Nameops.Name.get_id n),None))
 					nal
-                                  | Constrexpr.LocalPattern _ -> assert false
+                                  | Constrexpr.CLocalPattern _ -> assert false
 			       )
 			       nal_tas
 			    )
 			in
 			let b' = add_args (snd id) new_args b in
-			((((id,None), ( Some (Loc.ghost,rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
+			((((id,None), ( Some (Loc.tag rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
 		     )
 		     fixexprl
 		 in
 		 l
 	     | _ ->
-		let id = Label.to_id (con_label c) in
-		 [(((Loc.ghost,id),None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
+		let id = Label.to_id (Constant.label c) in
+		 [(((Loc.tag id),None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
 	 in
-	 let mp,dp,_ = repr_con c in
+	 let mp,dp,_ = Constant.repr3 c in
 	 do_generate_principle [c,Univ.Instance.empty] error_error  false false expr_list;
 	 (* We register the infos *)
 	 List.iter
-	   (fun ((((_,id),_),_,_,_,_),_) -> add_Function false (make_con mp dp (Label.of_id id)))
+	   (fun ((((_,id),_),_,_,_,_),_) -> add_Function false (Constant.make3 mp dp (Label.of_id id)))
 	   expr_list)
 
 let do_generate_principle = do_generate_principle [] warning_error true