Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 307 insertions, 256 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4310a01e..b161d001 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrintern.ml 14656 2011-11-16 08:46:31Z herbelin $ *)
-
 open Pp
 open Util
 open Flags
@@ -16,7 +14,7 @@ open Nameops
 open Namegen
 open Libnames
 open Impargs
-open Rawterm
+open Glob_term
 open Pattern
 open Pretyping
 open Cases
@@ -32,6 +30,7 @@ type var_internalization_type =
   | Inductive of identifier list (* list of params *)
   | Recursive
   | Method
+  | Variable
 
 type var_internalization_data =
     (* type of the "free" variable, for coqdoc, e.g. while typing the
@@ -46,9 +45,9 @@ type var_internalization_data =
     scope_name option list
 
 type internalization_env =
-    (identifier * var_internalization_data) list
+    (var_internalization_data) Idmap.t
 
-type raw_binder = (name * binding_kind * rawconstr option * rawconstr)
+type glob_binder = (name * binding_kind * glob_constr option * glob_constr)
 
 let interning_grammar = ref false
 
@@ -167,7 +166,7 @@ let error_inductive_parameter_not_implicit loc =
 (* Pre-computing the implicit arguments and arguments scopes needed   *)
 (* for interpretation *)
 
-let empty_internalization_env = []
+let empty_internalization_env = Idmap.empty
 
 let compute_explicitable_implicit imps = function
   | Inductive params ->
@@ -175,7 +174,7 @@ let compute_explicitable_implicit imps = function
       let sub_impl,_ = list_chop (List.length params) imps in
       let sub_impl' = List.filter is_status_implicit sub_impl in
       List.map name_of_implicit sub_impl'
-  | Recursive | Method ->
+  | Recursive | Method | Variable ->
       (* Unable to know in advance what the implicit arguments will be *)
       []
 
@@ -185,8 +184,9 @@ let compute_internalization_data env ty typ impl =
   (ty, expls_impl, impl, compute_arguments_scope typ)
 
 let compute_internalization_env env ty =
-  list_map3
-    (fun id typ impl -> (id,compute_internalization_data env ty typ impl))
+  list_fold_left3
+    (fun map id typ impl -> Idmap.add id (compute_internalization_data env ty typ impl) map)
+    empty_internalization_env
 
 (**********************************************************************)
 (* Contracting "{ _ }" in notations *)
@@ -234,6 +234,13 @@ let contract_pat_notation ntn (l,ll) =
   (* side effect; don't inline *)
   !ntn',(l,ll)
 
+type intern_env = {
+  ids: Names.Idset.t;
+  unb: bool;
+  tmp_scope: Topconstr.tmp_scope_name option;
+  scopes: Topconstr.scope_name list;
+  impls: internalization_env }
+
 (**********************************************************************)
 (* Remembering the parsing scope of variables in notations            *)
 
@@ -262,7 +269,7 @@ let error_expect_binder_notation_type loc id =
     pr_id id ++
     str " is expected to occur in binding position in the right-hand side.")
 
-let set_var_scope loc id istermvar (_,_,scopt,scopes) ntnvars =
+let set_var_scope loc id istermvar env ntnvars =
   try
     let idscopes,typ = List.assoc id ntnvars in
     if !idscopes <> None &
@@ -270,12 +277,12 @@ let set_var_scope loc id istermvar (_,_,scopt,scopes) ntnvars =
          we can tolerate having a variable occurring several times in
          different scopes: *) typ <> NtnInternTypeIdent &
       make_current_scope (Option.get !idscopes)
-      <> make_current_scope (scopt,scopes) then
+      <> make_current_scope (env.tmp_scope,env.scopes) then
 	error_inconsistent_scope loc id
 	  (make_current_scope (Option.get !idscopes))
-	  (make_current_scope (scopt,scopes))
+	  (make_current_scope (env.tmp_scope,env.scopes))
     else
-      idscopes := Some (scopt,scopes);
+      idscopes := Some (env.tmp_scope,env.scopes);
     match typ with
     | NtnInternTypeBinder ->
 	if istermvar then error_expect_binder_notation_type loc id
@@ -289,24 +296,43 @@ let set_var_scope loc id istermvar (_,_,scopt,scopes) ntnvars =
     (* Not in a notation *)
     ()
 
-let set_type_scope (ids,unb,tmp_scope,scopes) =
-  (ids,unb,Some Notation.type_scope,scopes)
+let set_type_scope env = {env with tmp_scope = Some Notation.type_scope}
 
-let reset_tmp_scope (ids,unb,tmp_scope,scopes) =
-  (ids,unb,None,scopes)
+let reset_tmp_scope env = {env with tmp_scope = None}
 
-let rec it_mkRProd env body =
+let rec it_mkGProd env body =
   match env with
-      (na, bk, _, t) :: tl -> it_mkRProd tl (RProd (dummy_loc, na, bk, t, body))
+      (na, bk, _, t) :: tl -> it_mkGProd tl (GProd (dummy_loc, na, bk, t, body))
     | [] -> body
 
-let rec it_mkRLambda env body =
+let rec it_mkGLambda env body =
   match env with
-      (na, bk, _, t) :: tl -> it_mkRLambda tl (RLambda (dummy_loc, na, bk, t, body))
+      (na, bk, _, t) :: tl -> it_mkGLambda tl (GLambda (dummy_loc, na, bk, t, body))
     | [] -> body
 
 (**********************************************************************)
 (* Utilities for binders                                              *)
+let build_impls = function
+  |Implicit -> (function
+		  |Name id ->  Some (id, Impargs.Manual, (true,true))
+		  |Anonymous -> anomaly "Anonymous implicit argument")
+  |Explicit -> fun _ -> None
+
+let impls_type_list ?(args = []) =
+  let rec aux acc = function
+    |GProd (_,na,bk,_,c) -> aux ((build_impls bk na)::acc) c
+    |_ -> (Variable,[],List.append args (List.rev acc),[])
+  in aux []
+
+let impls_term_list ?(args = []) =
+  let rec aux acc = function
+    |GLambda (_,na,bk,_,c) -> aux ((build_impls bk na)::acc) c
+    |GRec (_, fix_kind, nas, args, tys, bds) ->
+       let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in
+       let acc' = List.fold_left (fun a (na, bk, _, _) -> (build_impls bk na)::a) acc args.(nb) in
+	 aux acc' bds.(nb)
+    |_ -> (Variable,[],List.append args (List.rev acc),[])
+  in aux []
 
 let check_capture loc ty = function
   | Name id when occur_var_constr_expr id ty ->
@@ -315,50 +341,55 @@ let check_capture loc ty = function
       ()
 
 let locate_if_isevar loc na = function
-  | RHole _ ->
+  | GHole _ ->
       (try match na with
-	| Name id ->  Reserve.find_reserved_type id
+	| Name id -> glob_constr_of_aconstr loc (Reserve.find_reserved_type id)
 	| Anonymous -> raise Not_found
-      with Not_found -> RHole (loc, Evd.BinderType na))
+      with Not_found -> GHole (loc, Evd.BinderType na))
   | x -> x
 
-let reset_hidden_inductive_implicit_test (ltacvars,namedctxvars,ntnvars,impls) =
-  let f = function id,(Inductive _,b,c,d) -> id,(Inductive [],b,c,d) | x -> x in
-  (ltacvars,namedctxvars,ntnvars,List.map f impls)
+let reset_hidden_inductive_implicit_test env =
+  { env with impls = Idmap.fold (fun id x ->
+       let x = match x with
+         | (Inductive _,b,c,d) -> (Inductive [],b,c,d)
+         | x -> x
+       in Idmap.add id x) env.impls Idmap.empty }
 
