Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 561 insertions, 344 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index e1ee5486..9abee4d4 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -6,11 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrintern.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
+(* $Id: constrintern.ml 11065 2008-06-06 22:39:43Z msozeau $ *)
 
 open Pp
 open Util
-open Options
+open Flags
 open Names
 open Nameops
 open Libnames
@@ -32,6 +32,8 @@ type var_internalisation_data =
 type implicits_env = (identifier * var_internalisation_data) list
 type full_implicits_env = identifier list * implicits_env
 
+type raw_binder = (name * binding_kind * rawconstr option * rawconstr)
+
 let interning_grammar = ref false
 
 (* Historically for parsing grammar rules, but in fact used only for
@@ -42,8 +44,6 @@ let for_grammar f x =
     interning_grammar := false;
     a
 
-let variables_bind = ref false
-
 (**********************************************************************)
 (* Internalisation errors                                             *)
 
@@ -86,7 +86,7 @@ let explain_bad_patterns_number n1 n2 =
 
 let explain_bad_explicitation_number n po =
   match n with
-  | ExplByPos n ->
+  | ExplByPos (n,_id) ->
       let s = match po with
 	| None -> str "a regular argument"
 	| Some p -> int p in
@@ -142,15 +142,110 @@ let coqdoc_unfreeze (lt,tn,lp) =
   token_number := tn;
   last_pos := lp
 
-let add_glob loc ref = 
-  let sp = Nametab.sp_of_global ref in
-  let lib_dp = Lib.library_part ref in
+open Decl_kinds
+
+let type_of_logical_kind = function
+  | IsDefinition def -> 
+      (match def with
+      | Definition -> "def"
+      | Coercion -> "coe"
+      | SubClass -> "subclass"
+      | CanonicalStructure -> "canonstruc"
+      | Example -> "ex"
+      | Fixpoint -> "def"
+      | CoFixpoint -> "def"
+      | Scheme -> "scheme"
+      | StructureComponent -> "proj"
+      | IdentityCoercion -> "coe"
+      | Instance -> "inst"
+      | Method -> "meth")
+  | IsAssumption a ->
+      (match a with
+      | Definitional -> "defax"
+      | Logical -> "prfax"
+      | Conjectural -> "prfax")
+  | IsProof th ->
+      (match th with
+      | Theorem
+      | Lemma
+      | Fact
+      | Remark
+      | Property
+      | Proposition
+      | Corollary -> "thm")
+
+let type_of_global_ref gr =
+  if Typeclasses.is_class gr then
+    "class"
+  else
+    match gr with
+    | ConstRef cst -> 
+	type_of_logical_kind (Decls.constant_kind cst)
+    | VarRef v ->
+	"var" ^ type_of_logical_kind (Decls.variable_kind v)
+    | IndRef ind ->
+	let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in
+	  if mib.Declarations.mind_record then
+	    if mib.Declarations.mind_finite then "rec"
+	    else "corec"
+	  else if mib.Declarations.mind_finite then "ind"
+	  else "coind"
+    | ConstructRef _ -> "constr"
+
+let remove_sections dir =
+  if is_dirpath_prefix_of dir (Lib.cwd ()) then
+    (* Not yet (fully) discharged *)
+    extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ())
+  else
+    (* Theorem/Lemma outside its outer section of definition *)
+    dir
+
+let dump_reference loc filepath modpath ident ty =
+  dump_string (Printf.sprintf "R%d %s %s %s %s\n" 
+		  (fst (unloc loc)) filepath modpath ident ty)
+
+let add_glob_gen loc sp lib_dp ty =
   let mod_dp,id = repr_path sp in
-  let mod_dp_trunc =  drop_dirpath_prefix lib_dp mod_dp in
+  let mod_dp = remove_sections mod_dp in
+  let mod_dp_trunc = drop_dirpath_prefix lib_dp mod_dp in
   let filepath = string_of_dirpath lib_dp in
-  let fullname = string_of_qualid (make_qualid mod_dp_trunc id) in
-    dump_string (Printf.sprintf "R%d %s %s\n" (fst (unloc loc)) filepath fullname)
+  let modpath = string_of_dirpath mod_dp_trunc in
+  let ident = string_of_id id in
+    dump_reference loc filepath modpath ident ty
 
+let add_glob loc ref = 
+  let sp = Nametab.sp_of_global ref in
+  let lib_dp = Lib.library_part ref in
+  let ty = type_of_global_ref ref in
+    add_glob_gen loc sp lib_dp ty
+      
+let add_glob loc ref =
+  if !Flags.dump && loc <> dummy_loc then add_glob loc ref
+
+let mp_of_kn kn = 
+  let mp,sec,l = repr_kn kn in 
+    MPdot (mp,l) 
+
+let add_glob_kn loc kn =
+  let sp = Nametab.sp_of_syntactic_definition kn in
+  let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in
+    add_glob_gen loc sp lib_dp "syndef"
+
+let add_glob_kn loc ref =
+  if !Flags.dump && loc <> dummy_loc then add_glob_kn loc ref
+
+let add_local loc id = ()
+(*   let mod_dp,id = repr_path sp in *)
+(*   let mod_dp = remove_sections mod_dp in *)
+(*   let mod_dp_trunc = drop_dirpath_prefix lib_dp mod_dp in *)
+(*   let filepath = string_of_dirpath lib_dp in *)
+(*   let modpath = string_of_dirpath mod_dp_trunc in *)
+(*   let ident = string_of_id id in *)
+(*     dump_string (Printf.sprintf "R%d %s %s %s %s\n"  *)
+(* 		    (fst (unloc loc)) filepath modpath ident ty) *)
+
+let dump_binding loc id = ()
+      
 let loc_of_notation f loc args ntn =
   if args=[] or ntn.[0] <> '_' then fst (unloc loc)
   else snd (unloc (f (List.hd args)))
@@ -169,8 +264,8 @@ let dump_notation_location pos ((path,df),sc) =
   let loc = next (pos >= !last_pos) in
     last_pos := pos;
     let path = string_of_dirpath path in
-    let sc = match sc with Some sc -> " "^sc | None -> "" in
-      dump_string (Printf.sprintf "R%d %s \"%s\"%s\n" (fst (unloc loc)) path df sc)
+    let _sc = match sc with Some sc -> " "^sc | None -> "" in
+      dump_string (Printf.sprintf "R%d %s \"%s\" not\n" (fst (unloc loc)) path df)
 
 (**********************************************************************)
 (* Contracting "{ _ }" in notations *)
@@ -221,12 +316,12 @@ let contract_pat_notation ntn l =
 (**********************************************************************)
 (* Remembering the parsing scope of variables in notations            *)
 
-let make_current_scope (tmp_scope,scopes) = option_cons tmp_scope scopes
+let make_current_scope (tmp_scope,scopes) = Option.List.cons tmp_scope scopes
 
 let set_var_scope loc id (_,scopt,scopes) varscopes =
   let idscopes = List.assoc id varscopes in
   if !idscopes <> None & 
-    make_current_scope (out_some !idscopes)
+    make_current_scope (Option.get !idscopes)
     <> make_current_scope (scopt,scopes) then
       user_err_loc (loc,"set_var_scope",
       pr_id id ++ str " already occurs in a different scope")
