Ajout notation c.(f) en v8 pour les projections de Record

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4128 85f007b7-540e-0410-9357-904b9bb8a0f7

11 files changed, 278 insertions, 104 deletions

diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index 888f876de..0e6b3b7d2 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -107,7 +107,7 @@ open Coqast
 let mk_id loc id = mkRefC (Ident (loc, id))
 let mk_ref loc s = mk_id loc (id_of_string s)
 let mk_appl loc1 loc2 f args =
-  CApp (join_loc loc1 loc2, mk_ref loc1 f, List.map (fun a -> a,None) args)
+  CApp (join_loc loc1 loc2, (false,mk_ref loc1 f), List.map (fun a -> a,None) args)
 
 let conj_assert {a_name=n;a_value=a} {a_value=b} = 
   let loc1 = constr_loc a in
@@ -166,7 +166,7 @@ let rec coqast_of_program loc = function
 		   (function Term t -> (coqast_of_program t.loc t.desc,None)
 		      | _ -> invalid_arg "coqast_of_program") l
       in
-      CApp (dummy_loc, f, args)
+      CApp (dummy_loc, (false,f), args)
   | Expression c -> bdize c
   | _ -> invalid_arg "coqast_of_program"
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index cfb0c4fb1..17405769a 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -55,7 +55,7 @@ let explain_variable_capture id =
   str "The variable " ++ pr_id id ++ str " occurs in its type"
 
 let explain_wrong_explicit_implicit =
-  str "Found an explicitely given implicit argument but was expecting" ++
+  str "Found an explicitly given implicit argument but was expecting" ++
   fnl () ++ str "a regular one"
 
 let explain_negative_metavariable =
@@ -122,14 +122,18 @@ let add_glob loc ref =
 (**********************************************************************)
 (* Remembering the parsing scope of variables in notations            *)
 
-let set_var_scope loc id (_,_,scopes) (_,_,varscopes) =
+let make_current_scope (scopt,scopes) = option_cons scopt scopes
+
+let set_var_scope loc id (_,_,scopt,scopes) (_,_,varscopes) =
   try 
     let idscopes = List.assoc id varscopes in
-    if !idscopes <> None & !idscopes <> Some scopes then
+    if !idscopes <> None & 
+      make_current_scope (out_some !idscopes)
+      <> make_current_scope (scopt,scopes) then
       user_err_loc (loc,"set_var_scope",
         pr_id id ++ str " already occurs in a different scope")
     else
-      idscopes := Some scopes
+      idscopes := Some (scopt,scopes)
   with Not_found ->
     if_verbose warning ("Could not globalize " ^ (string_of_id id))
 
@@ -140,7 +144,7 @@ let set_var_scope loc id (_,_,scopes) (_,_,varscopes) =
    [vars2] is the set of global variables, env is the set of variables
    abstracted until this point *)
 
-let intern_var (env,impls,scopes) ((vars1,unbndltacvars),vars2,_) loc id =
+let intern_var (env,impls,_,_) ((vars1,unbndltacvars),vars2,_) loc id =
   (* Is [id] bound in current env or ltac vars bound to constr *)
   if Idset.mem id env or List.mem id vars1
   then
@@ -197,12 +201,22 @@ let intern_reference env lvar = function
 	else raise e
 
 let interp_reference vars r =
-  let (r,_,_) = intern_reference (Idset.empty,[],[]) (vars,[],[]) r in r
+  let (r,_,_) = intern_reference (Idset.empty,[],None,[]) (vars,[],[]) r in r
+
+let apply_scope_env (ids,impls,_,scopes as env) = function
+  | [] -> (ids,impls,None,scopes), []
+  | sc::scl -> (ids,impls,sc,scopes), scl
+
+let rec adjust_scopes env scopes = function
+  | [] -> []
+  | a::args ->
+      let (enva,scopes) = apply_scope_env env scopes in
+      enva :: adjust_scopes env scopes args
 
-let apply_scope_env (ids,impls,scopes as env) = function
-  | [] -> env, []
-  | (Some sc)::scl -> (ids,impls,sc::scopes), scl
-  | None::scl -> env, scl
+let rec simple_adjust_scopes = function
+  | _,[] -> []
+  | [],_::args -> None :: simple_adjust_scopes ([],args)
+  | sc::scopes,_::args -> sc :: simple_adjust_scopes (scopes,args)
 
 (**********************************************************************)
 (* Cases                                                              *)
@@ -298,21 +312,25 @@ let maybe_constructor ref =
   try ConstrPat (find_constructor ref)
   with InternalisationError _ -> VarPat (find_pattern_variable ref)
 
-let rec intern_cases_pattern scopes aliases = function
+let rec intern_cases_pattern scopes aliases tmp_scope = function
   | CPatAlias (loc, p, id) ->
       let aliases' = merge_aliases aliases id in
-      intern_cases_pattern scopes aliases' p
+      intern_cases_pattern scopes aliases' tmp_scope p
   | CPatCstr (loc, head, pl) ->
       let c = find_constructor head in