-let check_hidden_implicit_parameters id (_,_,_,impls) =
-  if List.exists (function
-    | (_,(Inductive indparams,_,_,_)) -> List.mem id indparams
+let check_hidden_implicit_parameters id impls =
+  if Idmap.exists (fun _ -> function
+    | (Inductive indparams,_,_,_) -> List.mem id indparams
     | _ -> false) impls
   then
     errorlabstrm "" (strbrk "A parameter of an inductive type " ++
     pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.")
 
-let push_name_env ?(global_level=false) lvar (ids,unb,tmpsc,scopes as env) =
+let push_name_env ?(global_level=false) lvar implargs env =
   function
   | loc,Anonymous ->
       if global_level then
 	user_err_loc (loc,"", str "Anonymous variables not allowed");
       env
   | loc,Name id ->
-      check_hidden_implicit_parameters id lvar;
-      set_var_scope loc id false env (let (_,_,ntnvars,_) = lvar in ntnvars);
+      check_hidden_implicit_parameters id env.impls ;
+      set_var_scope loc id false env (let (_,ntnvars) = lvar in ntnvars);
       if global_level then Dumpglob.dump_definition (loc,id) true "var"
       else Dumpglob.dump_binding loc id;
-      (Idset.add id ids,unb,tmpsc,scopes)
+      {env with ids = Idset.add id env.ids; impls = Idmap.add id implargs env.impls}
 
 let intern_generalized_binder ?(global_level=false) intern_type lvar
-    (ids,unb,tmpsc,sc as env) bl (loc, na) b b' t ty =
-  let ids = match na with Anonymous -> ids | Name na -> Idset.add na ids in
+    env bl (loc, na) b b' t ty =
+  let ids = (match na with Anonymous -> fun x -> x | Name na -> Idset.add na) env.ids in
   let ty, ids' =
     if t then ty, ids else
       Implicit_quantifiers.implicit_application ids
 	Implicit_quantifiers.combine_params_freevar ty
   in
-  let ty' = intern_type (ids,true,tmpsc,sc) ty in
-  let fvs = Implicit_quantifiers.generalizable_vars_of_rawconstr ~bound:ids ~allowed:ids' ty' in
-  let env' = List.fold_left (fun env (x, l) -> push_name_env ~global_level lvar env (l, Name x)) env fvs in
-  let bl = List.map (fun (id, loc) -> (Name id, b, None, RHole (loc, Evd.BinderType (Name id)))) fvs in
+  let ty' = intern_type {env with ids = ids; unb = true} ty in
+  let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:ids ~allowed:ids' ty' in
+  let env' = List.fold_left
+    (fun env (x, l) -> push_name_env ~global_level lvar (Variable,[],[],[])(*?*) env (l, Name x))
+    env fvs in
+  let bl = List.map (fun (id, loc) -> (Name id, b, None, GHole (loc, Evd.BinderType (Name id)))) fvs in
   let na = match na with
     | Anonymous ->
 	if global_level then na
@@ -371,7 +402,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar
 	    in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
 	  in Name name
     | _ -> na
-  in (push_name_env ~global_level lvar env' (loc,na)), (na,b',None,ty') :: List.rev bl
+  in (push_name_env ~global_level lvar (impls_type_list ty')(*?*) env' (loc,na)), (na,b',None,ty') :: List.rev bl
 
 let intern_local_binder_aux ?(global_level=false) intern intern_type lvar (env,bl) = function
   | LocalRawAssum(nal,bk,ty) ->
@@ -382,36 +413,37 @@ let intern_local_binder_aux ?(global_level=false) intern intern_type lvar (env,b
 	  let ty = locate_if_isevar loc na (intern_type env ty) in
 	    List.fold_left
 	     (fun (env,bl) na ->
-	       (push_name_env lvar env na,(snd na,k,None,ty)::bl))
+	       (push_name_env lvar (impls_type_list ty) env na,(snd na,k,None,ty)::bl))
 	      (env,bl) nal
       | Generalized (b,b',t) ->
 	  let env, b = intern_generalized_binder ~global_level intern_type lvar env bl (List.hd nal) b b' t ty in
 	    env, b @ bl)
   | LocalRawDef((loc,na as locna),def) ->
-      (push_name_env lvar env locna,
-      (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
+      let indef = intern env def in
+      (push_name_env lvar (impls_term_list indef) env locna,
+      (na,Explicit,Some(indef),GHole(loc,Evd.BinderType na))::bl)
 
-let intern_generalization intern (ids,unb,tmp_scope,scopes as env) lvar loc bk ak c =
-  let c = intern (ids,true,tmp_scope,scopes) c in
-  let fvs = Implicit_quantifiers.generalizable_vars_of_rawconstr ~bound:ids c in
+let intern_generalization intern env lvar loc bk ak c =
+  let c = intern {env with unb = true} c in
+  let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:env.ids c in
   let env', c' =
     let abs =
       let pi =
 	match ak with
 	| Some AbsPi -> true
-	| None when tmp_scope = Some Notation.type_scope
-	    || List.mem Notation.type_scope scopes -> true
+	| None when env.tmp_scope = Some Notation.type_scope
+	    || List.mem Notation.type_scope env.scopes -> true
 	| _ -> false
       in
 	if pi then
 	  (fun (id, loc') acc ->
-	    RProd (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc))
+	    GProd (join_loc loc' loc, Name id, bk, GHole (loc', Evd.BinderType (Name id)), acc))
 	else
 	  (fun (id, loc') acc ->
-	    RLambda (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc))
+	    GLambda (join_loc loc' loc, Name id, bk, GHole (loc', Evd.BinderType (Name id)), acc))
     in
       List.fold_right (fun (id, loc as lid) (env, acc) ->
-	let env' = push_name_env lvar env (loc, Name id) in
+	let env' = push_name_env lvar (Variable,[],[],[]) env (loc, Name id) in
 	  (env', abs lid acc)) fvs (env,c)
   in c'
 
@@ -425,14 +457,15 @@ let iterate_binder intern lvar (env,bl) = function
 	  let ty = intern_type env ty in
 	  let ty = locate_if_isevar loc na ty in
 	  List.fold_left
-	    (fun (env,bl) na -> (push_name_env lvar env na,(snd na,k,None,ty)::bl))
+	    (fun (env,bl) na -> (push_name_env lvar (impls_type_list ty) env na,(snd na,k,None,ty)::bl))
 	    (env,bl) nal
       | Generalized (b,b',t) ->
 	  let env, b = intern_generalized_binder intern_type lvar env bl (List.hd nal) b b' t ty in
 	    env, b @ bl)
   | LocalRawDef((loc,na as locna),def) ->
-      (push_name_env lvar env locna,
-      (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
+      let indef = intern env def in
+      (push_name_env lvar (impls_term_list indef) env locna,
+      (na,Explicit,Some(indef),GHole(loc,Evd.BinderType na))::bl)
 
 (**********************************************************************)
 (* Syntax extensions                                                  *)
@@ -450,14 +483,14 @@ let find_fresh_name renaming (terms,termlists,binders) id =
   next_ident_away id fvs
 
 let traverse_binder (terms,_,_ as subst)
-    (renaming,(ids,unb,tmpsc,scopes as env))=
+    (renaming,env)=
  function
  | Anonymous -> (renaming,env),Anonymous
  | Name id ->
   try
     (* Binders bound in the notation are considered first-order objects *)
     let _,na = coerce_to_name (fst (List.assoc id terms)) in
-    (renaming,(name_fold Idset.add na ids,unb,tmpsc,scopes)), na
+    (renaming,{env with ids = name_fold Idset.add na env.ids}), na
   with Not_found ->
     (* Binders not bound in the notation do not capture variables *)
     (* outside the notation (i.e. in the substitution) *)
@@ -465,7 +498,7 @@ let traverse_binder (terms,_,_ as subst)
     let renaming' = if id=id' then renaming else (id,id')::renaming in
     (renaming',env), Name id'
 
-let make_letins loc = List.fold_right (fun (na,b,t) c -> RLetIn (loc,na,b,c))
+let make_letins loc = List.fold_right (fun (na,b,t) c -> GLetIn (loc,na,b,c))
 
 let rec subordinate_letins letins = function
   (* binders come in reverse order; the non-let are returned in reverse order together *)
@@ -479,13 +512,13 @@ let rec subordinate_letins letins = function
       letins,[]
 
 let rec subst_iterator y t = function
-  | RVar (_,id) as x -> if id = y then t else x
-  | x -> map_rawconstr (subst_iterator y t) x
+  | GVar (_,id) as x -> if id = y then t else x
+  | x -> map_glob_constr (subst_iterator y t) x
 
-let subst_aconstr_in_rawconstr loc intern lvar subst infos c =
+let subst_aconstr_in_glob_constr loc intern lvar subst infos c =
   let (terms,termlists,binders) = subst in
-  let rec aux (terms,binderopt as subst') (renaming,(ids,unb,_,scopes as env)) c =
-    let subinfos = renaming,(ids,unb,None,scopes) in
+  let rec aux (terms,binderopt as subst') (renaming,env) c =
+    let subinfos = renaming,{env with tmp_scope = None} in
     match c with
     | AVar id ->
       begin
@@ -493,13 +526,14 @@ let subst_aconstr_in_rawconstr loc intern lvar subst infos c =
 	(* of the notations *)
 	try
 	  let (a,(scopt,subscopes)) = List.assoc id terms in
-	  intern (ids,unb,scopt,subscopes@scopes) a
+	  intern {env with tmp_scope = scopt;
+		    scopes = subscopes @ env.scopes} a
 	with Not_found ->
 	try
-	  RVar (loc,List.assoc id renaming)
+	  GVar (loc,List.assoc id renaming)
 	with Not_found ->
 	  (* Happens for local notation joint with inductive/fixpoint defs *)
-	  RVar (loc,id)
+	  GVar (loc,id)
       end
     | AList (x,_,iter,terminator,lassoc) ->
       (try
@@ -516,7 +550,7 @@ let subst_aconstr_in_rawconstr loc intern lvar subst infos c =
       let na =
         try snd (coerce_to_name (fst (List.assoc id terms)))
         with Not_found -> na in
-      RHole (loc,Evd.BinderType na)
+      GHole (loc,Evd.BinderType na)
     | ABinderList (x,_,iter,terminator) ->
       (try
         (* All elements of the list are in scopes (scopt,subscopes) *)
@@ -533,12 +567,12 @@ let subst_aconstr_in_rawconstr loc intern lvar subst infos c =
           anomaly "Inconsistent substitution of recursive notation")
     | AProd (Name id, AHole _, c') when option_mem_assoc id binderopt ->
         let (na,bk,t),letins = snd (Option.get binderopt) in
-	RProd (loc,na,bk,t,make_letins loc letins (aux subst' infos c'))
+	GProd (loc,na,bk,t,make_letins loc letins (aux subst' infos c'))
     | ALambda (Name id,AHole _,c') when option_mem_assoc id binderopt ->
         let (na,bk,t),letins = snd (Option.get binderopt) in
-	RLambda (loc,na,bk,t,make_letins loc letins (aux subst' infos c'))
+	GLambda (loc,na,bk,t,make_letins loc letins (aux subst' infos c'))
     | t ->
-      rawconstr_of_aconstr_with_binders loc (traverse_binder subst)
+      glob_constr_of_aconstr_with_binders loc (traverse_binder subst)
 	(aux subst') subinfos t
   in aux (terms,None) infos c
 
@@ -551,15 +585,15 @@ let split_by_type ids =
 
 let make_subst ids l = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids l
 
-let intern_notation intern (_,_,tmp_scope,scopes as env) lvar loc ntn fullargs =
+let intern_notation intern env lvar loc ntn fullargs =
   let ntn,(args,argslist,bll as fullargs) = contract_notation ntn fullargs in
-  let ((ids,c),df) = interp_notation loc ntn (tmp_scope,scopes) in
+  let ((ids,c),df) = interp_notation loc ntn (env.tmp_scope,env.scopes) in
   Dumpglob.dump_notation_location (ntn_loc loc fullargs ntn) ntn df;
   let ids,idsl,idsbl = split_by_type ids in
   let terms = make_subst ids args in
   let termlists = make_subst idsl argslist in
   let binders = make_subst idsbl bll in
-  subst_aconstr_in_rawconstr loc intern lvar
+  subst_aconstr_in_glob_constr loc intern lvar
     (terms,termlists,binders) ([],env) c
 
 (**********************************************************************)
@@ -569,30 +603,32 @@ let string_of_ty = function
   | Inductive _ -> "ind"
   | Recursive -> "def"
   | Method -> "meth"
+  | Variable -> "var"
 
-let intern_var (ids,_,_,_ as genv) (ltacvars,namedctxvars,ntnvars,impls) loc id =
+let intern_var genv (ltacvars,ntnvars) namedctx loc id =
   let (ltacvars,unbndltacvars) = ltacvars in
   (* Is [id] an inductive type potentially with implicit *)
   try
-    let ty,expl_impls,impls,argsc = List.assoc id impls in
+    let ty,expl_impls,impls,argsc = Idmap.find id genv.impls in
     let expl_impls = List.map
       (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) expl_impls in
     let tys = string_of_ty ty in
     Dumpglob.dump_reference loc "<>" (string_of_id id) tys;
-    RVar (loc,id), make_implicits_list impls, argsc, expl_impls
+    GVar (loc,id), make_implicits_list impls, argsc, expl_impls
   with Not_found ->
   (* Is [id] bound in current term or is an ltac var bound to constr *)
-  if Idset.mem id ids or List.mem id ltacvars
+  if Idset.mem id genv.ids or List.mem id ltacvars
   then
-    RVar (loc,id), [], [], []
+    GVar (loc,id), [], [], []
   (* Is [id] a notation variable *)
+
   else if List.mem_assoc id ntnvars
   then
-    (set_var_scope loc id true genv ntnvars; RVar (loc,id), [], [], [])
+    (set_var_scope loc id true genv ntnvars; GVar (loc,id), [], [], [])
   (* Is [id] the special variable for recursive notations *)
   else if ntnvars <> [] && id = ldots_var
   then
-    RVar (loc,id), [], [], []
+    GVar (loc,id), [], [], []
   else
   (* Is [id] bound to a free name in ltac (this is an ltac error message) *)
   try
@@ -602,7 +638,7 @@ let intern_var (ids,_,_,_ as genv) (ltacvars,namedctxvars,ntnvars,impls) loc id
       | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
   with Not_found ->
     (* Is [id] a goal or section variable *)
-    let _ = Sign.lookup_named id namedctxvars in
+    let _ = Sign.lookup_named id namedctx in
       try
 	(* [id] a section variable *)
 	(* Redundant: could be done in intern_qualid *)
@@ -610,14 +646,14 @@ let intern_var (ids,_,_,_ as genv) (ltacvars,namedctxvars,ntnvars,impls) loc id
 	let impls = implicits_of_global ref in
 	let scopes = find_arguments_scope ref in
 	Dumpglob.dump_reference loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var";
-	RRef (loc, ref), impls, scopes, []
+	GRef (loc, ref), impls, scopes, []
       with _ ->
 	(* [id] a goal variable *)
-	RVar (loc,id), [], [], []
+	GVar (loc,id), [], [], []
 
 let find_appl_head_data = function
-  | RRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[]
-  | RApp (_,RRef (_,ref),l) as x
+  | GRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[]
+  | GApp (_,GRef (_,ref),l) as x
       when l <> [] & Flags.version_strictly_greater Flags.V8_2 ->
       let n = List.length l in
       x,List.map (drop_first_implicits n) (implicits_of_global ref),
@@ -650,7 +686,7 @@ let intern_reference ref =
 let intern_qualid loc qid intern env lvar args =
   match intern_extended_global_of_qualid (loc,qid) with
   | TrueGlobal ref ->
-      RRef (loc, ref), args
+      GRef (loc, ref), args
   | SynDef sp ->
       let (ids,c) = Syntax_def.search_syntactic_definition sp in
       let nids = List.length ids in
@@ -658,20 +694,20 @@ let intern_qualid loc qid intern env lvar args =
       let args1,args2 = list_chop nids args in
       check_no_explicitation args1;
       let subst = make_subst ids (List.map fst args1) in
-      subst_aconstr_in_rawconstr loc intern lvar (subst,[],[]) ([],env) c, args2
+      subst_aconstr_in_glob_constr loc intern lvar (subst,[],[]) ([],env) c, args2
 
 (* Rule out section vars since these should have been found by intern_var *)
 let intern_non_secvar_qualid loc qid intern env lvar args =
   match intern_qualid loc qid intern env lvar args with
-    | RRef (loc, VarRef id),_ -> error_global_not_found_loc loc qid
+    | GRef (loc, VarRef id),_ -> error_global_not_found_loc loc qid
     | r -> r
 
-let intern_applied_reference intern (_, unb, _, _ as env) lvar args = function
+let intern_applied_reference intern env namedctx lvar args = function
   | Qualid (loc, qid) ->
       let r,args2 = intern_qualid loc qid intern env lvar args in
       find_appl_head_data r, args2
   | Ident (loc, id) ->
-      try intern_var env lvar loc id, args
+      try intern_var env lvar namedctx loc id, args
       with Not_found ->
       let qid = qualid_of_ident id in
       try
@@ -679,19 +715,21 @@ let intern_applied_reference intern (_, unb, _, _ as env) lvar args = function
 	find_appl_head_data r, args2
       with e ->
 	(* Extra allowance for non globalizing functions *)
-	if !interning_grammar || unb then
-	  (RVar (loc,id), [], [], []),args
+	if !interning_grammar || env.unb then
+	  (GVar (loc,id), [], [], []),args
 	else raise e
 
 let interp_reference vars r =
   let (r,_,_,_),_ =
     intern_applied_reference (fun _ -> error_not_enough_arguments dummy_loc)
-      (Idset.empty,false,None,[]) (vars,[],[],[]) [] r
+      {ids = Idset.empty; unb = false ;
+       tmp_scope = None; scopes = []; impls = empty_internalization_env} []
+      (vars,[]) [] r
   in r
 
-let apply_scope_env (ids,unb,_,scopes) = function
-  | [] -> (ids,unb,None,scopes), []
-  | sc::scl -> (ids,unb,sc,scopes), scl
+let apply_scope_env env = function
+  | [] -> {env with tmp_scope = None}, []
+  | sc::scl -> {env with tmp_scope = sc}, scl
 
 let rec simple_adjust_scopes n = function
   | [] -> if n=0 then [] else None :: simple_adjust_scopes (n-1) []
@@ -766,8 +804,8 @@ let alias_of = function
   | (id::_,_) -> Name id
 
 let message_redundant_alias (id1,id2) =
-  if_verbose warning
-   ("Alias variable "^(string_of_id id1)^" is merged with "^(string_of_id id2))
+  if_warn msg_warning
+    (str "Alias variable " ++ pr_id id1 ++ str " is merged with " ++ pr_id id2)
 
 (* Expanding notations *)
 
@@ -794,7 +832,7 @@ let rec subst_pat_iterator y t (subst,p) = match p with
       let pl = simple_product_of_cases_patterns l' in
       List.map (fun (subst',pl) -> subst'@subst,PatCstr (loc,id,pl,alias)) pl
 
-let subst_cases_pattern loc alias intern fullsubst scopes a =
+let subst_cases_pattern loc alias intern fullsubst env a =
   let rec aux alias (subst,substlist as fullsubst) = function
   | AVar id ->
       begin
@@ -802,7 +840,8 @@ let subst_cases_pattern loc alias intern fullsubst scopes a =
 	(* of the notations *)
 	try
 	  let (a,(scopt,subscopes)) = List.assoc id subst in
-	    intern (subscopes@scopes) ([],[]) scopt a
+	    intern {env with scopes=subscopes@env.scopes;
+		      tmp_scope = scopt} ([],[]) a
 	with Not_found ->
 	  if id = ldots_var then [], [[], PatVar (loc,Name id)] else
 	  anomaly ("Unbound pattern notation variable: "^(string_of_id id))
@@ -847,7 +886,7 @@ type pattern_qualid_kind =
       ((identifier * identifier) list * cases_pattern) list) list
   | VarPat of identifier
 
-let find_constructor ref f aliases pats scopes =
+let find_constructor ref f aliases pats env =
   let (loc,qid) = qualid_of_reference ref in
   let gref =
     try locate_extended qid
@@ -865,7 +904,7 @@ let find_constructor ref f aliases pats scopes =
 	   if List.length pats < nvars then error_not_enough_arguments loc;
 	   let pats1,pats2 = list_chop nvars pats in
 	   let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) vars pats1 in
-	   let idspl1 = List.map (subst_cases_pattern loc Anonymous f (subst,[]) scopes) args in
+	   let idspl1 = List.map (subst_cases_pattern loc Anonymous f (subst,[]) env) args in
 	   cstr, idspl1, pats2
        | _ -> raise Not_found)
 
@@ -884,9 +923,9 @@ let find_pattern_variable = function
   | Ident (loc,id) -> id
   | Qualid (loc,_) as x -> raise (InternalizationError(loc,NotAConstructor x))
 
-let maybe_constructor ref f aliases scopes =
+let maybe_constructor ref f aliases env =
   try
-    let c,idspl1,pl2 = find_constructor ref f aliases [] scopes in
+    let c,idspl1,pl2 = find_constructor ref f aliases [] env in
     assert (pl2 = []);
     ConstrPat (c,idspl1)
   with
@@ -894,12 +933,12 @@ let maybe_constructor ref f aliases scopes =
     | InternalizationError _ -> VarPat (find_pattern_variable ref)
       (* patt var also exists globally but does not satisfy preconditions *)
     | (Environ.NotEvaluableConst _ | Not_found) ->
-        if_verbose msg_warning (str "pattern " ++ pr_reference ref ++
+        if_warn msg_warning (str "pattern " ++ pr_reference ref ++
               str " is understood as a pattern variable");
         VarPat (find_pattern_variable ref)
 
-let mustbe_constructor loc ref f aliases patl scopes =
-  try find_constructor ref f aliases patl scopes
+let mustbe_constructor loc ref f aliases patl env =
+  try find_constructor ref f aliases patl env
   with (Environ.NotEvaluableConst _ | Not_found) ->
     raise (InternalizationError (loc,NotAConstructor ref))
 
@@ -918,7 +957,7 @@ let sort_fields mode loc l completer =
 	    try Recordops.find_projection
 	      (global_reference_of_reference refer)
 	    with Not_found ->
-	      user_err_loc (loc, "intern", str"Not a projection")
+	      user_err_loc (loc_of_reference refer, "intern", pr_reference refer ++ str": Not a projection")
 	    in
 	  (* elimination of the first field from the projections *)
 	  let rec build_patt l m i acc =
@@ -958,6 +997,10 @@ let sort_fields mode loc l completer =
 	    | [] -> accpatt
 	    | p::q->
 	       let refer, patt = p in
+	       let glob_refer = try global_reference_of_reference refer
+	       with |Not_found ->
+		 user_err_loc (loc_of_reference refer, "intern",
+			       str "The field \"" ++ pr_reference refer ++ str "\" does not exist.") in
 	       let rec add_patt l acc =
 		 match l with
 		   | [] ->
@@ -965,7 +1008,7 @@ let sort_fields mode loc l completer =
 			 (loc, "",
 			  str "This record contains fields of different records.")
 		   | (i, a) :: b->
-		       if global_reference_of_reference refer = a
+		       if glob_refer = a
 		       then (i,List.rev_append acc l)
 		       else add_patt b ((i,a)::acc)
 	         in
@@ -988,12 +1031,12 @@ let sort_fields mode loc l completer =
 	Some (nparams, base_constructor,
 	  List.rev (clean_list sorted_indexed_pattern 0 []))
 
-let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat=
+let rec intern_cases_pattern genv env (ids,asubst as aliases) pat =
   let intern_pat = intern_cases_pattern genv in
   match pat with
   | CPatAlias (loc, p, id) ->
       let aliases' = merge_aliases aliases id in
-      intern_pat scopes aliases' tmp_scope p
+      intern_pat env aliases' p
     | CPatRecord (loc, l) ->
 	let sorted_fields = sort_fields false loc l (fun _ l -> (CPatAtom (loc, None))::l) in
 	let self_patt =
@@ -1001,41 +1044,42 @@ let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat=
 	    | None -> CPatAtom (loc, None)
 	    | Some (_, head, pl) -> CPatCstr(loc, head, pl)
 	  in
-	intern_pat scopes aliases tmp_scope self_patt
-  | CPatCstr (loc, head, pl) ->
-      let c,idslpl1,pl2 = mustbe_constructor loc head intern_pat aliases pl scopes in
+	intern_pat env aliases self_patt
+  | CPatCstr (loc, head, pl) | CPatCstrExpl (loc, head, pl) ->
+      let c,idslpl1,pl2 = mustbe_constructor loc head intern_pat aliases pl env in
       check_constructor_length genv loc c idslpl1 pl2;
       let argscs2 = find_remaining_constructor_scopes idslpl1 pl2 c in
-      let idslpl2 = List.map2 (intern_pat scopes ([],[])) argscs2 pl2 in
+      let idslpl2 = List.map2 (fun x -> intern_pat {env with tmp_scope = x} ([],[])) argscs2 pl2 in
       let (ids',pll) = product_of_cases_patterns ids (idslpl1@idslpl2) in
       let pl' = List.map (fun (asubst,pl) ->
         (asubst, PatCstr (loc,c,pl,alias_of aliases))) pll in
       ids',pl'
   | CPatNotation (loc,"- _",([CPatPrim(_,Numeral p)],[]))
       when Bigint.is_strictly_pos p ->
-      intern_pat scopes aliases tmp_scope (CPatPrim(loc,Numeral(Bigint.neg p)))
+      intern_pat env aliases (CPatPrim(loc,Numeral(Bigint.neg p)))
   | CPatNotation (_,"( _ )",([a],[])) ->
-      intern_pat scopes aliases tmp_scope a
+      intern_pat env aliases a
   | CPatNotation (loc, ntn, fullargs) ->
       let ntn,(args,argsl as fullargs) = contract_pat_notation ntn fullargs in
-      let ((ids',c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
+      let ((ids',c),df) = Notation.interp_notation loc ntn (env.tmp_scope,env.scopes) in
       let (ids',idsl',_) = split_by_type ids' in
       Dumpglob.dump_notation_location (patntn_loc loc fullargs ntn) ntn df;
       let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in
       let substlist = List.map2 (fun (id,scl) a -> (id,(a,scl))) idsl' argsl in
       let ids'',pl =
 	subst_cases_pattern loc (alias_of aliases) intern_pat (subst,substlist)
-	  scopes c
+	  env c
       in ids@ids'', pl
   | CPatPrim (loc, p) ->
       let a = alias_of aliases in
       let (c,_) = Notation.interp_prim_token_cases_pattern loc p a
-	(tmp_scope,scopes) in
+	(env.tmp_scope,env.scopes) in
       (ids,[asubst,c])
   | CPatDelimiters (loc, key, e) ->
-      intern_pat (find_delimiters_scope loc key::scopes) aliases None e
+      intern_pat {env with scopes=find_delimiters_scope loc key::env.scopes;
+		    tmp_scope = None} aliases e
   | CPatAtom (loc, Some head) ->
-      (match maybe_constructor head intern_pat aliases scopes with
+      (match maybe_constructor head intern_pat aliases env with
 	 | ConstrPat (c,idspl) ->
 	     check_constructor_length genv loc c idspl [];
 	     let (ids',pll) = product_of_cases_patterns ids idspl in
@@ -1048,7 +1092,7 @@ let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat=
       (ids,[asubst, PatVar (loc,alias_of aliases)])
   | CPatOr (loc, pl) ->
       assert (pl <> []);
-      let pl' = List.map (intern_pat scopes aliases tmp_scope) pl in
+      let pl' = List.map (intern_pat env aliases) pl in
       let (idsl,pl') = List.split pl' in
       let ids = List.hd idsl in
       check_or_pat_variables loc ids (List.tl idsl);
@@ -1067,7 +1111,7 @@ let merge_impargs l args =
 
 let check_projection isproj nargs r =
   match (r,isproj) with
-  | RRef (loc, ref), Some _ ->
+  | GRef (loc, ref), Some _ ->
       (try
 	let n = Recordops.find_projection_nparams ref + 1 in
 	if nargs <> n then
@@ -1075,15 +1119,15 @@ let check_projection isproj nargs r =
       with Not_found ->
 	user_err_loc
 	(loc,"",pr_global_env Idset.empty ref ++ str " is not a registered projection."))
-  | _, Some _ -> user_err_loc (loc_of_rawconstr r, "", str "Not a projection.")
+  | _, Some _ -> user_err_loc (loc_of_glob_constr r, "", str "Not a projection.")
   | _, None -> ()
 
 let get_implicit_name n imps =
   Some (Impargs.name_of_implicit (List.nth imps (n-1)))
 
 let set_hole_implicit i b = function
-  | RRef (loc,r) | RApp (_,RRef (loc,r),_) -> (loc,Evd.ImplicitArg (r,i,b))
-  | RVar (loc,id) -> (loc,Evd.ImplicitArg (VarRef id,i,b))
+  | GRef (loc,r) | GApp (_,GRef (loc,r),_) -> (loc,Evd.ImplicitArg (r,i,b))
+  | GVar (loc,id) -> (loc,Evd.ImplicitArg (VarRef id,i,b))
   | _ -> anomaly "Only refs have implicits"
 
 let exists_implicit_name id =
@@ -1127,13 +1171,13 @@ let extract_explicit_arg imps args =
 (* Main loop                                                          *)
 
 let internalize sigma globalenv env allow_patvar lvar c =
-  let rec intern (ids,unb,tmp_scope,scopes as env) = function
+  let rec intern env = function
     | CRef ref as x ->
 	let (c,imp,subscopes,l),_ =
-	  intern_applied_reference intern env lvar [] ref in
+	  intern_applied_reference intern env (Environ.named_context globalenv) lvar [] ref in
 	(match intern_impargs c env imp subscopes l with
-          | [] -> c
-          | l -> RApp (constr_loc x, c, l))
+           | [] -> c
+           | l -> GApp (constr_loc x, c, l))
     | CFix (loc, (locid,iddef), dl) ->
         let lf = List.map (fun ((_, id),_,_,_,_) -> id) dl in
         let dl = Array.of_list dl in
@@ -1142,30 +1186,34 @@ let internalize sigma globalenv env allow_patvar lvar c =
           with Not_found ->
 	    raise (InternalizationError (locid,UnboundFixName (false,iddef)))
 	in
-        let idl = Array.map
-          (fun (id,(n,order),bl,ty,bd) ->
+	let idl_temp = Array.map
+          (fun (id,(n,order),bl,ty,_) ->
 	     let intern_ro_arg f =
 	       let before, after = split_at_annot bl n in
-	       let ((ids',_,_,_) as env',rbefore) =
+	       let (env',rbefore) =
 		 List.fold_left intern_local_binder (env,[]) before in
-	       let ro = f (intern (ids', unb, tmp_scope, scopes)) in
+	       let ro = f (intern env') in
 	       let n' = Option.map (fun _ -> List.length rbefore) n in
 		 n', ro, List.fold_left intern_local_binder (env',rbefore) after
 	     in
-	     let n, ro, ((ids',_,_,_),rbl) =
+	     let n, ro, (env',rbl) =
 	       match order with
 	       | CStructRec ->
-		   intern_ro_arg (fun _ -> RStructRec)
+		   intern_ro_arg (fun _ -> GStructRec)
 	       | CWfRec c ->
-		   intern_ro_arg (fun f -> RWfRec (f c))
+		   intern_ro_arg (fun f -> GWfRec (f c))
 	       | CMeasureRec (m,r) ->
-		   intern_ro_arg (fun f -> RMeasureRec (f m, Option.map f r))
+		   intern_ro_arg (fun f -> GMeasureRec (f m, Option.map f r))
 	     in
-	     let ids'' = List.fold_right Idset.add lf ids' in
-	     ((n, ro), List.rev rbl,
-             intern_type (ids',unb,tmp_scope,scopes) ty,
-             intern (ids'',unb,None,scopes) bd)) dl in
-	RRec (loc,RFix
+	       ((n, ro), List.rev rbl, intern_type env' ty, env')) dl in
+        let idl = array_map2 (fun (_,_,_,_,bd) (a,b,c,env') ->
+	     let env'' = list_fold_left_i (fun i en name -> 
+					     let (_,bli,tyi,_) = idl_temp.(i) in
+					     let fix_args = (List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli) in
+					       push_name_env lvar (impls_type_list ~args:fix_args tyi)
+					    en (dummy_loc, Name name)) 0 env' lf in
+             (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in
+	GRec (loc,GFix
 	      (Array.map (fun (ro,_,_,_) -> ro) idl,n),
               Array.of_list lf,
               Array.map (fun (_,bl,_,_) -> bl) idl,
@@ -1179,21 +1227,26 @@ let internalize sigma globalenv env allow_patvar lvar c =
           with Not_found ->
 	    raise (InternalizationError (locid,UnboundFixName (true,iddef)))
 	in
-        let idl = Array.map
-          (fun (id,bl,ty,bd) ->
-            let ((ids',_,_,_),rbl) =
+        let idl_tmp = Array.map
+          (fun (id,bl,ty,_) ->
+            let (env',rbl) =
               List.fold_left intern_local_binder (env,[]) bl in
-	    let ids'' = List.fold_right Idset.add lf ids' in
             (List.rev rbl,
-             intern_type (ids',unb,tmp_scope,scopes) ty,
-             intern (ids'',unb,None,scopes) bd)) dl in
-	RRec (loc,RCoFix n,
+             intern_type env' ty,env')) dl in
+	let idl = array_map2 (fun (_,_,_,bd) (b,c,env') ->
+	     let env'' = list_fold_left_i (fun i en name ->
+					     let (bli,tyi,_) = idl_tmp.(i) in
+					     let cofix_args =  List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli in
+	       push_name_env lvar (impls_type_list ~args:cofix_args tyi)
+					    en (dummy_loc, Name name)) 0 env' lf in
+             (b,c,intern {env'' with tmp_scope = None} bd)) dl idl_tmp in
+	GRec (loc,GCoFix n,
               Array.of_list lf,
               Array.map (fun (bl,_,_) -> bl) idl,
               Array.map (fun (_,ty,_) -> ty) idl,
               Array.map (fun (_,_,bd) -> bd) idl)
     | CArrow (loc,c1,c2) ->
-        RProd (loc, Anonymous, Explicit, intern_type env c1, intern_type env c2)
+        GProd (loc, Anonymous, Explicit, intern_type env c1, intern_type env c2)
     | CProdN (loc,[],c2) ->
         intern_type env c2
     | CProdN (loc,(nal,bk,ty)::bll,c2) ->
@@ -1203,8 +1256,9 @@ let internalize sigma globalenv env allow_patvar lvar c =
     | CLambdaN (loc,(nal,bk,ty)::bll,c2) ->
 	iterate_lam loc (reset_tmp_scope env) bk ty (CLambdaN (loc, bll, c2)) nal
     | CLetIn (loc,na,c1,c2) ->
-	RLetIn (loc, snd na, intern (reset_tmp_scope env) c1,
-          intern (push_name_env lvar env na) c2)
+	let inc1 = intern (reset_tmp_scope env) c1 in
+	GLetIn (loc, snd na, inc1,
+          intern (push_name_env lvar (impls_term_list inc1) env na) c2)
     | CNotation (loc,"- _",([CPrim (_,Numeral p)],[],[]))
 	when Bigint.is_strictly_pos p ->
 	intern env (CPrim (loc,Numeral (Bigint.neg p)))
@@ -1214,16 +1268,17 @@ let internalize sigma globalenv env allow_patvar lvar c =
     | CGeneralization (loc,b,a,c) ->
         intern_generalization intern env lvar loc b a c
     | CPrim (loc, p) ->
-	fst (Notation.interp_prim_token loc p (tmp_scope,scopes))
+	fst (Notation.interp_prim_token loc p (env.tmp_scope,env.scopes))
     | CDelimiters (loc, key, e) ->
-	intern (ids,unb,None,find_delimiters_scope loc key::scopes) e
+	intern {env with tmp_scope = None;
+		  scopes = find_delimiters_scope loc key :: env.scopes} e
     | CAppExpl (loc, (isproj,ref), args) ->
         let (f,_,args_scopes,_),args =
 	  let args = List.map (fun a -> (a,None)) args in
-	  intern_applied_reference intern env lvar args ref in
+	  intern_applied_reference intern env (Environ.named_context globalenv) lvar args ref in
 	check_projection isproj (List.length args) f;
-	(* Rem: RApp(_,f,[]) stands for @f *)
-	RApp (loc, f, intern_args env args_scopes (List.map fst args))
+	(* Rem: GApp(_,f,[]) stands for @f *)
+	GApp (loc, f, intern_args env args_scopes (List.map fst args))
     | CApp (loc, (isproj,f), args) ->
         let isproj,f,args = match f with
           (* Compact notations like "t.(f args') args" *)
@@ -1232,7 +1287,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
           | _ -> isproj,f,args in
 	let (c,impargs,args_scopes,l),args =
           match f with
-            | CRef ref -> intern_applied_reference intern env lvar args ref
+            | CRef ref -> intern_applied_reference intern env (Environ.named_context globalenv) lvar args ref
             | CNotation (loc,ntn,([],[],[])) ->
                 let c = intern_notation intern env lvar loc ntn ([],[],[]) in
                 find_appl_head_data c, args
@@ -1242,8 +1297,8 @@ let internalize sigma globalenv env allow_patvar lvar c =
 	check_projection isproj (List.length args) c;
 	(match c with
           (* Now compact "(f args') args" *)
-	  | RApp (loc', f', args') -> RApp (join_loc loc' loc, f',args'@args)
-	  | _ -> RApp (loc, c, args))
+	  | GApp (loc', f', args') -> GApp (join_loc loc' loc, f',args'@args)
+	  | _ -> GApp (loc, c, args))
     | CRecord (loc, _, fs) ->
 	let cargs =
 	  sort_fields true loc fs
@@ -1261,48 +1316,40 @@ let internalize sigma globalenv env allow_patvar lvar c =
         let tms,env' = List.fold_right
           (fun citm (inds,env) ->
 	    let (tm,ind),nal = intern_case_item env citm in
-	    (tm,ind)::inds,List.fold_left
-              (push_name_env (reset_hidden_inductive_implicit_test lvar))
-              env nal)
+	    (tm,ind)::inds,List.fold_left (push_name_env lvar (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal)
 	  tms ([],env) in
         let rtnpo = Option.map (intern_type env') rtnpo in
         let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
-	RCases (loc, sty, rtnpo, tms, List.flatten eqns')
+	GCases (loc, sty, rtnpo, tms, List.flatten eqns')
     | CLetTuple (loc, nal, (na,po), b, c) ->
 	let env' = reset_tmp_scope env in
         let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in
         let p' = Option.map (fun p ->
-          let env'' = List.fold_left 
-            (push_name_env (reset_hidden_inductive_implicit_test lvar))
-            env ids in
+          let env'' = List.fold_left (push_name_env lvar (Variable,[],[],[])) env ids in
 	  intern_type env'' p) po in
-        RLetTuple (loc, List.map snd nal, (na', p'), b',
-                   intern (List.fold_left (push_name_env lvar) env nal) c)
+        GLetTuple (loc, List.map snd nal, (na', p'), b',
+                   intern (List.fold_left (push_name_env lvar (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c)
     | CIf (loc, c, (na,po), b1, b2) ->
 	let env' = reset_tmp_scope env in
         let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in
         let p' = Option.map (fun p ->
-          let env'' = List.fold_left
-            (push_name_env (reset_hidden_inductive_implicit_test lvar))
-            env ids in
+          let env'' = List.fold_left (push_name_env lvar (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) ids in
 	  intern_type env'' p) po in
-        RIf (loc, c', (na', p'), intern env b1, intern env b2)
+        GIf (loc, c', (na', p'), intern env b1, intern env b2)
     | CHole (loc, k) ->
-	RHole (loc, match k with Some k -> k | None -> Evd.QuestionMark (Evd.Define true))
+	GHole (loc, match k with Some k -> k | None -> Evd.QuestionMark (Evd.Define true))
     | CPatVar (loc, n) when allow_patvar ->
-	RPatVar (loc, n)
+	GPatVar (loc, n)
     | CPatVar (loc, _) ->
 	raise (InternalizationError (loc,IllegalMetavariable))
     | CEvar (loc, n, l) ->
-	REvar (loc, n, Option.map (List.map (intern env)) l)
+	GEvar (loc, n, Option.map (List.map (intern env)) l)
     | CSort (loc, s) ->
-	RSort(loc,s)
+	GSort(loc,s)
     | CCast (loc, c1, CastConv (k, c2)) ->
-	RCast (loc,intern env c1, CastConv (k, intern_type env c2))
+	GCast (loc,intern env c1, CastConv (k, intern_type env c2))
     | CCast (loc, c1, CastCoerce) ->
-	RCast (loc,intern env c1, CastCoerce)
-
-    | CDynamic (loc,d) -> RDynamic (loc,d)
+	GCast (loc,intern env c1, CastCoerce)
 
   and intern_type env = intern (set_type_scope env)
 
@@ -1310,52 +1357,52 @@ let internalize sigma globalenv env allow_patvar lvar c =
     intern_local_binder_aux intern intern_type lvar env bind
 
   (* Expands a multiple pattern into a disjunction of multiple patterns *)
-  and intern_multiple_pattern scopes n (loc,pl) =
+  and intern_multiple_pattern env n (loc,pl) =
     let idsl_pll =
-      List.map (intern_cases_pattern globalenv scopes ([],[]) None) pl in
+      List.map (intern_cases_pattern globalenv {env with tmp_scope = None} ([],[])) pl in
     check_number_of_pattern loc n pl;
     product_of_cases_patterns [] idsl_pll
 
   (* Expands a disjunction of multiple pattern *)
-  and intern_disjunctive_multiple_pattern scopes loc n mpl =
+  and intern_disjunctive_multiple_pattern env loc n mpl =
     assert (mpl <> []);
-    let mpl' = List.map (intern_multiple_pattern scopes n) mpl in
+    let mpl' = List.map (intern_multiple_pattern env n) mpl in
     let (idsl,mpl') = List.split mpl' in
     let ids = List.hd idsl in
     check_or_pat_variables loc ids (List.tl idsl);
     (ids,List.flatten mpl')
 
   (* Expands a pattern-matching clause [lhs => rhs] *)
-  and intern_eqn n (ids,unb,tmp_scope,scopes) (loc,lhs,rhs) =
-    let eqn_ids,pll = intern_disjunctive_multiple_pattern scopes loc n lhs in
+  and intern_eqn n env (loc,lhs,rhs) =
+    let eqn_ids,pll = intern_disjunctive_multiple_pattern env loc n lhs in
     (* Linearity implies the order in ids is irrelevant *)
     check_linearity lhs eqn_ids;
-    let env_ids = List.fold_right Idset.add eqn_ids ids in
+    let env_ids = List.fold_right Idset.add eqn_ids env.ids in
     List.map (fun (asubst,pl) ->
       let rhs = replace_vars_constr_expr asubst rhs in
       List.iter message_redundant_alias asubst;
-      let rhs' = intern (env_ids,unb,tmp_scope,scopes) rhs in
+      let rhs' = intern {env with ids = env_ids} rhs in
       (loc,eqn_ids,pl,rhs')) pll
 
-  and intern_case_item (vars,unb,_,scopes as env) (tm,(na,t)) =
+  and intern_case_item env (tm,(na,t)) =
     let tm' = intern env tm in
     let ids,typ = match t with
     | Some t ->
 	let tids = ids_of_cases_indtype t in
 	let tids = List.fold_right Idset.add tids Idset.empty in
-	let t = intern_type (tids,unb,None,scopes) t in
+	let t = intern_type {env with ids = tids; tmp_scope = None} t in
 	let loc,ind,l = match t with
-	    | RRef (loc,IndRef ind) -> (loc,ind,[])
-	    | RApp (loc,RRef (_,IndRef ind),l) -> (loc,ind,l)
-	    | _ -> error_bad_inductive_type (loc_of_rawconstr t) in
+	    | GRef (loc,IndRef ind) -> (loc,ind,[])
+	    | GApp (loc,GRef (_,IndRef ind),l) -> (loc,ind,l)
+	    | _ -> error_bad_inductive_type (loc_of_glob_constr t) in
 	let nparams, nrealargs = inductive_nargs globalenv ind in
 	let nindargs = nparams + nrealargs in
 	if List.length l <> nindargs then
 	  error_wrong_numarg_inductive_loc loc globalenv ind nindargs;
 	let nal = List.map (function
-	  | RHole (loc,_) -> loc,Anonymous
-	  | RVar (loc,id) -> loc,Name id
-	  | c -> user_err_loc (loc_of_rawconstr c,"",str "Not a name.")) l in
+	  | GHole (loc,_) -> loc,Anonymous
+	  | GVar (loc,id) -> loc,Name id
+	  | c -> user_err_loc (loc_of_glob_constr c,"",str "Not a name.")) l in
 	let parnal,realnal = list_chop nparams nal in
 	if List.exists (fun (_,na) -> na <> Anonymous) parnal then
 	  error_inductive_parameter_not_implicit loc;
@@ -1363,8 +1410,8 @@ let internalize sigma globalenv env allow_patvar lvar c =
     | None ->
 	[], None in
     let na = match tm', na with
-      | RVar (loc,id), None when Idset.mem id vars -> loc,Name id
-      | RRef (loc, VarRef id), None -> loc,Name id
+      | GVar (loc,id), None when Idset.mem id env.ids -> loc,Name id
+      | GRef (loc, VarRef id), None -> loc,Name id
       | _, None -> dummy_loc,Anonymous
       | _, Some (loc,na) -> loc,na in
     (tm',(snd na,typ)), na::ids
@@ -1373,9 +1420,9 @@ let internalize sigma globalenv env allow_patvar lvar c =
     let rec default env bk = function
     | (loc1,na as locna)::nal ->
 	if nal <> [] then check_capture loc1 ty na;
-	let body = default (push_name_env lvar env locna) bk nal in
 	let ty = locate_if_isevar loc1 na (intern_type env ty) in
-	  RProd (join_loc loc1 loc2, na, bk, ty, body)
+	let body = default (push_name_env lvar (impls_type_list ty) env locna) bk nal in
+	  GProd (join_loc loc1 loc2, na, bk, ty, body)
     | [] -> intern_type env body
     in
       match bk with
@@ -1383,22 +1430,22 @@ let internalize sigma globalenv env allow_patvar lvar c =
 	| Generalized (b,b',t) ->
 	    let env, ibind = intern_generalized_binder intern_type lvar env [] (List.hd nal) b b' t ty in
 	    let body = intern_type env body in
-	      it_mkRProd ibind body
+	      it_mkGProd ibind body
 
   and iterate_lam loc2 env bk ty body nal =
     let rec default env bk = function
       | (loc1,na as locna)::nal ->
 	  if nal <> [] then check_capture loc1 ty na;
-	  let body = default (push_name_env lvar env locna) bk nal in
 	  let ty = locate_if_isevar loc1 na (intern_type env ty) in
-	    RLambda (join_loc loc1 loc2, na, bk, ty, body)
+	  let body = default (push_name_env lvar (impls_type_list ty) env locna) bk nal in
+	    GLambda (join_loc loc1 loc2, na, bk, ty, body)
       | [] -> intern env body
     in match bk with
       | Default b -> default env b nal
       | Generalized (b, b', t) ->
 	  let env, ibind = intern_generalized_binder intern_type lvar env [] (List.hd nal) b b' t ty in
 	  let body = intern env body in
-	    it_mkRLambda ibind body
+	    it_mkGLambda ibind body
 
   and intern_impargs c env l subscopes args =
     let l = select_impargs_size (List.length args) l in
@@ -1418,7 +1465,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
             (* with implicit arguments if maximal insertion is set *)
 	    []
 	  else
-	    RHole (set_hole_implicit (n,get_implicit_name n l) (force_inference_of imp) c) ::
+	    GHole (set_hole_implicit (n,get_implicit_name n l) (force_inference_of imp) c) ::
 	      aux (n+1) impl' subscopes' eargs rargs
 	  end
       | (imp::impl', a::rargs') ->
@@ -1426,7 +1473,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
       | (imp::impl', []) ->
 	  if eargs <> [] then
 	    (let (id,(loc,_)) = List.hd eargs in
-	       user_err_loc (loc,"",str "Not enough non implicit
+	       user_err_loc (loc,"",str "Not enough non implicit \
 	    arguments to accept the argument bound to " ++
 		 pr_id id ++ str"."));
 	  []
@@ -1450,7 +1497,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
 	  explain_internalization_error e)
 
 (**************************************************************************)
-(* Functions to translate constr_expr into rawconstr                       *)
+(* Functions to translate constr_expr into glob_constr                    *)
 (**************************************************************************)
 
 let extract_ids env =
@@ -1459,32 +1506,34 @@ let extract_ids env =
     Idset.empty
 
 let intern_gen isarity sigma env
-               ?(impls=[]) ?(allow_patvar=false) ?(ltacvars=([],[]))
+               ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[]))
                c =
   let tmp_scope =
     if isarity then Some Notation.type_scope else None in
-    internalize sigma env (extract_ids env, false, tmp_scope,[])
-      allow_patvar (ltacvars,Environ.named_context env, [], impls) c
+    internalize sigma env {ids = extract_ids env; unb = false;
+			   tmp_scope = tmp_scope; scopes = [];
+			  impls = impls}
+      allow_patvar (ltacvars, []) c
 
 let intern_constr sigma env c = intern_gen false sigma env c
 
 let intern_type sigma env c = intern_gen true sigma env c
 
-let intern_pattern env patt =
+let intern_pattern globalenv patt =
   try
-    intern_cases_pattern env [] ([],[]) None patt
+    intern_cases_pattern globalenv {ids = extract_ids globalenv; unb = false;
+				    tmp_scope = None; scopes = [];
+				    impls = empty_internalization_env} ([],[]) patt
   with
       InternalizationError (loc,e) ->
 	user_err_loc (loc,"internalize",explain_internalization_error e)
 
 
-type manual_implicits = (explicitation * (bool * bool * bool)) list
-
 (*********************************************************************)
 (* Functions to parse and interpret constructions *)
 
 let interp_gen kind sigma env
-               ?(impls=[]) ?(allow_patvar=false) ?(ltacvars=([],[]))
+               ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[]))
                c =
   let c = intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars sigma env c in
     Default.understand_gen kind sigma env c
@@ -1492,10 +1541,10 @@ let interp_gen kind sigma env
 let interp_constr sigma env c =
   interp_gen (OfType None) sigma env c
 
-let interp_type sigma env ?(impls=[]) c =
+let interp_type sigma env ?(impls=empty_internalization_env) c =
   interp_gen IsType sigma env ~impls c
 
-let interp_casted_constr sigma env ?(impls=[]) c typ =
+let interp_casted_constr sigma env ?(impls=empty_internalization_env) c typ =
   interp_gen (OfType (Some typ)) sigma env ~impls c
 
 let interp_open_constr sigma env c =
@@ -1503,19 +1552,19 @@ let interp_open_constr sigma env c =
 
 let interp_open_constr_patvar sigma env c =
   let raw = intern_gen false sigma env c ~allow_patvar:true in
-  let sigma = ref (Evd.create_evar_defs sigma) in
-  let evars = ref (Gmap.empty : (identifier,rawconstr) Gmap.t) in
+  let sigma = ref sigma in
+  let evars = ref (Gmap.empty : (identifier,glob_constr) Gmap.t) in
   let rec patvar_to_evar r = match r with
-    | RPatVar (loc,(_,id)) ->
+    | GPatVar (loc,(_,id)) ->
 	( try Gmap.find id !evars
 	  with Not_found ->
 	    let ev = Evarutil.e_new_evar sigma env (Termops.new_Type()) in
 	    let ev = Evarutil.e_new_evar sigma env ev in
-	    let rev = REvar (loc,(fst (Term.destEvar ev)),None) (*TODO*) in
+	    let rev = GEvar (loc,(fst (Term.destEvar ev)),None) (*TODO*) in
 	    evars := Gmap.add id rev !evars;
 	    rev
 	)
-    | _ -> map_rawconstr patvar_to_evar r in
+    | _ -> map_glob_constr patvar_to_evar r in
   let raw = patvar_to_evar raw in
   Default.understand_tcc !sigma env raw
 
@@ -1523,7 +1572,7 @@ let interp_constr_judgment sigma env c =
   Default.understand_judgment sigma env (intern_constr sigma env c)
 
 let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true)
-    env ?(impls=[]) kind c =
+    env ?(impls=empty_internalization_env) kind c =
   let evdref =
     match evdref with
     | None -> ref Evd.empty
@@ -1531,43 +1580,44 @@ let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true)
   in
   let istype = kind = IsType in
   let c = intern_gen istype ~impls !evdref env c in
-  let imps = Implicit_quantifiers.implicits_of_rawterm ~with_products:istype c in
+  let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:istype c in
     Default.understand_tcc_evars ~fail_evar evdref env kind c, imps
 
 let interp_casted_constr_evars_impls ?evdref ?(fail_evar=true)
-    env ?(impls=[]) c typ =
+    env ?(impls=empty_internalization_env) c typ =
   interp_constr_evars_gen_impls ?evdref ~fail_evar env ~impls (OfType (Some typ)) c
 
-let interp_type_evars_impls ?evdref ?(fail_evar=true) env ?(impls=[]) c =
+let interp_type_evars_impls ?evdref ?(fail_evar=true) env ?(impls=empty_internalization_env) c =
   interp_constr_evars_gen_impls ?evdref ~fail_evar env IsType ~impls c
 
-let interp_constr_evars_impls ?evdref ?(fail_evar=true) env ?(impls=[]) c =
+let interp_constr_evars_impls ?evdref ?(fail_evar=true) env ?(impls=empty_internalization_env) c =
   interp_constr_evars_gen_impls ?evdref ~fail_evar env (OfType None) ~impls c
 
-let interp_constr_evars_gen evdref env ?(impls=[]) kind c =
-  let c = intern_gen (kind=IsType) ~impls ( !evdref) env c in
+let interp_constr_evars_gen evdref env ?(impls=empty_internalization_env) kind c =
+  let c = intern_gen (kind=IsType) ~impls !evdref env c in
     Default.understand_tcc_evars evdref env kind c
 
-let interp_casted_constr_evars evdref env ?(impls=[]) c typ =
+let interp_casted_constr_evars evdref env ?(impls=empty_internalization_env) c typ =
   interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c
 
-let interp_type_evars evdref env ?(impls=[]) c =
+let interp_type_evars evdref env ?(impls=empty_internalization_env) c =
   interp_constr_evars_gen evdref env IsType ~impls c
 
 type ltac_sign = identifier list * unbound_ltac_var_map
 
 let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=([],[])) c =
   let c = intern_gen as_type ~allow_patvar:true ~ltacvars sigma env c in
-  pattern_of_rawconstr c
+  pattern_of_glob_constr c
 
-let interp_aconstr ?(impls=[]) vars recvars a =
+let interp_aconstr ?(impls=empty_internalization_env) vars recvars a =
   let env = Global.env () in
   (* [vl] is intended to remember the scope of the free variables of [a] *)
   let vl = List.map (fun (id,typ) -> (id,(ref None,typ))) vars in
-  let c = internalize Evd.empty (Global.env()) (extract_ids env, false, None, [])
-    false (([],[]),Environ.named_context env,vl,impls) a in
+  let c = internalize Evd.empty (Global.env()) {ids = extract_ids env; unb = false;
+						tmp_scope = None; scopes = []; impls = impls}
+    false (([],[]),vl) a in
   (* Translate and check that [c] has all its free variables bound in [vars] *)
-  let a = aconstr_of_rawconstr vars recvars c in
+  let a = aconstr_of_glob_constr vars recvars c in
   (* Splits variables into those that are binding, bound, or both *)
   (* binding and bound *)
   let out_scope = function None -> None,[] | Some (a,l) -> a,l in
@@ -1579,12 +1629,12 @@ let interp_aconstr ?(impls=[]) vars recvars a =
 
 let interp_binder sigma env na t =
   let t = intern_gen true sigma env t in
-  let t' = locate_if_isevar (loc_of_rawconstr t) na t in
+  let t' = locate_if_isevar (loc_of_glob_constr t) na t in
   Default.understand_type sigma env t'
 
 let interp_binder_evars evdref env na t =
   let t = intern_gen true !evdref env t in
-  let t' = locate_if_isevar (loc_of_rawconstr t) na t in
+  let t' = locate_if_isevar (loc_of_glob_constr t) na t in
   Default.understand_tcc_evars evdref env IsType t'
 
 open Environ
@@ -1595,11 +1645,12 @@ let my_intern_constr sigma env lvar acc c =
 
 let my_intern_type sigma env lvar acc c = my_intern_constr sigma env lvar (set_type_scope acc) c
 
-let intern_context global_level sigma env params =
-  let lvar = (([],[]),Environ.named_context env, [], []) in
-    snd (List.fold_left
+let intern_context global_level sigma env impl_env params =
+  let lvar = (([],[]), []) in
+  let lenv, bl = List.fold_left
 	    (intern_local_binder_aux ~global_level (my_intern_constr sigma env lvar) (my_intern_type sigma env lvar) lvar)
-	    ((extract_ids env,false,None,[]), []) params)
+	    ({ids = extract_ids env; unb = false;
+	      tmp_scope = None; scopes = []; impls = impl_env}, []) params in (lenv.impls, bl)
 
 let interp_rawcontext_gen understand_type understand_judgment env bl =
   let (env, par, _, impls) =
@@ -1607,7 +1658,7 @@ let interp_rawcontext_gen understand_type understand_judgment env bl =
       (fun (env,params,n,impls) (na, k, b, t) ->
 	match b with
 	    None ->
-	      let t' = locate_if_isevar (loc_of_rawconstr t) na t in
+	      let t' = locate_if_isevar (loc_of_glob_constr t) na t in
 	      let t = understand_type env t' in
 	      let d = (na,None,t) in
 	      let impls =
@@ -1624,15 +1675,15 @@ let interp_rawcontext_gen understand_type understand_judgment env bl =
       (env,[],1,[]) (List.rev bl)
   in (env, par), impls
 
-let interp_context_gen understand_type understand_judgment ?(global_level=false) sigma env params =
-  let bl = intern_context global_level sigma env params in
-    interp_rawcontext_gen understand_type understand_judgment env bl
+let interp_context_gen understand_type understand_judgment ?(global_level=false) ?(impl_env=empty_internalization_env) sigma env params =
+  let int_env,bl = intern_context global_level sigma env impl_env params in
+    int_env, interp_rawcontext_gen understand_type understand_judgment env bl
 
-let interp_context ?(global_level=false) sigma env params =
-  interp_context_gen (Default.understand_type sigma) 
-    (Default.understand_judgment sigma) ~global_level sigma env params
+let interp_context ?(global_level=false) ?(impl_env=empty_internalization_env) sigma env params =
+  interp_context_gen (Default.understand_type sigma)
+    (Default.understand_judgment sigma) ~global_level ~impl_env sigma env params
 
-let interp_context_evars ?(global_level=false) evdref env params =
+let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) evdref env params =
   interp_context_gen (fun env t -> Default.understand_tcc_evars evdref env IsType t)
-    (Default.understand_judgment_tcc evdref) ~global_level !evdref env params
-    
+    (Default.understand_judgment_tcc evdref) ~global_level ~impl_env !evdref env params
+