@@ -234,6 +329,92 @@ let set_var_scope loc id (_,scopt,scopes) varscopes =
     idscopes := Some (scopt,scopes)
 
 (**********************************************************************)
+(* Syntax extensions                                                  *)
+
+let traverse_binder subst (renaming,(ids,tmpsc,scopes as env)) id =
+  try
+    (* Binders bound in the notation are considered first-order objects *)
+    let _,id' = coerce_to_id (fst (List.assoc id subst)) in
+    (renaming,(Idset.add id' ids,tmpsc,scopes)), id'
+  with Not_found ->
+    (* Binders not bound in the notation do not capture variables *)
+    (* outside the notation (i.e. in the substitution) *)
+    let fvs1 = List.map (fun (_,(c,_)) -> free_vars_of_constr_expr c) subst in
+    let fvs2 = List.map snd renaming in
+    let fvs = List.flatten (List.map Idset.elements fvs1) @ fvs2 in
+    let id' = next_ident_away id fvs in
+    let renaming' = if id=id' then renaming else (id,id')::renaming in
+    (renaming',env), id'
+
+let decode_constrlist_value = function
+  | CAppExpl (_,_,l) -> l
+  | _ -> anomaly "Ill-formed list argument of notation"
+
+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
+
+let rec subst_aconstr_in_rawconstr loc interp subst (renaming,(ids,_,scopes)) =
+  function
+  | AVar id ->
+      begin
+	(* subst remembers the delimiters stack in the interpretation *)
+	(* of the notations *)
+	try 
+	  let (a,(scopt,subscopes)) = List.assoc id subst in
+	  interp (ids,scopt,subscopes@scopes) a
+	with Not_found -> 
+	try 
+	  RVar (loc,List.assoc id renaming)
+	with Not_found -> 
+	  (* Happens for local notation joint with inductive/fixpoint defs *)
+	  RVar (loc,id)
+      end
+  | AList (x,_,iter,terminator,lassoc) ->
+      (try 
+        (* All elements of the list are in scopes (scopt,subscopes) *)
+	let (a,(scopt,subscopes)) = List.assoc x subst in
+        let termin = 
+          subst_aconstr_in_rawconstr loc interp subst 
+	    (renaming,(ids,None,scopes)) terminator in
+        let l = decode_constrlist_value a in
+	List.fold_right (fun a t -> 
+          subst_iterator ldots_var t
+            (subst_aconstr_in_rawconstr loc interp 
+              ((x,(a,(scopt,subscopes)))::subst)
+	      (renaming,(ids,None,scopes)) iter))
+            (if lassoc then List.rev l else l) termin
+      with Not_found -> 
+          anomaly "Inconsistent substitution of recursive notation")
+  | t ->
+      rawconstr_of_aconstr_with_binders loc (traverse_binder subst)
+      (subst_aconstr_in_rawconstr loc interp subst)
+      (renaming,(ids,None,scopes)) t
+
+let intern_notation intern (_,tmp_scope,scopes as env) loc ntn args =
+  let ntn,args = contract_notation ntn args in
+  let ((ids,c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
+  if !dump then dump_notation_location (ntn_loc loc args ntn) df;
+  let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
+  subst_aconstr_in_rawconstr loc intern subst ([],env) c
+
+let set_type_scope (ids,tmp_scope,scopes) =
+  (ids,Some Notation.type_scope,scopes)
+
+let reset_tmp_scope (ids,tmp_scope,scopes) =
+  (ids,None,scopes)
+
+let rec it_mkRProd env body =
+  match env with
+      (na, bk, _, t) :: tl -> it_mkRProd tl (RProd (dummy_loc, na, bk, t, body))
+    | [] -> body
+
+let rec it_mkRLambda env body =
+  match env with
+      (na, bk, _, t) :: tl -> it_mkRLambda tl (RLambda (dummy_loc, na, bk, t, body))
+    | [] -> body
+
+(**********************************************************************)
 (* Discriminating between bound variables and global references       *)
 
 (* [vars1] is a set of name to avoid (used for the tactic language);
@@ -281,52 +462,60 @@ let find_appl_head_data (_,_,_,(_,impls)) = function
   | RRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[]
   | x -> x,[],[],[]
 
+let error_not_enough_arguments loc =
+  user_err_loc (loc,"",str "Abbreviation is not applied enough")
+
+let check_no_explicitation l =
+  let l = List.filter (fun (a,b) -> b <> None) l in
+  if l <> [] then
+    let loc = fst (Option.get (snd (List.hd l))) in
+    user_err_loc
+      (loc,"",str"Unexpected explicitation of the argument of an abbreviation")
+
 (* Is it a global reference or a syntactic definition? *)
-let intern_qualid loc qid =
+let intern_qualid loc qid intern env args =
   try match Nametab.extended_locate qid with
   | TrueGlobal ref ->
-      if !dump then add_glob loc ref;
-      RRef (loc, ref)
+      add_glob loc ref;
+      RRef (loc, ref), args
   | SyntacticDef sp ->
-      Syntax_def.search_syntactic_definition loc sp
+      add_glob_kn loc sp;
+      let (ids,c) = Syntax_def.search_syntactic_definition loc sp in
+      let nids = List.length ids in
+      if List.length args < nids then error_not_enough_arguments loc;
+      let args1,args2 = list_chop nids args in
+      check_no_explicitation args1;
+      let subst = List.map2 (fun (id,scl) a -> (id,(fst a,scl))) ids args1 in
+      subst_aconstr_in_rawconstr loc intern subst ([],env) c, args2
   with Not_found ->
     error_global_not_found_loc loc qid
 
 (* Rule out section vars since these should have been found by intern_var *)
-let intern_non_secvar_qualid loc qid =
-  match intern_qualid loc qid with
-    | RRef (loc, VarRef id) -> error_global_not_found_loc loc qid
+let intern_non_secvar_qualid loc qid intern env args =
+  match intern_qualid loc qid intern env args with
+    | RRef (loc, VarRef id),_ -> error_global_not_found_loc loc qid
     | r -> r
 
-let intern_inductive r =
-  let loc,qid = qualid_of_reference r in
-  try match Nametab.extended_locate qid with
-  | TrueGlobal (IndRef ind) -> ind, []
-  | TrueGlobal _ -> raise Not_found
-  | SyntacticDef sp ->
-      (match Syntax_def.search_syntactic_definition loc sp with
-	| RApp (_,RRef(_,IndRef ind),l)
-	    when List.for_all (function RHole _ -> true | _ -> false) l ->
-	    (ind, List.map (fun _ -> Anonymous) l)
-	| _ -> raise Not_found)
-  with Not_found ->
-    error_global_not_found_loc loc qid
-
-let intern_reference env lvar = function
+let intern_applied_reference intern env lvar args = function
   | Qualid (loc, qid) ->
-      find_appl_head_data lvar (intern_qualid loc qid)
+      let r,args2 = intern_qualid loc qid intern env args in
+      find_appl_head_data lvar r, args2
   | Ident (loc, id) ->
-      try intern_var env lvar loc id
+      try intern_var env lvar loc id, args
       with Not_found -> 
       let qid = make_short_qualid id in
-      try find_appl_head_data lvar (intern_non_secvar_qualid loc qid)
+      try
+	let r,args2 = intern_non_secvar_qualid loc qid intern env args in
+	find_appl_head_data lvar r, args2
       with e ->
 	(* Extra allowance for non globalizing functions *)
-	if !interning_grammar then RVar (loc,id), [], [], []
+	if !interning_grammar then (RVar (loc,id), [], [], []),args
 	else raise e
 
 let interp_reference vars r =
-  let r,_,_,_ = intern_reference (Idset.empty,None,[]) (vars,[],[],([],[])) r 
+  let (r,_,_,_),_ =
+    intern_applied_reference (fun _ -> error_not_enough_arguments dummy_loc)
+      (Idset.empty,None,[]) (vars,[],[],([],[])) [] r
   in r
 
 let apply_scope_env (ids,_,scopes) = function
@@ -339,10 +528,16 @@ let rec adjust_scopes env scopes = function
       let (enva,scopes) = apply_scope_env env scopes in
       enva :: adjust_scopes env scopes args
 
-let rec simple_adjust_scopes = function
-  | _,[] -> []
-  | [],_::args -> None :: simple_adjust_scopes ([],args)
-  | sc::scopes,_::args -> sc :: simple_adjust_scopes (scopes,args)
+let rec simple_adjust_scopes n = function
+  | [] -> if n=0 then [] else None :: simple_adjust_scopes (n-1) []
+  | sc::scopes -> sc :: simple_adjust_scopes (n-1) scopes
+
+let find_remaining_constructor_scopes pl1 pl2 (ind,j as cstr) =
+  let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
+  let npar = mib.Declarations.mind_nparams in
+  snd (list_chop (List.length pl1 + npar)
+    (simple_adjust_scopes (npar + List.length pl2)
+      (find_arguments_scope (ConstructRef cstr))))
 
 (**********************************************************************)
 (* Cases                                                              *)
@@ -368,8 +563,7 @@ let rec has_duplicate = function
   | x::l -> if List.mem x l then (Some x) else has_duplicate l
 
 let loc_of_lhs lhs = 
- join_loc (cases_pattern_expr_loc (List.hd (List.hd lhs)))
-          (cases_pattern_expr_loc (list_last (list_last lhs)))
+ join_loc (fst (List.hd lhs)) (fst (list_last lhs))
 
 let check_linearity lhs ids =
   match has_duplicate ids with
@@ -412,6 +606,16 @@ let message_redundant_alias (id1,id2) =
 
 (* Expanding notations *)
 
+let error_invalid_pattern_notation loc =
+  user_err_loc (loc,"",str "Invalid notation for pattern")
+
+let chop_aconstr_constructor loc (ind,k) args =
+  let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
+  let params,args = list_chop nparams args in
+  List.iter (function AHole _ -> ()
+    | _ -> error_invalid_pattern_notation loc) params;
+  args
+
 let decode_patlist_value = function
   | CPatCstr (_,_,l) -> l
   | _ -> anomaly "Ill-formed list argument of notation"
@@ -445,13 +649,12 @@ let subst_cases_pattern loc alias intern subst scopes a =
       end
   | ARef (ConstructRef c) ->
       ([],[[], PatCstr (loc,c, [], alias)])
-  | AApp (ARef (ConstructRef (ind,_ as c)),args) ->
-      let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
-      let _,args = list_chop nparams args in
+  | AApp (ARef (ConstructRef cstr),args) ->
+      let args = chop_aconstr_constructor loc cstr args in
       let idslpll = List.map (aux Anonymous subst) args in
       let ids',pll = product_of_cases_patterns [] idslpll in
       let pl' = List.map (fun (subst,pl) -> 
-        subst,PatCstr (loc,c,pl,alias)) pll in
+        subst,PatCstr (loc,cstr,pl,alias)) pll in
 	ids', pl'
   | AList (x,_,iter,terminator,lassoc) ->
       (try 
@@ -469,65 +672,57 @@ let subst_cases_pattern loc alias intern subst scopes a =
 	  match pl with PatCstr (loc, c, pl, Anonymous) -> (subst, PatCstr (loc, c, pl, alias)) | _ -> x) v
       with Not_found -> 
           anomaly "Inconsistent substitution of recursive notation")
-  | t -> user_err_loc (loc,"",str "Invalid notation for pattern")
+  | t -> error_invalid_pattern_notation loc
   in aux alias subst a
     
 (* Differentiating between constructors and matching variables *)
 type pattern_qualid_kind =
-  | ConstrPat of (constructor * cases_pattern list)
+  | ConstrPat of constructor * (identifier list * 
+      ((identifier * identifier) list * cases_pattern) list) list
   | VarPat of identifier
 
-let rec patt_of_rawterm loc cstr =
-  match cstr with
-    | RRef (_,(ConstructRef c as x)) ->
-	if !dump then add_glob loc x; 
- 	(c,[])
-    | RApp (_,RApp(_,h,l1),l2) -> patt_of_rawterm loc (RApp(loc,h,l1@l2))
-    | RApp (_,RRef(_,(ConstructRef c as x)),pl) ->
-        if !dump then add_glob loc x;
-        let (mib,_) = Inductive.lookup_mind_specif (Global.env()) (fst c) in
-        let npar = mib.Declarations.mind_nparams in
-        let (params,args) =
-          if List.length pl <= npar then (pl,[]) else
-            list_chop npar pl in
-        (* All parameters must be _ *)
-        List.iter
-          (function RHole _ -> ()
-            | _ -> raise Not_found) params;
-        let pl' = List.map
-          (fun c ->
-            let (c,pl) = patt_of_rawterm loc c in
-            PatCstr(loc,c,pl,Anonymous)) args in
-        (c,pl')
-    | _ -> raise Not_found
-
-let find_constructor ref =
+let find_constructor ref f aliases pats scopes =
   let (loc,qid) = qualid_of_reference ref in
   let gref =
     try extended_locate qid
-    with Not_found ->
-      raise (InternalisationError (loc,NotAConstructor ref)) in
-    match gref with
-      | SyntacticDef sp ->
-          let sdef = Syntax_def.search_syntactic_definition loc sp in
-            patt_of_rawterm loc sdef
-      | TrueGlobal r ->
-          let rec unf = function
-            | ConstRef cst ->
-		let v = Environ.constant_value (Global.env()) cst in
-		  unf (global_of_constr v)
-            | ConstructRef c -> 
-		if !dump then add_glob loc r; 
-		c, []
-            | _ -> raise Not_found
-          in unf r
+    with Not_found -> raise (InternalisationError (loc,NotAConstructor ref)) in
+  match gref with
+  | SyntacticDef sp ->
+      let (vars,a) = Syntax_def.search_syntactic_definition loc sp in
+      (match a with
+       | ARef (ConstructRef cstr) ->
+	   assert (vars=[]);
+	   cstr, [], pats
+       | AApp (ARef (ConstructRef cstr),args) ->
+	   let args = chop_aconstr_constructor loc cstr args in
+	   let nvars = List.length vars in
+	   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 (alias_of aliases) f subst scopes) args in
+	   cstr, idspl1, pats2
+       | _ -> raise Not_found)
+      
+  | TrueGlobal r ->
+      let rec unf = function
+        | ConstRef cst ->
+	    let v = Environ.constant_value (Global.env()) cst in
+	    unf (global_of_constr v)
+        | ConstructRef cstr -> 
+	    add_glob loc r; 
+	    cstr, [], pats
+        | _ -> raise Not_found
+      in unf r
 
 let find_pattern_variable = function
   | Ident (loc,id) -> id
   | Qualid (loc,_) as x -> raise (InternalisationError(loc,NotAConstructor x))
 
-let maybe_constructor ref =
-  try ConstrPat (find_constructor ref)
+let maybe_constructor ref f aliases scopes =
+  try
+    let c,idspl1,pl2 = find_constructor ref f aliases [] scopes in
+    assert (pl2 = []);
+    ConstrPat (c,idspl1)
   with
       (* patt var does not exists globally *)
     | InternalisationError _ -> VarPat (find_pattern_variable ref)
@@ -537,39 +732,37 @@ let maybe_constructor ref =
               str " is understood as a pattern variable");
         VarPat (find_pattern_variable ref)
 
-let mustbe_constructor loc ref = 
-  try find_constructor ref
+let mustbe_constructor loc ref f aliases patl scopes = 
+  try find_constructor ref f aliases patl scopes
   with (Environ.NotEvaluableConst _ | Not_found) ->
     raise (InternalisationError (loc,NotAConstructor ref))
 
-let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope = 
-  function
+let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope pat =
+  let intern_pat = intern_cases_pattern genv in 
+  match pat with
   | CPatAlias (loc, p, id) ->
       let aliases' = merge_aliases aliases id in
-      intern_cases_pattern genv scopes aliases' tmp_scope p
+      intern_pat scopes aliases' tmp_scope p
   | CPatCstr (loc, head, pl) ->
-      let c,pl0 = mustbe_constructor loc head in
-      let argscs =
-	simple_adjust_scopes (find_arguments_scope (ConstructRef c), pl) in
-      check_constructor_length genv loc c pl0 pl;
-      let idslpl =
-	List.map2 (intern_cases_pattern genv scopes ([],[])) argscs pl in
-      let (ids',pll) = product_of_cases_patterns ids idslpl in
+      let c,idslpl1,pl2 = mustbe_constructor loc head intern_pat aliases pl scopes 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 (ids',pll) = product_of_cases_patterns ids (idslpl1@idslpl2) in
       let pl' = List.map (fun (subst,pl) ->
-        (subst, PatCstr (loc,c,pl0@pl,alias_of aliases))) pll in
+        (subst, PatCstr (loc,c,pl,alias_of aliases))) pll in
       ids',pl'
   | CPatNotation (loc,"- _",[CPatPrim(_,Numeral p)]) 
       when Bigint.is_strictly_pos p ->
-      let np = Numeral (Bigint.neg p) in
-      intern_cases_pattern genv scopes aliases tmp_scope (CPatPrim(loc,np))
+      intern_pat scopes aliases tmp_scope (CPatPrim(loc,Numeral(Bigint.neg p)))
   | CPatNotation (_,"( _ )",[a]) ->
-      intern_cases_pattern genv scopes aliases tmp_scope a
+      intern_pat scopes aliases tmp_scope a
   | CPatNotation (loc, ntn, args) ->
       let ntn,args = contract_pat_notation ntn args in
       let ((ids',c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
       if !dump then dump_notation_location (patntn_loc loc args ntn) df;
       let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in
-      let ids'',pl = subst_cases_pattern loc (alias_of aliases) (intern_cases_pattern genv) subst scopes 
+      let ids'',pl = subst_cases_pattern loc (alias_of aliases) intern_pat subst scopes 
 	c
       in ids@ids'', pl
   | CPatPrim (loc, p) ->
@@ -579,13 +772,14 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope =
       if !dump then dump_notation_location (fst (unloc loc)) df;
       (ids,[subst,c])
   | CPatDelimiters (loc, key, e) ->
-      intern_cases_pattern genv (find_delimiters_scope loc key::scopes)
-        aliases None e
+      intern_pat (find_delimiters_scope loc key::scopes) aliases None e
   | CPatAtom (loc, Some head) ->
-      (match maybe_constructor head with
-	 | ConstrPat (c,args) ->
-	     check_constructor_length genv loc c [] [];
-	     (ids,[subst, PatCstr (loc,c,args,alias_of aliases)])
+      (match maybe_constructor head intern_pat aliases scopes with
+	 | ConstrPat (c,idspl) ->
+	     check_constructor_length genv loc c idspl [];
+	     let (ids',pll) = product_of_cases_patterns ids idspl in
+	     (ids,List.map (fun (subst,pl) ->
+	       (subst, PatCstr (loc,c,pl,alias_of aliases))) pll)
 	 | VarPat id ->
 	     let ids,subst = merge_aliases aliases id in
 	     (ids,[subst, PatVar (loc,alias_of (ids,subst))]))
@@ -593,8 +787,7 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope =
       (ids,[subst, PatVar (loc,alias_of aliases)])
   | CPatOr (loc, pl) ->
       assert (pl <> []);
-      let pl' = 
-	List.map (intern_cases_pattern genv scopes aliases tmp_scope) pl in
+      let pl' = List.map (intern_pat scopes aliases tmp_scope) pl in
       let (idsl,pl') = List.split pl' in
       let ids = List.hd idsl in
       check_or_pat_variables loc ids (List.tl idsl);
@@ -632,6 +825,44 @@ let push_name_env lvar (ids,tmpsc,scopes as env) = function
       check_hidden_implicit_parameters id lvar;
       (Idset.add id ids,tmpsc,scopes)
 
+let push_loc_name_env lvar (ids,tmpsc,scopes as env) loc = function
+  | Anonymous -> env 
+  | Name id -> 
+      check_hidden_implicit_parameters id lvar;
+      dump_binding loc id;
+      (Idset.add id ids,tmpsc,scopes)
+
+let intern_typeclass_binders intern_type lvar env bl =
+  List.fold_left 
+    (fun ((ids,ts,sc) as env,bl) ((loc, na), bk, ty) ->
+      let env = push_loc_name_env lvar env loc na in
+      let ty = locate_if_isevar loc na (intern_type env ty) in
+	(env, (na,bk,None,ty)::bl))
+    env bl
+
+let intern_typeclass_binder intern_type lvar (env,bl) na b ty =
+  let ctx = (na, b, ty) in
+  let (fvs, bind) = Implicit_quantifiers.generalize_class_binders_raw (pi1 env) [ctx] in
+  let env, ifvs = intern_typeclass_binders intern_type lvar (env,bl) fvs in
+    intern_typeclass_binders intern_type lvar (env,ifvs) bind
+    
+let intern_local_binder_aux intern intern_type lvar ((ids,ts,sc as env),bl) = function
+  | LocalRawAssum(nal,bk,ty) ->
+      (match bk with
+	| Default k ->
+	    let (loc,na) = List.hd nal in
+	      (* TODO: fail if several names with different implicit types *)
+	    let ty = locate_if_isevar loc na (intern_type env ty) in
+	      List.fold_left
+		(fun ((ids,ts,sc),bl) (_,na) ->
+		  ((name_fold Idset.add na ids,ts,sc), (na,k,None,ty)::bl))
+		(env,bl) nal
+	| TypeClass b ->
+	    intern_typeclass_binder intern_type lvar (env,bl) (List.hd nal) b ty)
+  | LocalRawDef((loc,na),def) ->
+      ((name_fold Idset.add na ids,ts,sc),
+      (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
+
 (**********************************************************************)
 (* Utilities for application                                          *)
 
@@ -683,7 +914,7 @@ let extract_explicit_arg imps args =
 		user_err_loc (loc,"",str "Argument name " ++ pr_id id
 		++ str " occurs more than once");
 	      id
-	  | ExplByPos p ->
+	  | ExplByPos (p,_id) ->
 	      let id =
 		try 
 		  let imp = List.nth imps (p-1) in
@@ -700,120 +931,53 @@ let extract_explicit_arg imps args =
   in aux args
 
 (**********************************************************************)
-(* Syntax extensions                                                  *)
-
-let traverse_binder subst (renaming,(ids,tmpsc,scopes as env)) id =
-  try
-    (* Binders bound in the notation are considered first-order objects *)
-    let _,id' = coerce_to_id (fst (List.assoc id subst)) in
-    (renaming,(Idset.add id' ids,tmpsc,scopes)), id'
-  with Not_found ->
-    (* Binders not bound in the notation do not capture variables *)
-    (* outside the notation (i.e. in the substitution) *)
-    let fvs1 = List.map (fun (_,(c,_)) -> free_vars_of_constr_expr c) subst in
-    let fvs2 = List.map snd renaming in
-    let fvs = List.flatten (List.map Idset.elements fvs1) @ fvs2 in
-    let id' = next_ident_away id fvs in
-    let renaming' = if id=id' then renaming else (id,id')::renaming in
-    (renaming',env), id'
-
-let decode_constrlist_value = function
-  | CAppExpl (_,_,l) -> l
-  | _ -> anomaly "Ill-formed list argument of notation"
-
-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
-
-let rec subst_aconstr_in_rawconstr loc interp subst (renaming,(ids,_,scopes)) =
-  function
-  | AVar id ->
-      begin
-	(* subst remembers the delimiters stack in the interpretation *)
-	(* of the notations *)
-	try 
-	  let (a,(scopt,subscopes)) = List.assoc id subst in
-	  interp (ids,scopt,subscopes@scopes) a
-	with Not_found -> 
-	try 
-	  RVar (loc,List.assoc id renaming)
-	with Not_found -> 
-	  (* Happens for local notation joint with inductive/fixpoint defs *)
-	  RVar (loc,id)
-      end
-  | AList (x,_,iter,terminator,lassoc) ->
-      (try 
-        (* All elements of the list are in scopes (scopt,subscopes) *)
-	let (a,(scopt,subscopes)) = List.assoc x subst in
-        let termin = 
-          subst_aconstr_in_rawconstr loc interp subst 
-	    (renaming,(ids,None,scopes)) terminator in
-        let l = decode_constrlist_value a in
-	List.fold_right (fun a t -> 
-          subst_iterator ldots_var t
-            (subst_aconstr_in_rawconstr loc interp 
-              ((x,(a,(scopt,subscopes)))::subst)
-	      (renaming,(ids,None,scopes)) iter))
-            (if lassoc then List.rev l else l) termin
-      with Not_found -> 
-          anomaly "Inconsistent substitution of recursive notation")
-  | t ->
-      rawconstr_of_aconstr_with_binders loc (traverse_binder subst)
-      (subst_aconstr_in_rawconstr loc interp subst)
-      (renaming,(ids,None,scopes)) t
-
-let intern_notation intern (_,tmp_scope,scopes as env) loc ntn args =
-  let ntn,args = contract_notation ntn args in
-  let ((ids,c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
-  if !dump then dump_notation_location (ntn_loc loc args ntn) df;
-  let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
-  subst_aconstr_in_rawconstr loc intern subst ([],env) c
-
-let set_type_scope (ids,tmp_scope,scopes) =
-  (ids,Some Notation.type_scope,scopes)
-
-let reset_tmp_scope (ids,tmp_scope,scopes) =
-  (ids,None,scopes)
-
-(**********************************************************************)
 (* Main loop                                                          *)
 
-let internalise sigma globalenv env allow_soapp lvar c =
+let internalise sigma globalenv env allow_patvar lvar c =
   let rec intern (ids,tmp_scope,scopes as env) = function
     | CRef ref as x ->
-	let (c,imp,subscopes,l) = intern_reference env lvar ref in
+	let (c,imp,subscopes,l),_ =
+	  intern_applied_reference intern env lvar [] ref in
 	(match intern_impargs c env imp subscopes l with
           | [] -> c
           | l -> RApp (constr_loc x, c, l))
     | CFix (loc, (locid,iddef), dl) ->
-        let lf = List.map (fun (id,_,_,_,_) -> id) dl in
+        let lf = List.map (fun ((_, id),_,_,_,_) -> id) dl in
         let dl = Array.of_list dl in
 	let n =
-	  try
-	    (list_index iddef lf) -1
+	  try list_index0 iddef lf
           with Not_found ->
 	    raise (InternalisationError (locid,UnboundFixName (false,iddef)))
 	in
         let idl = Array.map
           (fun (id,(n,order),bl,ty,bd) ->
 	     let intern_ro_arg c f =
-	       let before, after = list_chop (succ (out_some n)) bl in
-	       let ((ids',_,_),rafter) =
-		 List.fold_left intern_local_binder (env,[]) after in
-	       let ro = (intern (ids', tmp_scope, scopes) c) in
-		 f ro, List.fold_left intern_local_binder (env,rafter) before
+	       let idx = 
+		 match n with
+		     Some (loc, n) -> list_index0 (Name n) (List.map snd (names_of_local_assums bl))
+		   | None -> 0
+	       in
+	       let before, after = list_chop idx bl in
+	       let ((ids',_,_) as env',rbefore) =
+		 List.fold_left intern_local_binder (env,[]) before in
+	       let ro =
+		 match c with 
+		   | None -> RStructRec 
+		   | Some c' -> f (intern (ids', tmp_scope, scopes) c') 
+	       in 
+	       let n' = Option.map (fun _ -> List.length before) n in
+		 n', ro, List.fold_left intern_local_binder (env',rbefore) after
 	     in
-	     let ro, ((ids',_,_),rbl) =
+	     let n, ro, ((ids',_,_),rbl) =
 	       (match order with
-		    CStructRec -> 
-		      RStructRec,
-		      List.fold_left intern_local_binder (env,[]) bl
-		  | CWfRec c ->
-		      intern_ro_arg c (fun r -> RWfRec r)
-		  | CMeasureRec c ->
-		      intern_ro_arg c (fun r -> RMeasureRec r))
-	    in
-	    let ids'' = List.fold_right Idset.add lf ids' in
+		 | CStructRec -> 
+		     intern_ro_arg None (fun _ -> RStructRec)
+		 | CWfRec c ->
+		     intern_ro_arg (Some c) (fun r -> RWfRec r)
+		 | CMeasureRec c ->
+		     intern_ro_arg (Some c) (fun r -> RMeasureRec r))
+	     in
+	     let ids'' = List.fold_right Idset.add lf ids' in
 	     ((n, ro), List.rev rbl, 
              intern_type (ids',tmp_scope,scopes) ty,
              intern (ids'',None,scopes) bd)) dl in
@@ -824,11 +988,10 @@ let internalise sigma globalenv env allow_soapp lvar c =
               Array.map (fun (_,_,ty,_) -> ty) idl,
               Array.map (fun (_,_,_,bd) -> bd) idl)
     | CCoFix (loc, (locid,iddef), dl) ->
-        let lf = List.map (fun (id,_,_,_) -> id) dl in
+        let lf = List.map (fun ((_, id),_,_,_) -> id) dl in
         let dl = Array.of_list dl in
 	let n =
-          try 
-	    (list_index iddef lf) -1
+          try list_index0 iddef lf
           with Not_found ->
 	    raise (InternalisationError (locid,UnboundFixName (true,iddef)))
 	in
@@ -846,18 +1009,18 @@ let internalise sigma globalenv env allow_soapp lvar c =
               Array.map (fun (_,ty,_) -> ty) idl,
               Array.map (fun (_,_,bd) -> bd) idl)
     | CArrow (loc,c1,c2) ->
-        RProd (loc, Anonymous, intern_type env c1, intern_type env c2)
+        RProd (loc, Anonymous, Explicit, intern_type env c1, intern_type env c2)
     | CProdN (loc,[],c2) ->
         intern_type env c2
-    | CProdN (loc,(nal,ty)::bll,c2) ->
-        iterate_prod loc env ty (CProdN (loc, bll, c2)) nal
+    | CProdN (loc,(nal,bk,ty)::bll,c2) ->
+        iterate_prod loc env bk ty (CProdN (loc, bll, c2)) nal
     | CLambdaN (loc,[],c2) ->
         intern env c2
-    | CLambdaN (loc,(nal,ty)::bll,c2) ->
-	iterate_lam loc (reset_tmp_scope env) ty (CLambdaN (loc, bll, c2)) nal
-    | CLetIn (loc,(_,na),c1,c2) ->
+    | CLambdaN (loc,(nal,bk,ty)::bll,c2) ->
+	iterate_lam loc (reset_tmp_scope env) bk ty (CLambdaN (loc, bll, c2)) nal
+    | CLetIn (loc,(loc1,na),c1,c2) ->
 	RLetIn (loc, na, intern (reset_tmp_scope env) c1,
-          intern (push_name_env lvar env na) c2)
+          intern (push_loc_name_env lvar env loc1 na) c2)
     | CNotation (loc,"- _",[CPrim (_,Numeral p)])
 	when Bigint.is_strictly_pos p -> 
 	intern env (CPrim (loc,Numeral (Bigint.neg p)))
@@ -871,22 +1034,24 @@ let internalise sigma globalenv env allow_soapp lvar c =
     | CDelimiters (loc, key, e) ->
 	intern (ids,None,find_delimiters_scope loc key::scopes) e
     | CAppExpl (loc, (isproj,ref), args) ->
-        let (f,_,args_scopes,_) = intern_reference env lvar ref in
+        let (f,_,args_scopes,_),args =
+	  let args = List.map (fun a -> (a,None)) args in
+	  intern_applied_reference intern env lvar args ref in
 	check_projection isproj (List.length args) f;
-	RApp (loc, f, intern_args env args_scopes args)
+	RApp (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" *)
           | CApp (_,(Some _,f), args') when isproj=None -> isproj,f,args'@args
           (* Don't compact "(f args') args" to resolve implicits separately *)
           | _ -> isproj,f,args in
-	let (c,impargs,args_scopes,l) =
+	let (c,impargs,args_scopes,l),args =
           match f with
-            | CRef ref -> intern_reference env lvar ref
+            | CRef ref -> intern_applied_reference intern env lvar args ref
             | CNotation (loc,ntn,[]) ->
                 let c = intern_notation intern env loc ntn [] in
-                find_appl_head_data lvar c
-            | x -> (intern env f,[],[],[]) in
+                find_appl_head_data lvar c, args
+            | x -> (intern env f,[],[],[]), args in
 	let args = 
 	  intern_impargs c env impargs args_scopes (merge_impargs l args) in
 	check_projection isproj (List.length args) c;
@@ -894,38 +1059,36 @@ let internalise sigma globalenv env allow_soapp lvar c =
           (* Now compact "(f args') args" *)
 	  | RApp (loc', f', args') -> RApp (join_loc loc' loc, f',args'@args)
 	  | _ -> RApp (loc, c, args))
-    | CCases (loc, rtnpo, tms, eqns) ->
+    | CCases (loc, sty, rtnpo, tms, eqns) ->
         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 lvar) env nal)
 	  tms ([],env) in
-        let rtnpo = option_map (intern_type env') rtnpo in
+        let rtnpo = Option.map (intern_type env') rtnpo in
         let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
-	RCases (loc, rtnpo, tms, List.flatten eqns')
+	RCases (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 env'' = List.fold_left (push_name_env lvar) env ids in
-        let p' = option_map (intern_type env'') po in
+        let p' = Option.map (intern_type env'') po in
         RLetTuple (loc, nal, (na', p'), b',
                    intern (List.fold_left (push_name_env lvar) 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 env'' = List.fold_left (push_name_env lvar) env ids in
-        let p' = option_map (intern_type env'') po in
+        let p' = Option.map (intern_type env'') po in
         RIf (loc, c', (na', p'), intern env b1, intern env b2)
-    | CHole loc -> 
-	RHole (loc, Evd.QuestionMark true)
-    | CPatVar (loc, n) when allow_soapp ->
+    | CHole (loc, k) -> 
+	RHole (loc, match k with Some k -> k | None -> Evd.QuestionMark true)
+    | CPatVar (loc, n) when allow_patvar ->
 	RPatVar (loc, n)
-    | CPatVar (loc, (false,n)) ->
-        error_unbound_patvar loc n
     | CPatVar (loc, _) ->
 	raise (InternalisationError (loc,NegativeMetavariable))
-    | CEvar (loc, n) ->
-	REvar (loc, n, None)
+    | CEvar (loc, n, l) ->
+	REvar (loc, n, Option.map (List.map (intern env)) l)
     | CSort (loc, s) ->
 	RSort(loc,s)
     | CCast (loc, c1, CastConv (k, c2)) ->
@@ -937,29 +1100,20 @@ let internalise sigma globalenv env allow_soapp lvar c =
 
   and intern_type env = intern (set_type_scope env)
 
-  and intern_local_binder ((ids,ts,sc as env),bl) = function
-    | LocalRawAssum(nal,ty) ->
-	let (loc,na) = List.hd nal in
-	(* TODO: fail if several names with different implicit types *)
-	let ty = locate_if_isevar loc na (intern_type env ty) in
-        List.fold_left
-          (fun ((ids,ts,sc),bl) (_,na) ->
-            ((name_fold Idset.add na ids,ts,sc), (na,None,ty)::bl))
-          (env,bl) nal
-    | LocalRawDef((loc,na),def) ->
-        ((name_fold Idset.add na ids,ts,sc),
-         (na,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
+  and intern_local_binder env bind = 
+    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 pl =
+  and intern_multiple_pattern scopes n (loc,pl) =
     let idsl_pll = 
       List.map (intern_cases_pattern globalenv scopes ([],[]) 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 mpl =
+  and intern_disjunctive_multiple_pattern scopes loc n mpl =
     assert (mpl <> []);
-    let mpl' = List.map (intern_multiple_pattern scopes) mpl in
+    let mpl' = List.map (intern_multiple_pattern scopes 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);
@@ -967,10 +1121,9 @@ let internalise sigma globalenv env allow_soapp lvar c =
 
   (* Expands a pattern-matching clause [lhs => rhs] *)
   and intern_eqn n (ids,tmp_scope,scopes) (loc,lhs,rhs) =
-    let eqn_ids,pll = intern_disjunctive_multiple_pattern scopes loc lhs in
+    let eqn_ids,pll = intern_disjunctive_multiple_pattern scopes loc n lhs in
     (* Linearity implies the order in ids is irrelevant *)
     check_linearity lhs eqn_ids;
-    check_number_of_pattern loc n (snd (List.hd pll));
     let env_ids = List.fold_right Idset.add eqn_ids ids in
     List.map (fun (subst,pl) ->
       let rhs = replace_vars_constr_expr subst rhs in
@@ -1008,23 +1161,40 @@ let internalise sigma globalenv env allow_soapp lvar c =
       | _, None -> Anonymous
       | _, Some na -> na in
     (tm',(na,typ)), na::ids
-
-  and iterate_prod loc2 env ty body = function
+      
+  and iterate_prod loc2 env bk ty body nal =
+    let rec default env bk = function
     | (loc1,na)::nal ->
 	if nal <> [] then check_capture loc1 ty na;
-	let body = iterate_prod loc2 (push_name_env lvar env na) ty body nal in
+	let body = default (push_loc_name_env lvar env loc1 na) bk nal in
 	let ty = locate_if_isevar loc1 na (intern_type env ty) in
-	RProd (join_loc loc1 loc2, na, ty, body)
+	  RProd (join_loc loc1 loc2, na, bk, ty, body)
     | [] -> intern_type env body
-
-  and iterate_lam loc2 env ty body = function
-    | (loc1,na)::nal ->
-	if nal <> [] then check_capture loc1 ty na;
-	let body = iterate_lam loc2 (push_name_env lvar env na) ty body nal in
-	let ty = locate_if_isevar loc1 na (intern_type env ty) in
-	RLambda (join_loc loc1 loc2, na, ty, body)
-    | [] -> intern env body
-
+    in
+      match bk with
+	| Default b -> default env b nal
+	| TypeClass b -> 
+	    let env, ibind = intern_typeclass_binder intern_type lvar
+	      (env, []) (List.hd nal) b ty in
+	    let body = intern_type env body in
+	      it_mkRProd ibind body
+					   
+  and iterate_lam loc2 env bk ty body nal = 
+    let rec default env bk = function 
+      | (loc1,na)::nal ->
+	  if nal <> [] then check_capture loc1 ty na;
+	  let body = default (push_loc_name_env lvar env loc1 na) bk nal in
+	  let ty = locate_if_isevar loc1 na (intern_type env ty) in
+	    RLambda (join_loc loc1 loc2, na, bk, ty, body)
+      | [] -> intern env body
+    in match bk with
+      | Default b -> default env b nal
+      | TypeClass b ->	  
+	  let env, ibind = intern_typeclass_binder intern_type lvar
+	    (env, []) (List.hd nal) b ty in
+	  let body = intern env body in
+	    it_mkRLambda ibind body
+	      
   and intern_impargs c env l subscopes args =
     let eargs, rargs = extract_explicit_arg l args in
     let rec aux n impl subscopes eargs rargs =
@@ -1037,10 +1207,9 @@ let internalise sigma globalenv env allow_soapp lvar c =
 	    let eargs' = List.remove_assoc id eargs in
 	    intern enva a :: aux (n+1) impl' subscopes' eargs' rargs
 	  with Not_found ->
-	  if rargs=[] & eargs=[] &
-	    not (List.for_all is_status_implicit impl') then
-	    (* Less regular arguments than expected: don't complete *)
-	    (* with implicit arguments *)
+	  if rargs=[] & eargs=[] & not (maximal_insertion_of imp) then
+            (* Less regular arguments than expected: complete *)
+            (* with implicit arguments if maximal insertion is set *)
 	    []
 	  else
 	    RHole (set_hole_implicit (n,get_implicit_name n l) c) :: 
@@ -1051,7 +1220,7 @@ let internalise sigma globalenv env allow_soapp 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));
 	  []
       | ([], rargs) ->
@@ -1082,13 +1251,13 @@ let extract_ids env =
     Idset.empty
 
 let intern_gen isarity sigma env
-               ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[]))
+               ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
                c =
   let tmp_scope = 
     if isarity then Some Notation.type_scope else None in
-  internalise sigma env (extract_ids env, tmp_scope,[])
-    allow_soapp (ltacvars,Environ.named_context env, [], impls) c
-
+    internalise sigma env (extract_ids env, tmp_scope,[])
+      allow_patvar (ltacvars,Environ.named_context env, [], impls) 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 
@@ -1104,17 +1273,36 @@ let intern_pattern env patt =
 let intern_ltac isarity ltacvars sigma env c =
   intern_gen isarity sigma env ~ltacvars:ltacvars c
 
+type manual_implicits = (explicitation * (bool * bool)) list
+
+let implicits_of_rawterm l = 
+  let rec aux i c = 
+    match c with
+	RProd (loc, na, bk, t, b) | RLambda (loc, na, bk, t, b) -> 
+	  let rest = aux (succ i) b in
+	    if bk = Implicit then
+	      let name =
+		match na with
+		    Name id -> Some id
+		  | Anonymous -> None
+	      in
+		(ExplByPos (i, name), (true, true)) :: rest
+	    else rest
+      | RLetIn (loc, na, t, b) -> aux i b
+      | _ -> []
+  in aux 1 l
+
 (*********************************************************************)
 (* Functions to parse and interpret constructions *)
 
 let interp_gen kind sigma env 
-               ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[]))
+               ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
                c =
-  Default.understand_gen kind sigma env 
-    (intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars sigma env c)
+  let c = intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars sigma env c in
+    Default.understand_gen kind sigma env c
 
 let interp_constr sigma env c =
-  interp_gen (OfType None) sigma env c 
+  interp_gen (OfType None) sigma env c
 
 let interp_type sigma env ?(impls=([],[])) c =
   interp_gen IsType sigma env ~impls c
@@ -1128,25 +1316,46 @@ let interp_open_constr sigma env c =
 let interp_constr_judgment sigma env c =
   Default.understand_judgment sigma env (intern_constr sigma env c)
 
-
-let interp_constr_evars_gen isevars env ?(impls=([],[])) kind c =
-  Default.understand_tcc_evars isevars env kind
-    (intern_gen (kind=IsType) ~impls (Evd.evars_of !isevars) env c)
-
-let interp_casted_constr_evars isevars env ?(impls=([],[])) c typ =
-  interp_constr_evars_gen isevars env ~impls (OfType (Some typ)) c
-
-let interp_type_evars isevars env ?(impls=([],[])) c =
-  interp_constr_evars_gen isevars env IsType ~impls c
-
-let interp_constr_judgment_evars isevars env c =
-  Default.understand_judgment_tcc isevars env
-    (intern_constr (Evd.evars_of !isevars) env c)
+let interp_constr_evars_gen_impls ?evdref
+    env ?(impls=([],[])) kind c =
+  match evdref with 
+    | None -> 
+	let c = intern_gen (kind=IsType) ~impls Evd.empty env c in
+	let imps = implicits_of_rawterm c in
+	  Default.understand_gen kind Evd.empty env c, imps
+    | Some evdref ->
+	let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in
+	let imps = implicits_of_rawterm c in
+	  Default.understand_tcc_evars evdref env kind c, imps
+
+let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c =
+  let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in
+    Default.understand_tcc_evars evdref env kind c
+      
+let interp_casted_constr_evars_impls ?evdref
+    env ?(impls=([],[])) c typ =
+  interp_constr_evars_gen_impls ?evdref env ~impls (OfType (Some typ)) c
+
+let interp_type_evars_impls ?evdref env ?(impls=([],[])) c =
+  interp_constr_evars_gen_impls ?evdref env IsType ~impls c
+
+let interp_constr_evars_impls ?evdref env ?(impls=([],[])) c =
+  interp_constr_evars_gen_impls ?evdref env (OfType None) ~impls c
+
+let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ =
+  interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c
+
+let interp_type_evars evdref env ?(impls=([],[])) c =
+  interp_constr_evars_gen evdref env IsType ~impls c
+
+let interp_constr_judgment_evars evdref env c =
+  Default.understand_judgment_tcc evdref env
+    (intern_constr (Evd.evars_of !evdref) env c)
 
 type ltac_sign = identifier list * unbound_ltac_var_map
 
 let interp_constrpattern sigma env c =
-  pattern_of_rawconstr (intern_gen false sigma env ~allow_soapp:true c)
+  pattern_of_rawconstr (intern_gen false sigma env ~allow_patvar:true c)
 
 let interp_aconstr impls vars a =
   let env = Global.env () in
@@ -1169,50 +1378,58 @@ let interp_binder sigma env na t =
   let t' = locate_if_isevar (loc_of_rawconstr t) na t in
   Default.understand_type sigma env t'
 
-let interp_binder_evars isevars env na t =
-  let t = intern_gen true (Evd.evars_of !isevars) env t in
+let interp_binder_evars evdref env na t =
+  let t = intern_gen true (Evd.evars_of !evdref) env t in
   let t' = locate_if_isevar (loc_of_rawconstr t) na t in
-  Default.understand_tcc_evars isevars env IsType t'
+  Default.understand_tcc_evars evdref env IsType t'
 
 open Environ
 open Term
 
-let interp_context sigma env params = 
-  List.fold_left
-    (fun (env,params) d -> match d with
-      | LocalRawAssum ([_,na],(CHole _ as t)) ->
-	  let t = interp_binder sigma env na t in
-	  let d = (na,None,t) in
-	  (push_rel d env, d::params)
-      | LocalRawAssum (nal,t) ->
-	  let t = interp_type sigma env t in
-	  let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in
-	  let ctx = List.rev ctx in
-	  (push_rel_context ctx env, ctx@params)
-      | LocalRawDef ((_,na),c) ->
-	  let c = interp_constr_judgment sigma env c in
-	  let d = (na, Some c.uj_val, c.uj_type) in
-	  (push_rel d env,d::params))
-    (env,[]) params
-
-let interp_context_evars isevars env params =
-  List.fold_left
-    (fun (env,params) d -> match d with
-      | LocalRawAssum ([_,na],(CHole _ as t)) ->
-	  let t = interp_binder_evars isevars env na t in
-	  let d = (na,None,t) in
-	  (push_rel d env, d::params)
-      | LocalRawAssum (nal,t) ->
-	  let t = interp_type_evars isevars env t in
-	  let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in
-	  let ctx = List.rev ctx in
-	  (push_rel_context ctx env, ctx@params)
-      | LocalRawDef ((_,na),c) ->
-	  let c = interp_constr_judgment_evars isevars env c in
-	  let d = (na, Some c.uj_val, c.uj_type) in
-	  (push_rel d env,d::params))
-    (env,[]) params
+let my_intern_constr sigma env lvar acc c =
+  internalise sigma env acc false lvar c
+
+let my_intern_type sigma env lvar acc c = my_intern_constr sigma env lvar (set_type_scope acc) c
+
+let intern_context sigma env params =
+  let lvar = (([],[]),Environ.named_context env, [], ([], [])) in
+    snd (List.fold_left
+	    (intern_local_binder_aux (my_intern_constr sigma env lvar) (my_intern_type sigma env lvar) lvar)
+	    ((extract_ids env,None,[]), []) params)
+
+let interp_context_gen understand_type understand_judgment env bl = 
+  let (env, par, _, impls) =
+    List.fold_left
+      (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 = understand_type env t' in
+	      let d = (na,None,t) in
+	      let impls = 
+		if k = Implicit then
+		  let na = match na with Name n -> Some n | Anonymous -> None in
+		    (ExplByPos (n, na), (true, true)) :: impls
+		else impls
+	      in
+		(push_rel d env, d::params, succ n, impls)
+	  | Some b ->
+	      let c = understand_judgment env b in
+	      let d = (na, Some c.uj_val, c.uj_type) in
+		(push_rel d env,d::params, succ n, impls))
+      (env,[],1,[]) (List.rev bl)
+  in (env, par), impls
 
+let interp_context sigma env params = 
+  let bl = intern_context sigma env params in
+    interp_context_gen (Default.understand_type sigma) 
+      (Default.understand_judgment sigma) env bl
+    
+let interp_context_evars evdref env params =
+  let bl = intern_context (Evd.evars_of !evdref) env params in
+    interp_context_gen (fun env t -> Default.understand_tcc_evars evdref env IsType t)
+      (Default.understand_judgment_tcc evdref) env bl
+    
 (**********************************************************************)
 (* Locating reference, possibly via an abbreviation *)
 
@@ -1221,7 +1438,7 @@ let locate_reference qid =
     | TrueGlobal ref -> ref
     | SyntacticDef kn -> 
 	match Syntax_def.search_syntactic_definition dummy_loc kn with
-	  | Rawterm.RRef (_,ref) -> ref
+	  | [],ARef ref -> ref
 	  | _ -> raise Not_found
 
 let is_global id =