+      let argscs =
+	simple_adjust_scopes (find_arguments_scope (ConstructRef c), pl) in
       let (idsl,pl') =
-	List.split (List.map (intern_cases_pattern scopes ([],[])) pl)
+	List.split (List.map2 (intern_cases_pattern scopes ([],[])) argscs pl)
       in
       (aliases::(List.flatten idsl), PatCstr (loc,c,pl',alias_of aliases))
   | CPatNumeral (loc, n) ->
+      let scopes = option_cons tmp_scope scopes in
       ([aliases],
       Symbols.interp_numeral_as_pattern loc n (alias_of aliases) scopes)
   | CPatDelimiters (loc, key, e) ->
-      intern_cases_pattern (find_delimiters_scope loc key::scopes) aliases e
+      intern_cases_pattern (find_delimiters_scope loc key::scopes)
+        aliases None e
   | CPatAtom (loc, Some head) ->
       (match maybe_constructor head with
 	 | ConstrPat c ->
@@ -358,6 +376,18 @@ let locate_if_isevar loc na = function
 (**********************************************************************)
 (* Utilities for application                                          *)
 
+
+let check_projection nargs = function
+  | RRef (loc, ref) ->
+      (try
+	let n = Recordops.find_projection_nparams ref in
+	if nargs <> n+1 then 
+	  user_err_loc (loc,"",str "Projection has not enough parameters");
+      with Not_found -> 
+	user_err_loc
+	(loc,"",pr_global_env Idset.empty ref ++ str " is not a registered projection"))
+  | r -> user_err_loc (loc_of_rawconstr r, "", str "Not a projection")
+
 let set_hole_implicit i = function
   | RRef (loc,r) -> (loc,ImplicitArg (r,i))
   | RVar (loc,id) -> (loc,ImplicitArg (VarRef id,i))
@@ -372,25 +402,43 @@ let coerce_to_id = function
       user_err_loc (constr_loc c, "subst_rawconstr",
         str"This expression should be a simple identifier")
 
-let traverse_binder subst id (ids,impls,scopes as env) =
+let traverse_binder subst id (ids,impls,tmpsc,scopes as env) =
   let id = try coerce_to_id (fst (List.assoc id subst)) with Not_found -> id in
-  id,(Idset.add id ids,impls,scopes)
+  id,(Idset.add id ids,impls,tmpsc,scopes)
 
-let rec subst_rawconstr loc interp subst (ids,impls,scopes as env) = function
+type ameta_scope =
+  | RefArg of (global_reference * int) list
+  | TypeArg
+
+let rec subst_rawconstr loc interp subst (ids,impls,_,scopes as env) = function
   | AVar id ->
-      let (a,subscopes) =
+      let (a,(scopt,subscopes)) =
+	(* subst remembers the delimiters stack in the interpretation *)
+	(* of the notations *)
 	try List.assoc id subst
-	with Not_found -> (CRef (Ident (loc,id)),[]) in
-      interp (ids,impls,subscopes@scopes) a
+	with Not_found -> (CRef (Ident (loc,id)),(None,[])) in
+      let env = (ids,impls,scopt,subscopes@scopes) in
+      interp env a
+(*
+  | AApp (ARef ref,args) ->
+      let argscopes = find_arguments_scope ref in
+      let argsenv = adjust_scopes env argscopes args in
+      RApp (loc,RRef (loc,ref),
+        List.map2 (subst_rawconstr loc interp subst) argsenv args)
+	(* TODO: adjust type_scope for lambda, annotations, etc *)
+*)
   | t ->
       map_aconstr_with_binders_loc loc (traverse_binder subst)
-      (subst_rawconstr loc interp subst) env t
+      (subst_rawconstr loc interp subst) (ids,impls,None,scopes) t
+
+let set_type_scope (ids,impls,tmp_scope,scopes) =
+  (ids,impls,Some Symbols.type_scope,scopes)
 
 (**********************************************************************)
 (* Main loop                                                          *)
 
-let internalise isarity sigma env allow_soapp lvar c =
-  let rec intern isarity (ids,impls,scopes as env) = function
+let internalise sigma env allow_soapp lvar c =
+  let rec intern (ids,impls,tmp_scope,scopes as env) = function
     | CRef ref as x ->
 	let (c,imp,subscopes) = intern_reference env lvar ref in
 	(match intern_impargs c env imp subscopes [] with
@@ -406,8 +454,8 @@ let internalise isarity sigma env allow_soapp lvar c =
 	in
 	let ids' = List.fold_right Idset.add lf ids in
 	let defl =
-	  Array.of_list (List.map (intern false (ids',impls,scopes)) lt) in
-	let arityl = Array.of_list (List.map (intern true env) lc) in
+	  Array.of_list (List.map (intern (ids',impls,None,scopes)) lt) in
+	let arityl = Array.of_list (List.map (intern_type env) lc) in
 	RRec (loc,RFix (Array.of_list ln,n), Array.of_list lf, arityl, defl)
     | CCoFix (loc, (locid,iddef), ldecl) ->
 	let (lf,lc,lt) = intern_cofix ldecl in
@@ -419,56 +467,60 @@ let internalise isarity sigma env allow_soapp lvar c =
 	in
 	let ids' = List.fold_right Idset.add lf ids in
 	let defl =
-	  Array.of_list (List.map (intern false (ids',impls,scopes)) lt) in
-	let arityl = Array.of_list (List.map (intern true env) lc) in
+	  Array.of_list (List.map (intern (ids',impls,None,scopes)) lt) in
+	let arityl = Array.of_list (List.map (intern_type env) lc) in
 	RRec (loc,RCoFix n, Array.of_list lf, arityl, defl)
     | CArrow (loc,c1,c2) ->
-        RProd (loc, Anonymous, intern true env c1, intern true env c2)
+        RProd (loc, Anonymous, intern_type env c1, intern_type env c2)
     | CProdN (loc,[],c2) ->
-        intern true env c2
+        intern_type env c2
     | CProdN (loc,(nal,ty)::bll,c2) ->
         iterate_prod loc env ty (CProdN (loc, bll, c2)) nal
     | CLambdaN (loc,[],c2) ->
-        intern isarity env c2
+        intern env c2
     | CLambdaN (loc,(nal,ty)::bll,c2) ->
-	iterate_lam loc isarity env ty (CLambdaN (loc, bll, c2)) nal
+	iterate_lam loc env ty (CLambdaN (loc, bll, c2)) nal
     | CLetIn (loc,(_,na),c1,c2) ->
-	RLetIn (loc, na, intern false env c1,
-          intern false (name_fold Idset.add na ids,impls,scopes) c2)
+	RLetIn (loc, na, intern env c1,
+          intern (name_fold Idset.add na ids,impls,tmp_scope,scopes) c2)
     | CNotation (loc,"- _",[CNumeral(_,Bignat.POS p)]) ->
+	let scopes = option_cons tmp_scope scopes in
         Symbols.interp_numeral loc (Bignat.NEG p) scopes
     | CNotation (loc,ntn,args) ->
-	let scopes = if isarity then Symbols.type_scope::scopes else scopes in
+	let scopes = option_cons tmp_scope scopes in
 	let (ids,c) = Symbols.interp_notation ntn scopes in
 	let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
-	subst_rawconstr loc (intern false) subst env c
+	subst_rawconstr loc intern subst env c
     | CNumeral (loc, n) ->
+	let scopes = option_cons tmp_scope scopes in
 	Symbols.interp_numeral loc n scopes
     | CDelimiters (loc, key, e) ->
-	intern isarity (ids,impls,find_delimiters_scope loc key::scopes) e
-    | CAppExpl (loc, ref, args) ->
+	intern (ids,impls,None,find_delimiters_scope loc key::scopes) e
+    | CAppExpl (loc, (isproj,ref), args) ->
         let (f,_,args_scopes) = intern_reference env lvar ref in
+	if isproj then check_projection (List.length args) f;
 	RApp (loc, f, intern_args env args_scopes args)
-    | CApp (loc, f, args) ->
+    | CApp (loc, (isproj,f), args) ->
 	let (c, impargs, args_scopes) =
 	  match f with
 	    | CRef ref -> intern_reference env lvar ref
-	    | _ -> (intern false env f, [], [])
+	    | _ -> (intern env f, [], [])
         in
 	let args = intern_impargs c env impargs args_scopes args in
+	if isproj then check_projection (List.length args) c;
 	(match c with 
 	  | RApp (loc', f', args') ->
 	      (* May happen with the ``...`` and `...` grammars *)
 	      RApp (join_loc loc' loc, f',args'@args)
 	  | _ -> RApp (loc, c, args))
     | CCases (loc, po, tms, eqns) ->
-	RCases (loc, option_app (intern true env) po,
-		List.map (intern false env) tms,
+	RCases (loc, option_app (intern_type env) po,
+		List.map (intern env) tms,
 		List.map (intern_eqn (List.length tms) env) eqns)
     | COrderedCase (loc, tag, po, c, cl) ->
-	ROrderedCase (loc, tag, option_app (intern true env) po,
-	          intern false env c,
-		  Array.of_list (List.map (intern false env) cl))
+	ROrderedCase (loc, tag, option_app (intern_type env) po,
+	          intern env c,
+		  Array.of_list (List.map (intern env) cl))
     | CHole loc -> 
 	RHole (loc, QuestionMark)
     | CPatVar (loc, n) when allow_soapp ->
@@ -488,13 +540,17 @@ let internalise isarity sigma env allow_soapp lvar c =
     | CSort (loc, s) ->
 	RSort(loc,s)
     | CCast (loc, c1, c2) ->
-	RCast (loc,intern false env c1,intern true env c2)
+	RCast (loc,intern env c1,intern_type env c2)
 
     | CDynamic (loc,d) -> RDynamic (loc,d)
 
-  and intern_eqn n (ids,impls,scopes as env) (loc,lhs,rhs) =
+  and intern_type (ids,impls,tmp_scope,scopes) =
+    intern (ids,impls,Some Symbols.type_scope,scopes)
+
+  and intern_eqn n (ids,impls,tmp_scope,scopes as env) (loc,lhs,rhs) =
 	let (idsl_substl_list,pl) =
-	  List.split (List.map (intern_cases_pattern scopes ([],[])) lhs) in
+	  List.split 
+	    (List.map (intern_cases_pattern scopes ([],[]) None) lhs) in
 	let idsl, substl = List.split (List.flatten idsl_substl_list) in
 	let eqn_ids = List.flatten idsl in
 	let subst = List.flatten substl in 
@@ -505,25 +561,25 @@ let internalise isarity sigma env allow_soapp lvar c =
 	let rhs = replace_vars_constr_expr subst rhs in
 	List.iter message_redundant_alias subst;
 	let env_ids = List.fold_right Idset.add eqn_ids ids in
-	(loc, eqn_ids,pl,intern false (env_ids,impls,scopes) rhs)
+	(loc, eqn_ids,pl,intern (env_ids,impls,tmp_scope,scopes) rhs)
 
-  and iterate_prod loc2 (ids,impls,scopes as env) ty body = function
+  and iterate_prod loc2 (ids,impls,tmpsc,scopes as env) ty body = function
     | (loc1,na)::nal ->
 	if nal <> [] then check_capture loc1 ty na;
 	let ids' = name_fold Idset.add na ids in
-	let body = iterate_prod loc2 (ids',impls,scopes) ty body nal in
-	let ty = locate_if_isevar loc1 na (intern true env ty) in
+	let body = iterate_prod loc2 (ids',impls,tmpsc,scopes) ty body nal in
+	let ty = locate_if_isevar loc1 na (intern_type env ty) in
 	RProd (join_loc loc1 loc2, na, ty, body)
-    | [] -> intern true env body
+    | [] -> intern env body
 
-  and iterate_lam loc2 isarity (ids,impls,scopes as env) ty body = function
+  and iterate_lam loc2 (ids,impls,tmpsc,scopes as env) ty body = function
     | (loc1,na)::nal ->
 	if nal <> [] then check_capture loc1 ty na;
 	let ids' = name_fold Idset.add na ids in
-	let body = iterate_lam loc2 isarity (ids',impls,scopes) ty body nal in
-	let ty = locate_if_isevar loc1 na (intern true env ty) in
+	let body = iterate_lam loc2 (ids',impls,tmpsc,scopes) 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 isarity env body
+    | [] -> intern env body
 
   and intern_impargs c env l subscopes args =
     let rec aux n l subscopes args = 
@@ -532,7 +588,7 @@ let internalise isarity sigma env allow_soapp lvar c =
       | (imp::l', (a,Some j)::args') ->
 	  if is_status_implicit imp & j>=n then
 	    if j=n then 
-	      (intern false enva a)::(aux (n+1) l' subscopes' args')
+	      (intern enva a)::(aux (n+1) l' subscopes' args')
 	    else 
 	      (RHole (set_hole_implicit n c))::(aux (n+1) l' subscopes' args)
 	  else 
@@ -543,7 +599,7 @@ let internalise isarity sigma env allow_soapp lvar c =
 	  if is_status_implicit imp then 
 	    (RHole (set_hole_implicit n c))::(aux (n+1) l' subscopes' args)
 	  else 
-	    (intern false enva a)::(aux (n+1) l' subscopes' args')
+	    (intern enva a)::(aux (n+1) l' subscopes' args')
       | ([],args) -> intern_tailargs env subscopes args
       | (_::l',[]) ->
           if List.for_all is_status_implicit l then
@@ -557,18 +613,18 @@ let internalise isarity sigma env allow_soapp lvar c =
 	raise (InternalisationError (constr_loc a, WrongExplicitImplicit))
     | (a,None)::args ->
       let (enva,subscopes) = apply_scope_env env subscopes in
-      (intern false enva a) :: (intern_tailargs env subscopes args)
+      (intern enva a) :: (intern_tailargs env subscopes args)
     | [] -> []
 
   and intern_args env subscopes = function
     | [] -> []
     | a::args ->
         let (enva,subscopes) = apply_scope_env env subscopes in
-        (intern false enva a) :: (intern_args env subscopes args)
+        (intern enva a) :: (intern_args env subscopes args)
 
   in 
   try 
-    intern isarity env c
+    intern env c
   with
       InternalisationError (loc,e) ->
 	user_err_loc (loc,"internalize",explain_internalisation_error e)
@@ -583,7 +639,8 @@ let extract_ids env =
     Idset.empty
 
 let interp_rawconstr_gen isarity sigma env impls allow_soapp ltacvar c =
-  internalise isarity sigma (extract_ids env, impls, [])
+  let tmp_scope = if isarity then Some Symbols.type_scope else None in
+  internalise sigma (extract_ids env, impls, tmp_scope,[])
     allow_soapp (ltacvar,Environ.named_context env, []) c
 
 let interp_rawconstr sigma env c =
@@ -677,10 +734,12 @@ let interp_aconstr vars 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 -> (id,ref None)) vars in
-  let c = for_grammar (internalise false Evd.empty (extract_ids env, [], [])
+  let c = for_grammar (internalise Evd.empty (extract_ids env, [], None, [])
     false (([],[]),Environ.named_context env,vl)) a in
   (* Translate and check that [c] has all its free variables bound in [vars] *)
   let a = aconstr_of_rawconstr vars c in
   (* Returns [a] and the ordered list of variables with their scopes *)
-  (* Variables occuring in binders have no relevant scope since bound *)
-  List.map (fun (id,r) -> (id,match !r with None -> [] | Some l -> l)) vl, a
+  (* Variables occurring in binders have no relevant scope since bound *)
+  List.map
+    (fun (id,r) -> (id,match !r with None -> None,[] | Some (a,l) -> a,l)) vl,
+  a
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index c8f79b8c5..5b1d2813b 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -176,6 +176,11 @@ allowed in abbreviatable expressions"
 
 (* Pattern-matching rawconstr and aconstr *)
 
+let rec adjust_scopes = function
+  | _,[] -> []
+  | [],a::args -> (None,a) :: adjust_scopes ([],args)
+  | sc::scopes,a::args -> (sc,a) :: adjust_scopes (scopes,args)
+
 exception No_match
 
 let rec alpha_var id1 id2 = function
@@ -186,12 +191,79 @@ let rec alpha_var id1 id2 = function
 
 let alpha_eq_val (x,y) = x = y
 
+(*
+let bind_env sc sigma var v =
+  try
+    let vvar,_ = List.assoc var sigma in
+    if alpha_eq_val (v,vvar) then sigma
+    else raise No_match
+  with Not_found ->
+    (* TODO: handle the case of multiple occs in different scopes *)
+    (var,(v,sc))::sigma
+
+let rec match_ sc alp metas sigma a1 a2 = match (a1,a2) with
+  | r1, AVar id2 when List.mem id2 metas -> bind_env sc sigma id2 r1
+  | RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma
+  | RRef (_,r1), ARef r2 when r1 = r2 -> sigma
+  | RPatVar (_,(_,n1)), APatVar n2 when n1=n2 -> sigma
+  | RApp (_,f1,l1), AApp (f2,l2) when List.length l1 = List.length l2 ->
+      let sigma = match_ sc alp metas sigma f1 f2 in
+      let l1 = match f1 with
+	| RRef (_,ref) -> adjust_scopes (Symbols.find_arguments_scope ref,l1)
+	| _ -> List.map (fun a -> (None,a)) l1 in
+      List.fold_left2 (fun sigma (sc,a) b -> match_ sc alp metas sigma a b) sigma l1 l2
+  | RLambda (_,na1,t1,b1), ALambda (na2,t2,b2) ->
+     match_binders sc alp metas (match_type alp metas sigma t1 t2) b1 b2 na1 na2
+  | RProd (_,na1,t1,b1), AProd (na2,t2,b2) ->
+     match_binders (Some Symbols.type_scope) alp metas (match_type alp metas sigma t1 t2) b1 b2 na1 na2
+  | RLetIn (_,na1,t1,b1), AProd (na2,t2,b2) ->
+     match_binders sc alp metas (match_ sc alp metas sigma t1 t2) b1 b2 na1 na2
+  | RCases (_,po1,tml1,eqnl1), ACases (po2,tml2,eqnl2) ->
+     let sigma = option_fold_left2 (match_type alp metas) sigma po1 po2 in
+     let sigma = List.fold_left2 (match_ sc alp metas) sigma tml1 tml2 in
+     List.fold_left2 (match_equations sc alp metas) sigma eqnl1 eqnl2
+  | ROrderedCase (_,st,po1,c1,bl1), AOrderedCase (st2,po2,c2,bl2) ->
+     let sigma = option_fold_left2 (match_type alp metas) sigma po1 po2 in
+     array_fold_left2 (match_ sc alp metas)
+       (match_ sc alp metas sigma c1 c2) bl1 bl2
+  | RCast(_,c1,t1), ACast(c2,t2) ->
+      match_type alp metas (match_ sc alp metas sigma c1 c2) t1 t2
+  | RSort (_,s1), ASort s2 when s1 = s2 -> sigma
+  | RPatVar _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
+  | a, AHole _ when not(Options.do_translate()) -> sigma
+  | RHole _, AHole _ -> sigma
+  | (RDynamic _ | RRec _ | REvar _), _ 
+  | _,_ -> raise No_match
+
+and match_type x = match_ (Some Symbols.type_scope) x
+
+and match_binders sc alp metas sigma b1 b2 na1 na2 = match (na1,na2) with
+  | (na1,Name id2) when List.mem id2 metas ->
+      let sigma =
+	name_fold
+	  (fun id sigma -> bind_env None sigma id2 (RVar (dummy_loc,id))) na1 sigma
+      in 
+      match_ sc alp metas sigma b1 b2
+  | (na1,na2) -> 
+      let alp =
+        name_fold
+	  (fun id1 -> name_fold (fun id2 alp -> (id1,id2)::alp) na2) na1 alp in
+      match_ sc alp metas sigma b1 b2
+
+and match_equations sc alp metas sigma (_,idl1,pat1,rhs1) (idl2,pat2,rhs2) =
+  if idl1 = idl2 & pat1 = pat2 (* Useful to reason up to alpha ?? *) then
+    match_ sc alp metas sigma rhs1 rhs2
+  else raise No_match
+
+*)
+
 let bind_env sigma var v =
   try
     let vvar = List.assoc var sigma in
     if alpha_eq_val (v,vvar) then sigma
     else raise No_match
-  with Not_found -> 
+  with Not_found ->
+    (* TODO: handle the case of multiple occs in different scopes *)
     (var,v)::sigma
 
 let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
@@ -243,7 +315,21 @@ and match_equations alp metas sigma (_,idl1,pat1,rhs1) (idl2,pat2,rhs2) =
 
 type scope_name = string
 
-type interpretation = (identifier * scope_name list) list * aconstr
+type interpretation = 
+    (identifier * (scope_name option * scope_name list)) list * aconstr
+
+(*
+let match_aconstr sc c (metas_scl,pat) =
+  let subst = match_ sc [] (List.map fst metas_scl) [] c pat in
+  (* Reorder canonically the substitution *)
+  let find x subst =
+    try List.assoc x subst
+    with Not_found ->
+      (* Happens for binders bound to Anonymous *)
+      (* Find a better way to propagate Anonymous... *)
+      RVar (dummy_loc,x),None in
+  List.map (fun (x,scl) -> let (a,sc) = find x subst in (a,sc,scl)) metas_scl
+*)
 
 let match_aconstr c (metas_scl,pat) =
   let subst = match_ [] (List.map fst metas_scl) [] c pat in
@@ -263,6 +349,8 @@ type notation = string
 
 type explicitation = int
 
+type proj_flag = bool (* [true] = is projection *)
+
 type cases_pattern_expr =
   | CPatAlias of loc * cases_pattern_expr * identifier
   | CPatCstr of loc * reference * cases_pattern_expr list
@@ -278,8 +366,9 @@ type constr_expr =
   | CProdN of loc * (name located list * constr_expr) list * constr_expr
   | CLambdaN of loc * (name located list * constr_expr) list * constr_expr
   | CLetIn of loc * name located * constr_expr * constr_expr
-  | CAppExpl of loc * reference * constr_expr list
-  | CApp of loc * constr_expr * (constr_expr * explicitation option) list
+  | CAppExpl of loc * (proj_flag * reference) * constr_expr list
+  | CApp of loc * (proj_flag * constr_expr) * 
+      (constr_expr * explicitation option) list
   | CCases of loc * constr_expr option * constr_expr list *
       (loc * cases_pattern_expr list * constr_expr) list
   | COrderedCase of loc * case_style * constr_expr option * constr_expr
@@ -345,9 +434,9 @@ let occur_var_constr_ref id = function
 let rec occur_var_constr_expr id = function
   | CRef r -> occur_var_constr_ref id r
   | CArrow (loc,a,b) -> occur_var_constr_expr id a or occur_var_constr_expr id b
-  | CAppExpl (loc,r,l) ->
+  | CAppExpl (loc,(_,r),l) ->
       occur_var_constr_ref id r or List.exists (occur_var_constr_expr id) l
-  | CApp (loc,f,l) ->
+  | CApp (loc,(_,f),l) ->
       occur_var_constr_expr id f or
       List.exists (fun (a,_) -> occur_var_constr_expr id a) l
   | CProdN (_,l,b) -> occur_var_binders id b l
@@ -372,7 +461,7 @@ and occur_var_binders id b = function
 
 let mkIdentC id  = CRef (Ident (dummy_loc, id))
 let mkRefC r     = CRef r
-let mkAppC (f,l) = CApp (dummy_loc, f, List.map (fun x -> (x,None)) l)
+let mkAppC (f,l) = CApp (dummy_loc, (false,f), List.map (fun x -> (x,None)) l)
 let mkCastC (a,b)  = CCast (dummy_loc,a,b)
 let mkLambdaC (idl,a,b) = CLambdaN (dummy_loc,[idl,a],b)
 let mkLetInC (id,a,b)   = CLetIn (dummy_loc,id,a,b)
@@ -389,7 +478,8 @@ let map_binders f g e bl =
 let map_constr_expr_with_binders f g e = function
   | CArrow (loc,a,b) -> CArrow (loc,f e a,f e b)
   | CAppExpl (loc,r,l) -> CAppExpl (loc,r,List.map (f e) l) 
-  | CApp (loc,a,l) -> CApp (loc,f e a,List.map (fun (a,i) -> (f e a,i)) l)
+  | CApp (loc,(p,a),l) -> 
+      CApp (loc,(p,f e a),List.map (fun (a,i) -> (f e a,i)) l)
   | CProdN (loc,bl,b) ->
       let (e,bl) = map_binders f g e bl in CProdN (loc,bl,f e b)
   | CLambdaN (loc,bl,b) ->
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 8f0f5fb75..f5f620528 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -50,10 +50,11 @@ val aconstr_of_rawconstr : identifier list -> rawconstr -> aconstr
 exception No_match
 
 type scope_name = string
-type interpretation = (identifier * scope_name list) list * aconstr
+type interpretation = 
+    (identifier * (scope_name option * scope_name list)) list * aconstr
 
-val match_aconstr : rawconstr -> interpretation ->
-      (rawconstr * scope_name list) list
+val match_aconstr : (* scope_name option -> *) rawconstr -> interpretation ->
+      (rawconstr * (scope_name option * scope_name list)) list
 
 (*s Concrete syntax for terms *)
 
@@ -61,6 +62,8 @@ type notation = string
 
 type explicitation = int
 
+type proj_flag = bool (* [true] = is projection *)
+
 type cases_pattern_expr =
   | CPatAlias of loc * cases_pattern_expr * identifier
   | CPatCstr of loc * reference * cases_pattern_expr list
@@ -76,8 +79,9 @@ type constr_expr =
   | CProdN of loc * (name located list * constr_expr) list * constr_expr
   | CLambdaN of loc * (name located list * constr_expr) list * constr_expr
   | CLetIn of loc * name located * constr_expr * constr_expr
-  | CAppExpl of loc * reference * constr_expr list
-  | CApp of loc * constr_expr * (constr_expr * explicitation option) list
+  | CAppExpl of loc * (proj_flag * reference) * constr_expr list
+  | CApp of loc * (proj_flag * constr_expr) * 
+        (constr_expr * explicitation option) list
   | CCases of loc * constr_expr option * constr_expr list *
       (loc * cases_pattern_expr list * constr_expr) list
   | COrderedCase of loc * case_style * constr_expr option * constr_expr
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 83f4cad58..397189271 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -274,10 +274,11 @@ let subst_constr_expr a loc subs =
       let na = name_app (subst_id subs) na in
       CLetIn (loc,(loc,na),subst b,subst c)
   | CArrow (_,a,b) -> CArrow (loc,subst a,subst b)
-  | CAppExpl (_,Ident (_,id),l) ->
-      CAppExpl (loc,subst_ref loc subs id,List.map subst l) 
+  | CAppExpl (_,(p,Ident (_,id)),l) ->
+      CAppExpl (loc,(p,subst_ref loc subs id),List.map subst l) 
   | CAppExpl (_,r,l) -> CAppExpl (loc,r,List.map subst l) 
-  | CApp (_,a,l) -> CApp (loc,subst a,List.map (fun (a,i) -> (subst a,i)) l)
+  | CApp (_,(p,a),l) ->
+      CApp (loc,(p,subst a),List.map (fun (a,i) -> (subst a,i)) l)
   | CCast (_,a,b) -> CCast (loc,subst a,subst b)
   | CNotation (_,n,l) -> CNotation (loc,n,List.map subst l)
   | CDelimiters (_,s,a) -> CDelimiters (loc,s,subst a)
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 367fd5e0e..be9e00c58 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -23,7 +23,7 @@ let constr_kw =
     ":"; "("; ")"; "["; "]"; "{"; "}"; ","; ";"; "->"; "="; ":="; "!";
     "::"; "<:"; ":<"; "=>"; "<"; ">"; "|"; "?"; "/";
     "<->"; "\\/"; "/\\"; "`"; "``"; "&"; "*"; "+"; "@"; "^"; "#"; "-";
-    "~"; "'"; "<<"; ">>"; "<>";
+    "~"; "'"; "<<"; ">>"; "<>"; ".("
   ]
 let _ = List.iter (fun s -> Lexer.add_token ("",s)) constr_kw
 (* "let" is not a keyword because #Core#let.cci would not parse.
@@ -127,12 +127,12 @@ GEXTEND Gram
   operconstr:
     [ "10" RIGHTA
       [ "!"; f = global; args = LIST0 (operconstr LEVEL "9") ->
-          CAppExpl (loc, f, args)
+          CAppExpl (loc, (false,f), args)
 (*
       | "!"; f = global; "with"; b = binding_list ->
 	  <:ast< (APPLISTWITH $f $b) >>
 *)
-      | f = operconstr; args = LIST1 constr91 -> CApp (loc, f, args) ]
+      | f = operconstr; args = LIST1 constr91 -> CApp (loc, (false,f), args) ]
     | "9" RIGHTA
       [ c1 = operconstr; "::"; c2 = operconstr LEVEL "9" -> CCast (loc, c1, c2) ]
     | "8" RIGHTA
@@ -196,7 +196,7 @@ GEXTEND Gram
       | "("; lc1 = lconstr; ")"; "@"; "["; cl = ne_constr_list; "]" ->
 	  (match lc1 with
 	    | CPatVar (loc2,(false,n)) -> 
-                CApp (loc,CPatVar (loc2, (true,n)), List.map (fun c -> c, None) cl)
+                CApp (loc,(false,CPatVar (loc2, (true,n))), List.map (fun c -> c, None) cl)
 	    | _ ->
 	    Util.error "Second-order pattern-matching expects a head metavariable")
       | IDENT "Fix"; id = identref; "{"; fbinders = fixbinders; "}" ->
@@ -208,7 +208,7 @@ GEXTEND Gram
       | s = sort -> CSort (loc, s)
       | v = global -> CRef v
       | n = bigint -> CNumeral (loc,n)
-      | "!"; f = global -> CAppExpl (loc,f,[])
+      | "!"; f = global -> CAppExpl (loc,(false,f),[])
       | "'"; test_ident_colon; key = IDENT; ":"; c = constr; "'" -> 
           CDelimiters (loc,key,c) ] ]
   ;
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index 88d108fdd..1876863d4 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -142,11 +142,15 @@ GEXTEND Gram
     | "40L" LEFTA
       [ "-"; c = operconstr -> CNotation(loc,"- _",[c]) ]
     | "10L" LEFTA
-      [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,f,args)
-      | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,f,args) ]
+      [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,(false,f),args)
+      | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(false,f),args) ]
     | "9" [ ]
     | "1L" LEFTA
-      [ c=operconstr; "%"; key=IDENT -> CDelimiters (loc,key,c) ]
+      [ c=operconstr; "%"; key=IDENT -> CDelimiters (loc,key,c)
+      |	c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" ->
+	  CApp(loc,(true,CRef f),args@[c,None])
+      | c=operconstr; ".("; "@"; f=global; args=LIST0 NEXT ->
+	  CAppExpl(loc,(false,f),args@[c]) ]
     | "0"
       [ c=atomic_constr -> c
       | c=match_constr -> c
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 7fba1f279..5acc694aa 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -117,10 +117,12 @@ GEXTEND Gram
   hints:
     [ [ IDENT "Resolve"; l = LIST1 global; dbnames = opt_hintbases ->
          (dbnames, 
-	  HintsResolve (List.map (fun qid -> (None, CAppExpl(loc,qid,[]))) l))
+	  HintsResolve
+	    (List.map (fun qid -> (None, CAppExpl(loc,(false,qid),[]))) l))
       | IDENT "Immediate"; l = LIST1 global; dbnames = opt_hintbases ->
         (dbnames, 
-	 HintsImmediate (List.map (fun qid-> (None, CAppExpl (loc,qid,[]))) l))
+	 HintsImmediate
+	   (List.map (fun qid-> (None, CAppExpl (loc,(false,qid),[]))) l))
       | IDENT "Unfold"; l = LIST1 global; dbnames = opt_hintbases ->
         (dbnames, HintsUnfold (List.map (fun qid -> (None,qid)) l)) ] ]
     ;
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 629c20177..0d431ea93 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -422,7 +422,7 @@ GEXTEND Gram
 	   let c = match n with
 	     | Some n ->
 		 let l = list_tabulate (fun _ -> (CHole (loc),None)) n in
-		 CApp (loc,c,l)
+		 CApp (loc,(false,c),l)
 	     | None -> c in
 	   VernacNotation (false,c,Some("'"^id^"'",[]),None,None)
       | IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" ->
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 72a693012..361e24647 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -213,6 +213,19 @@ let pr_cases pr po tml eqns =
       prlist_with_sep (fun () -> str "| ") (pr_eqn pr) eqns ++
       str "end"))
 
+let pr_proj pr pr_app a f l =
+  hov 0 (pr (latom,E) a ++ cut() ++ str ".(" ++ pr_app pr f l ++ str ")")
+
+let pr_explapp pr f l =
+  hov 0 (
+    str "!" ++ pr_reference f ++ 
+    prlist (fun a -> brk (1,1) ++ pr (lapp,L) a) l)
+
+let pr_app pr a l =
+  hov 0 (
+    pr (lapp,L) a ++ 
+    prlist (fun a -> brk (1,1) ++ pr_expl_args pr a) l)
+
 let rec pr inherited a =
   let (strm,prec) = match a with
   | CRef r -> pr_reference r, latom
@@ -234,14 +247,15 @@ let rec pr inherited a =
       hv 1 (
 	hv 1 (str "[" ++ pr_let_binder pr (snd x) a ++ bll ++ str "]") ++
 	brk (0,1) ++ b), lletin
-  | CAppExpl (_,f,l) ->
-      hov 0 (
-	str "!" ++ pr_reference f ++
-	prlist (fun a -> brk (1,1) ++ pr (lapp,L) a) l), lapp
-  | CApp (_,a,l) ->
-      hov 0 (
-	pr (lapp,L) a ++ 
-	prlist (fun a -> brk (1,1) ++ pr_expl_args pr a) l), lapp
+  | CAppExpl (_,(true,f),l) ->
+      let a,l = list_sep_last l in
+      pr_proj pr pr_explapp a f l, lapp
+  | CAppExpl (_,(false,f),l) -> pr_explapp pr f l, lapp
+  | CApp (_,(true,a),l) ->
+      let c,l = list_sep_last l in
+      assert (snd c = None);
+      pr_proj pr pr_app (fst c) a l, lapp
+  | CApp (_,(false,a),l) -> pr_app pr a l, lapp
   | CCases (_,po,tml,eqns) ->
       pr_cases pr po tml eqns, lcases
   | COrderedCase (_,IfStyle,po,c,[b1;b2]) ->
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index a42465572..cf59d9a97 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -194,8 +194,8 @@ let rec mlexpr_of_constr = function
   | Topconstr.CProdN (loc,l,a) -> <:expr< Topconstr.CProdN $dloc$ $mlexpr_of_list (mlexpr_of_pair (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_constr) l$ $mlexpr_of_constr a$ >>
   | Topconstr.CLambdaN (loc,l,a) -> <:expr< Topconstr.CLambdaN $dloc$ $mlexpr_of_list (mlexpr_of_pair (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_constr) l$ $mlexpr_of_constr a$ >>
   | Topconstr.CLetIn (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO"
-  | Topconstr.CAppExpl (loc,a,l) -> <:expr< Topconstr.CAppExpl $dloc$ $mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >>
-  | Topconstr.CApp (loc,a,l) -> <:expr< Topconstr.CApp $dloc$ $mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option mlexpr_of_int)) l$ >>
+  | Topconstr.CAppExpl (loc,a,l) -> <:expr< Topconstr.CAppExpl $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >>
+  | Topconstr.CApp (loc,a,l) -> <:expr< Topconstr.CApp $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option mlexpr_of_int)) l$ >>
   | Topconstr.CCases (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO"
   | Topconstr.COrderedCase (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO"
   | Topconstr.CHole loc -> <:expr< Topconstr.CHole $dloc$ >>