Open notation for declaring record instances.

It solves feature request 1852, makes me and Arnaud happy and 
will permit to factor some more code in typeclasses.
- Records are introduced using the syntax "{| x := t; y := foo |}" and
"with" clauses are currently parsed but not yet supported in the
elaboration. You are invited to suggest other syntaxes :)
- Missing fields are turned into holes, extra fields cause an error
message. The current implementation finds the type of the record
at pretyping time, from the typing constraint alone (and just expects
an inductive with one constructor). It is then impossible to use
scope information to parse the bodies: that may be wrong. The other
solution I see is using the fields to detect the type earlier, before
internalisation of the bodies, but then we get in name clash hell.
- In funind/contrib/interface I mostly put [assert false] everywhere to 
avoid warnings.


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

23 files changed, 211 insertions, 40 deletions

diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 46e33360cf..320bac8302 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -212,6 +212,7 @@ let rec is_rec names =
     | RRef _ | REvar _ | RPatVar _ | RSort _ |  RHole _ | RDynamic _ -> false
     | RCast(_,b,_) -> lookup names b
     | RRec _ -> error "RRec not handled"
+    | RRecord _ -> error "Not handled RRecord"
     | RIf(_,b,_,lhs,rhs) -> 
 	(lookup names b) || (lookup names lhs) || (lookup names rhs)
     | RLetIn(_,na,t,b) | RLambda(_,na,_,t,b) | RProd(_,na,_,t,b)  -> 
@@ -612,6 +613,7 @@ let rec add_args id new_args b =
       CCast(loc,add_args id new_args b1,CastConv(ck,add_args id new_args b2))
   | CCast(loc,b1,CastCoerce) ->
       CCast(loc,add_args id new_args b1,CastCoerce)
+  | CRecord _ -> anomaly "add_args : CRecord"
   | CNotation _ -> anomaly "add_args : CNotation"
   | CGeneralization _ -> anomaly "add_args : CGeneralization"
   | CPrim _ -> b
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index 08a97fd221..7534ce2ca7 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -583,6 +583,7 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 		*)
 		build_entry_lc env funnames avoid (mkRApp(b,args))
 	    | RRec _ -> error "Not handled RRec"
+	    | RRecord _ -> error "Not handled RRecord"
 	    | RProd _ -> error "Cannot apply a type"
 	end (* end of the application treatement *) 
 
@@ -685,6 +686,7 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 
 	end
     | RRec _ -> error "Not handled RRec"
+    | RRecord _ -> error "Not handled RRecord"
     | RCast(_,b,_) -> 
 	build_entry_lc env funnames  avoid b
     | RDynamic _ -> error "Not handled RDynamic"
@@ -1024,7 +1026,7 @@ let rec compute_cst_params relnames params = function
 		 discriminitation ones *)
   | RSort _ -> params
   | RHole _ -> params
-  | RIf _ | RRec _ | RCast _ | RDynamic _  ->
+  | RIf _ | RRecord _ | RRec _ | RCast _ | RDynamic _  ->
       raise (UserError("compute_cst_params", str "Not handled case"))
 and compute_cst_params_from_app acc (params,rtl) = 
   match params,rtl with 
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index 92396af590..ffd7cd007d 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -176,6 +176,7 @@ let change_vars =
 	      change_vars mapping lhs,
 	      change_vars mapping rhs
 	     )
+      | RRecord _ -> error "Records are not supported"
       | RRec _ -> error "Local (co)fixes are not supported"
       | RSort _ -> rt 
       | RHole _ -> rt 
@@ -358,6 +359,7 @@ let rec alpha_rt excluded rt =
 	    alpha_rt excluded rhs
 	   )
     | RRec _ -> error "Not handled RRec"
+    | RRecord _ -> error "Not handled RRecord"
     | RSort _ -> rt 
     | RHole _ -> rt 
     | RCast (loc,b,CastConv (k,t)) -> 
@@ -409,6 +411,7 @@ let is_free_in id =
 	  
     | RIf(_,cond,_,br1,br2) ->
 	is_free_in cond || is_free_in br1 || is_free_in br2
+    | RRecord _ -> raise (UserError ("", str "Not handled RRecord"))
     | RRec _ -> raise (UserError("",str "Not handled RRec"))
     | RSort _ -> false
     | RHole _ -> false
@@ -507,6 +510,7 @@ let replace_var_by_term x_id term =
 	      replace_var_by_pattern rhs
 	     )
       | RRec _ -> raise (UserError("",str "Not handled RRec"))
+      | RRecord _ -> raise (UserError("",str "Not handled RRecord"))
       | RSort _ -> rt 
       | RHole _ -> rt 
       | RCast(loc,b,CastConv(k,t)) -> 
@@ -604,6 +608,8 @@ let ids_of_rawterm c =
       | RCases (loc,sty,rtntypopt,tml,brchl) -> 
 	  List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_rawterm [] c) brchl)
       | RRec _ -> failwith "Fix inside a constructor branch"
+      | RRecord (loc,w,l) -> Option.cata (ids_of_rawterm []) [] w @ 
+	  List.flatten (List.map (fun ((_,id), x) -> id :: ids_of_rawterm [] x) l)
       | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> []
   in
   (* build the set *)
@@ -661,6 +667,7 @@ let zeta_normalize =
 	      zeta_normalize_term lhs,
 	      zeta_normalize_term rhs
 	     )
+      | RRecord _ -> raise (UserError("",str "Not handled RRecord"))
       | RRec _ -> raise (UserError("",str "Not handled RRec"))
       | RSort _ -> rt 
       | RHole _ -> rt 
@@ -705,6 +712,7 @@ let expand_as =
       | RIf(loc,e,(na,po),br1,br2) ->
 	  RIf(loc,expand_as map e,(na,Option.map (expand_as map) po),
 	      expand_as map br1, expand_as map br2)
+      | RRecord _ ->  error "Not handled RRecord"
       | RRec _ ->  error "Not handled RRec"
       | RDynamic _ -> error "Not handled RDynamic"
       | RCast(loc,b,CastConv(kind,t)) -> RCast(loc,expand_as map b,CastConv(kind,expand_as map t))
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index 203bc9e3dd..e7c6c5bcbf 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -210,6 +210,8 @@ let rec depends_of_rawconstr rc acc = match rc with
   | RLambda (_, _, _, rct, rcb)
   | RProd   (_, _, _, rct, rcb)
   | RLetIn  (_, _, rct, rcb) -> depends_of_rawconstr rcb (depends_of_rawconstr rct acc)
+  | RRecord (_, w, l) -> depends_of_rawconstr_list (List.map snd l)
+      (Option.fold_right depends_of_rawconstr w acc)
   | RCases  (_, _, rco, tmt, cc) ->
       (* LEM TODO: handle the cc *)
       (Option.fold_right depends_of_rawconstr rco
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 8201e8fdcc..3c32c40682 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -501,6 +501,45 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  in
 	    { uj_val = v; uj_type = p }
 
+    | RRecord (loc,w,l) ->
+	let cw = Option.map (pretype tycon env isevars lvar) w in
+	let cj = match cw with
+	  | None -> 
+	      (match tycon with
+	      | None -> user_err_loc (loc,"pretype",(str "Unnable to infer the record type."))
+	      | Some (_, ty) -> {uj_val=ty;uj_type=ty})
+	  | Some cj -> cj
+	in
+	let constructor = 
+	  let (IndType (indf,realargs)) = 
+	    try find_rectype env (evars_of !isevars) cj.uj_type
+	    with Not_found ->
+	      error_case_not_inductive_loc loc env (evars_of !isevars) cj
+	  in
+	  let cstrs = get_constructors env indf in 
+	    if Array.length cstrs <> 1 then 
+	      user_err_loc (loc,"pretype",(str "Inductive is not a singleton."))
+	    else
+	      let info = cstrs.(0) in
+	      let fields, rest = 
+		List.fold_left (fun (args, rest as acc) (na, b, t) ->
+		  if b = None then 
+		    try 
+		      let id = out_name na in
+		      let _, t = List.assoc id rest in
+			t :: args, List.remove_assoc id rest
+		    with _ -> RHole (loc, Evd.QuestionMark (Evd.Define false)) :: args, rest
+		  else acc) ([], List.map (fun ((loc, id), t) -> id, (loc, t)) l) info.cs_args
+	      in
+		if rest <> [] then 
+		  let id, (loc, t) = List.hd rest in
+		    user_err_loc (loc,"pretype",(str "Unknown field name " ++ pr_id id))
+		else
+		  RApp (loc,
+		       RDynamic (loc, constr_in (applistc (mkConstruct info.cs_cstr) info.cs_params)),
+		       fields)
+	in pretype tycon env isevars lvar constructor
+
     | RCases (loc,sty,po,tml,eqns) ->
 	Cases.compile_cases loc sty
 	  ((fun vtyc env isevars -> pretype vtyc env isevars lvar),isevars)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index add71a8b09..67946e3a28 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -676,6 +676,11 @@ let rec extern inctx scopes vars r =
       let t = extern_typ scopes vars (anonymize_if_reserved na t) in
       let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in
       CLambdaN (loc,[(dummy_loc,na)::idl,Default bk,t],c)
+	
+  | RRecord (loc,w,l) ->
+      let t' = Option.map (extern inctx scopes vars) w in
+      let l' = List.map (fun (id, c) -> (id, extern inctx scopes vars c)) l in
+      CRecord (loc, t', l')
 
   | RCases (loc,sty,rtntypopt,tml,eqns) ->
       let vars' = 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index cfa88f3cd0..ef7ad36f12 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -946,6 +946,9 @@ let internalise sigma globalenv env allow_patvar lvar c =
           (* Now compact "(f args') args" *)
 	  | RApp (loc', f', args') -> RApp (join_loc loc' loc, f',args'@args)
 	  | _ -> RApp (loc, c, args))
+    | CRecord (loc, w, fs) ->
+	RRecord (loc, Option.map (intern env) w, 
+		List.map (fun (id, c) -> (id, intern env c)) fs)
     | CCases (loc, sty, rtnpo, tms, eqns) ->
         let tms,env' = List.fold_right
           (fun citm (inds,env) ->
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 876af8f54b..0bfc109ab3 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -63,6 +63,24 @@ let free_vars_of_constr_expr c ?(bound=Idset.empty) l =
     | c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c
   in aux bound l c
 
+let ids_of_names l = 
+  List.fold_left (fun acc x -> match snd x with Name na -> na :: acc | Anonymous -> acc) [] l
+
+let free_vars_of_binders ?(bound=Idset.empty) l (binders : local_binder list) = 
+  let rec aux bdvars l c = match c with
+      ((LocalRawAssum (n, _, c)) :: tl) ->
+	let bound = ids_of_names n in
+	let l' = free_vars_of_constr_expr c ~bound:bdvars l in
+	  aux (Idset.union (ids_of_list bound) bdvars) l' tl
+
+    | ((LocalRawDef (n, c)) :: tl) -> 
+	let bound = match snd n with Anonymous -> [] | Name n -> [n] in
+	let l' = free_vars_of_constr_expr c ~bound:bdvars l in
+	  aux (Idset.union (ids_of_list bound) bdvars) l' tl
+	
+    | [] -> bdvars, l
+  in aux bound l binders
+
 let add_name_to_ids set na = 
   match na with 
   | Anonymous -> set 
@@ -80,6 +98,8 @@ let free_vars_of_rawconstr ?(bound=Idset.empty) =
 	let vs' = vars bound vs ty in 
 	let bound' = add_name_to_ids bound na in 
 	vars bound' vs' c
+    | RRecord (loc,w,l) -> List.fold_left (vars bound) vs 
+	(Option.List.cons w (List.map snd l))
     | RCases (loc,sty,rtntypopt,tml,pl) ->
 	let vs1 = vars_option bound vs rtntypopt in 
 	let vs2 = List.fold_left (fun vs (tm,_) -> vars bound vs tm) vs1 tml in 
@@ -128,33 +148,11 @@ let free_vars_of_rawconstr ?(bound=Idset.empty) =
   in 
   fun rt -> List.rev (vars bound [] rt)
       
-
-let ids_of_names l = 
-  List.fold_left (fun acc x -> match snd x with Name na -> na :: acc | Anonymous -> acc) [] l
-
-let free_vars_of_binders ?(bound=Idset.empty) l (binders : local_binder list) = 
-  let rec aux bdvars l c = match c with
-      ((LocalRawAssum (n, _, c)) :: tl) ->
-	let bound = ids_of_names n in
-	let l' = free_vars_of_constr_expr c ~bound:bdvars l in
-	  aux (Idset.union (ids_of_list bound) bdvars) l' tl
-
-    | ((LocalRawDef (n, c)) :: tl) -> 
-	let bound = match snd n with Anonymous -> [] | Name n -> [n] in
-	let l' = free_vars_of_constr_expr c ~bound:bdvars l in
-	  aux (Idset.union (ids_of_list bound) bdvars) l' tl
-	
-    | [] -> bdvars, l
-  in aux bound l binders
-
 let rec make_fresh ids env x =
   if is_freevar ids env x then x else make_fresh ids env (Nameops.lift_ident x)
 
 let freevars_of_ids env ids = 
   List.filter (is_freevar env (Global.env())) ids
-
-let binder_list_of_ids ids =
-  List.map (fun id -> LocalRawAssum ([dummy_loc, Name id], Default Implicit, CHole (dummy_loc, None))) ids
       
 let next_ident_away_from id avoid = make_fresh avoid (Global.env ()) id
 
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 5934272091..dc83e2135c 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -28,19 +28,20 @@ val ids_of_list : identifier list -> Idset.t
 val destClassApp : constr_expr -> loc * reference * constr_expr list
 val destClassAppExpl : constr_expr -> loc * reference * (constr_expr * explicitation located option) list
 
-val free_vars_of_constr_expr :     Topconstr.constr_expr ->
-    ?bound:Idset.t ->
-  Names.identifier list -> Names.identifier list
+(* Fragile, should be used only for construction a set of identifiers to avoid *)
 
-val free_vars_of_rawconstr : ?bound:Idset.t -> rawconstr -> (Names.identifier * loc) list
-
-val binder_list_of_ids : identifier list -> local_binder list
-
-val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier
+val free_vars_of_constr_expr : constr_expr -> ?bound:Idset.t ->
+  identifier list -> identifier list
 
 val free_vars_of_binders :
   ?bound:Idset.t -> Names.identifier list -> local_binder list -> Idset.t * Names.identifier list
 
+(* Returns the free ids in left-to-right order with the location of their first occurence *)
+
+val free_vars_of_rawconstr : ?bound:Idset.t -> rawconstr -> (Names.identifier * loc) list
+
+val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier
+
 val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool)) list
 
 val combine_params_freevar :
diff --git a/interp/reserve.ml b/interp/reserve.ml
index f49c42a55d..2479f1f04e 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -57,6 +57,7 @@ let rec unloc = function
   | RLambda (_,na,bk,ty,c) -> RLambda (dummy_loc,na,bk,unloc ty,unloc c)
   | RProd (_,na,bk,ty,c) -> RProd (dummy_loc,na,bk,unloc ty,unloc c)
   | RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c)
+  | RRecord (_,w,l) -> RRecord (dummy_loc,w,l)
   | RCases (_,sty,rtntypopt,tml,pl) ->
       RCases (dummy_loc,sty,
         (Option.map unloc rtntypopt),
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index c0b81c90c3..3dc77dd604 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -37,6 +37,7 @@ type aconstr =
   | ALambda of name * aconstr * aconstr
   | AProd of name * aconstr * aconstr
   | ALetIn of name * aconstr * aconstr
+  | ARecord of aconstr option * (identifier * aconstr) list
   | ACases of case_style * aconstr option *
       (aconstr * (name * (inductive * int * name list) option)) list *
       (cases_pattern list * aconstr) list
@@ -82,6 +83,8 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
       let e,na = name_fold_map g e na in RProd (loc,na,Explicit,f e ty,f e c)
   | ALetIn (na,b,c) ->
       let e,na = name_fold_map g e na in RLetIn (loc,na,f e b,f e c)
+  | ARecord (b,l) ->
+      RRecord (loc, Option.map (f e) b, List.map (fun (id, x) -> ((loc,id),f e x)) l)
   | ACases (sty,rtntypopt,tml,eqnl) ->
       let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
 	let e',t' = match t with
@@ -146,7 +149,7 @@ let compare_rawconstr f t1 t2 = match t1,t2 with
       f ty1 ty2 & f c1 c2
   | RHole _, RHole _ -> true
   | RSort (_,s1), RSort (_,s2) -> s1 = s2
-  | (RLetIn _ | RCases _ | RRec _ | RDynamic _
+  | (RLetIn _ | RRecord _ | RCases _ | RRec _ | RDynamic _
     | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _),_
   | _,(RLetIn _ | RCases _ | RRec _ | RDynamic _
       | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _)
@@ -192,6 +195,7 @@ let aconstr_and_vars_of_rawconstr a =
   | RLambda (_,na,bk,ty,c) -> add_name found na; ALambda (na,aux ty,aux c)
   | RProd (_,na,bk,ty,c) -> add_name found na; AProd (na,aux ty,aux c)
   | RLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c)
+  | RRecord (_,w,l) -> ARecord (Option.map aux w,List.map (fun ((_,id), x) -> id, aux x) l)
   | RCases (_,sty,rtntypopt,tml,eqnl) ->
       let f (_,idl,pat,rhs) = found := idl@(!found); (pat,aux rhs) in
       ACases (sty,Option.map aux rtntypopt,
@@ -319,6 +323,12 @@ let rec subst_aconstr subst bound raw =
 	if r1' == r1 && r2' == r2 then raw else
 	  ALetIn (n,r1',r2')
 
+  | ARecord (r1,r2) -> 
+      let r1' = Option.smartmap (subst_aconstr subst bound) r1 
+      and r2' = list_smartmap (fun (id, x) -> id,subst_aconstr subst bound x) r2 in
+	if r1' == r1 && r2' == r2 then raw else
+	  ARecord (r1',r2')
+
   | ACases (sty,rtntypopt,rl,branches) -> 
       let rtntypopt' = Option.smartmap (subst_aconstr subst bound) rtntypopt
       and rl' = list_smartmap
@@ -637,6 +647,7 @@ type constr_expr =
   | CAppExpl of loc * (proj_flag * reference) * constr_expr list
   | CApp of loc * (proj_flag * constr_expr) * 
       (constr_expr * explicitation located option) list
+  | CRecord of loc * constr_expr option * (identifier located * constr_expr) list
   | CCases of loc * case_style * constr_expr option *
       (constr_expr * (name option * constr_expr option)) list *
       (loc * cases_pattern_expr list located list * constr_expr) list
@@ -709,6 +720,7 @@ let constr_loc = function
   | CLetIn (loc,_,_,_) -> loc
   | CAppExpl (loc,_,_) -> loc
   | CApp (loc,_,_) -> loc
+  | CRecord (loc,_,_) -> loc
   | CCases (loc,_,_,_,_) -> loc
   | CLetTuple (loc,_,_,_,_) -> loc
   | CIf (loc,_,_,_,_) -> loc
@@ -806,6 +818,7 @@ let fold_constr_expr_with_binders g f n acc = function
   | CDelimiters (loc,_,a) -> f n acc a
   | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _  | CRef _ ->
       acc
+  | CRecord (loc,_,l) -> List.fold_left (fun acc (id, c) -> f n acc c) acc l
   | CCases (loc,sty,rtnpo,al,bl) ->
       let ids = ids_of_cases_tomatch al in
       let acc = Option.fold_left (f (List.fold_right g ids n)) acc rtnpo in
@@ -919,6 +932,7 @@ let map_constr_expr_with_binders g f e = function
   | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
   | CHole _ | CEvar _ | CPatVar _ | CSort _ 
   | CPrim _ | CDynamic _ | CRef _ as x -> x
+  | CRecord (loc,p,l) -> CRecord (loc,p,List.map (fun (id, c) -> (id, f e c)) l)
   | CCases (loc,sty,rtnpo,a,bl) ->
       (* TODO: apply g on the binding variables in pat... *)
       let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 0064d238d1..b6e2927bbd 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -33,6 +33,7 @@ type aconstr =
   | ALambda of name * aconstr * aconstr
   | AProd of name * aconstr * aconstr
   | ALetIn of name * aconstr * aconstr
+  | ARecord of aconstr option * (identifier * aconstr) list
   | ACases of case_style * aconstr option *
       (aconstr * (name * (inductive * int * name list) option)) list *
       (cases_pattern list * aconstr) list
@@ -133,6 +134,7 @@ type constr_expr =
   | CAppExpl of loc * (proj_flag * reference) * constr_expr list
   | CApp of loc * (proj_flag * constr_expr) * 
       (constr_expr * explicitation located option) list
+  | CRecord of loc * constr_expr option * (identifier located * constr_expr) list
   | CCases of loc * case_style * constr_expr option *
       (constr_expr * (name option * constr_expr option)) list *
       (loc * cases_pattern_expr list located list * constr_expr) list
diff --git a/lib/option.ml b/lib/option.ml
index 543c108ab9..3d98034256 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id:$ i*)
+(*i $Id$ i*)
 
 (** Module implementing basic combinators for OCaml option type.
    It tries follow closely the style of OCaml standard library.
@@ -97,6 +97,10 @@ let fold_right f x a =
   | Some y -> f y a
   | _ -> a
 
+(** [cata f a x] is [a] if [x] is [None] and [f y] if [x] is [Some y]. *)
+let cata f a = function
+  | Some c -> f c
+  | None -> a
 
 (** {6 More Specific operations} ***)
 
diff --git a/lib/option.mli b/lib/option.mli
index c1260d9acf..04f3ca37d0 100644
--- a/lib/option.mli
+++ b/lib/option.mli
@@ -66,6 +66,8 @@ val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option -> 'c option -> 'a
 (** [fold_right f x a] is [f y a] if [x] is [Some y], and [a] otherwise. *)
 val fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b
 
+(** [cata e f x] is [e] if [x] is [None] and [f a] if [x] is [Some a] *)
+val cata : ('a -> 'b) -> 'b -> 'a option -> 'b
 
 (** {6 More Specific Operations} ***)
 
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 77b4f003cd..5ecbab90ed 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -25,7 +25,7 @@ let constr_kw =
   [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; 
     "end"; "as"; "let"; "if"; "then"; "else"; "return";
     "Prop"; "Set"; "Type"; ".("; "_"; "..";
-    "`{"; "`("; ]
+    "`{"; "`("; "{|"; "|}" ]
 
 let _ = List.iter (fun s -> Lexer.add_token("",s)) constr_kw
 
@@ -125,6 +125,18 @@ let ident_colon =
               | _ -> raise Stream.Failure)
         | _ -> raise Stream.Failure)
 
+let ident_with =
+  Gram.Entry.of_parser "ident_with"
+    (fun strm ->
+      match Stream.npeek 1 strm with
+      | [("IDENT",s)] ->
+          (match Stream.npeek 2 strm with
+          | [_; ("", "with")] ->
+              Stream.junk strm; Stream.junk strm;
+              Names.id_of_string s
+          | _ -> raise Stream.Failure)
+      | _ -> raise Stream.Failure)
+    
 let aliasvar = function CPatAlias (_, _, id) -> Some (Name id) | _ -> None
 
 GEXTEND Gram
@@ -205,6 +217,7 @@ GEXTEND Gram
               CPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
                 CNotation(loc,"( _ )",([c],[]))
             | _ -> c)
+      | "{|"; c = record_declaration; "|}" -> c
       | "`{"; c = operconstr LEVEL "200"; "}" ->
 	  CGeneralization (loc, Implicit, None, c)
       | "`("; c = operconstr LEVEL "200"; ")" ->
@@ -221,6 +234,15 @@ GEXTEND Gram
     | IDENT "λ" -> ()
     ] ]
   ;
+  record_declaration:
+    [ [ fs = LIST1 record_field_declaration SEP ";" -> CRecord (loc, None, fs)
+      | c = lconstr; "with"; fs = LIST1 record_field_declaration SEP ";" ->
+	  CRecord (loc, Some c, fs)
+    ] ]
+  ;
+  record_field_declaration:
+    [ [ id = identref; ":="; c = lconstr -> (id, c) ] ]
+  ;
   binder_constr:
     [ [ forall; bl = binder_list; ","; c = operconstr LEVEL "200" ->
           mkCProdN loc bl c
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index a2cad8e170..19446b7d19 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -552,6 +552,17 @@ let rec pr sep inherited a =
       else
 	p, lproj
   | CApp (_,(None,a),l) -> pr_app (pr mt) a l, lapp
+  | CRecord (_,w,l) ->
+      let beg = 
+	match w with
+	| None -> spc () 
+	| Some t -> spc () ++ pr spc ltop t ++ spc () ++ str"with" ++ spc ()
+      in
+	hv 0 (str"{" ++ beg ++	       
+		 prlist_with_sep (fun () -> spc () ++ str";" ++ spc ())
+		 (fun ((_,id), c) -> pr_id id ++ spc () ++ str":=" ++ spc () ++ pr spc ltop c)
+		 l), latom
+
   | CCases (_,LetPatternStyle,rtntypopt,[c,asin],[(_,[(loc,[p])],b)]) ->
       hv 0 (
 	str "let '" ++ 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 6854a4a7c5..eb4c737914 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -603,6 +603,12 @@ let rec subst_rawconstr subst raw =
 	if r1' == r1 && r2' == r2 then raw else
 	  RLetIn (loc,n,r1',r2')
 
+  | RRecord (loc,w,rl) ->
+      let w' = Option.smartmap (subst_rawconstr subst) w 
+      and rl' = list_smartmap (fun (id, x) -> (id, subst_rawconstr subst x)) rl in
+	if w == w' && rl == rl' then raw else
+	  RRecord (loc,w',rl')
+
   | RCases (loc,sty,rtno,rl,branches) -> 
       let rtno' = Option.smartmap (subst_rawconstr subst) rtno
       and rl' = list_smartmap (fun (a,x as y) ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 08ecae12e8..c114a922c0 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -587,6 +587,45 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  in
 	    { uj_val = v; uj_type = p }
 	
+    | RRecord (loc,w,l) ->
+	let cw = Option.map (pretype tycon env evdref lvar) w in
+	let cj = match cw with
+	  | None -> 
+	      (match tycon with
+	      | None -> user_err_loc (loc,"pretype",(str "Unnable to infer the record type."))
+	      | Some (_, ty) -> {uj_val=ty;uj_type=ty})
+	  | Some cj -> cj
+	in
+	let constructor = 
+	  let (IndType (indf,realargs)) = 
+	    try find_rectype env (evars_of !evdref) cj.uj_type
+	    with Not_found ->
+	      error_case_not_inductive_loc loc env (evars_of !evdref) cj
+	  in
+	  let cstrs = get_constructors env indf in 
+	    if Array.length cstrs <> 1 then 
+	      user_err_loc (loc,"pretype",(str "Inductive is not a singleton."))
+	    else
+	      let info = cstrs.(0) in
+	      let fields, rest = 
+		List.fold_left (fun (args, rest as acc) (na, b, t) ->
+		  if b = None then 
+		    try 
+		      let id = out_name na in
+		      let _, t = List.assoc id rest in
+			t :: args, List.remove_assoc id rest
+		    with _ -> RHole (loc, Evd.QuestionMark (Evd.Define false)) :: args, rest
+		  else acc) ([], List.map (fun ((loc, id), t) -> id, (loc, t)) l) info.cs_args
+	      in
+		if rest <> [] then 
+		  let id, (loc, t) = List.hd rest in
+		    user_err_loc (loc,"pretype",(str "Unknown field name " ++ pr_id id))
+		else
+		  RApp (loc,
+		       RDynamic (loc, constr_in (applistc (mkConstruct info.cs_cstr) info.cs_params)),
+		       fields)
+	in pretype tycon env evdref lvar constructor
+	  
     | RCases (loc,sty,po,tml,eqns) ->
 	Cases.compile_cases loc sty
 	  ((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref)
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index ea622de7f4..b2e770f65a 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -62,6 +62,7 @@ type rawconstr =
   | RLambda of loc * name * binding_kind * rawconstr * rawconstr
   | RProd of loc * name * binding_kind * rawconstr * rawconstr
   | RLetIn of loc * name * rawconstr * rawconstr
+  | RRecord of loc * rawconstr option * ((loc * identifier) * rawconstr) list
   | RCases of loc * case_style * rawconstr option * tomatch_tuples * cases_clauses
   | RLetTuple of loc * name list * (name * rawconstr option) * 
       rawconstr * rawconstr
@@ -114,6 +115,7 @@ let map_rawconstr f = function
   | RLambda (loc,na,bk,ty,c) -> RLambda (loc,na,bk,f ty,f c)
   | RProd (loc,na,bk,ty,c) -> RProd (loc,na,bk,f ty,f c)
   | RLetIn (loc,na,b,c) -> RLetIn (loc,na,f b,f c)
+  | RRecord (loc,c,l) -> RRecord (loc,Option.map f c,List.map (fun (id,c) -> id, f c) l)
   | RCases (loc,sty,rtntypopt,tml,pl) ->
       RCases (loc,sty,Option.map f rtntypopt,
         List.map (fun (tm,x) -> (f tm,x)) tml,
@@ -174,6 +176,8 @@ let occur_rawconstr id =
     | RLambda (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
     | RProd (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
     | RLetIn (loc,na,b,c) -> (occur b) or ((na <> Name id) & (occur c))
+    | RRecord (loc,w,l) -> Option.cata occur false w
+	or List.exists (fun (_, c) -> occur c) l
     | RCases (loc,sty,rtntypopt,tml,pl) ->
 	(occur_option rtntypopt)
         or (List.exists (fun (tm,_) -> occur tm) tml)
@@ -219,7 +223,9 @@ let free_rawvars  =
     | RLambda (loc,na,_,ty,c) | RProd (loc,na,_,ty,c) | RLetIn (loc,na,ty,c) -> 
 	let vs' = vars bounded vs ty in 
 	let bounded' = add_name_to_ids bounded na in 
-	vars bounded' vs' c
+       vars bounded' vs' c
+    | RRecord (loc,f,args) -> 
+	List.fold_left (vars bounded) vs (Option.List.cons f (List.map snd args))
     | RCases (loc,sty,rtntypopt,tml,pl) ->
 	let vs1 = vars_option bounded vs rtntypopt in 
 	let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in 
@@ -280,6 +286,7 @@ let loc_of_rawconstr = function
   | RLambda (loc,_,_,_,_) -> loc
   | RProd (loc,_,_,_,_) -> loc
   | RLetIn (loc,_,_,_) -> loc
+  | RRecord (loc,_,_) -> loc
   | RCases (loc,_,_,_,_) -> loc
   | RLetTuple (loc,_,_,_,_) -> loc
   | RIf (loc,_,_,_,_) -> loc
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 3628e2a503..5115e2d59b 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -66,6 +66,7 @@ type rawconstr =
   | RLambda of loc * name * binding_kind *  rawconstr * rawconstr
   | RProd of loc * name * binding_kind * rawconstr * rawconstr
   | RLetIn of loc * name * rawconstr * rawconstr
+  | RRecord of loc * rawconstr option * ((loc * identifier) * rawconstr) list
   | RCases of loc * case_style * rawconstr option * tomatch_tuples * cases_clauses
   | RLetTuple of loc * name list * (name * rawconstr option) * 
       rawconstr * rawconstr
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 97fbae075b..c437d9eab2 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -25,7 +25,7 @@ open Util
 (* This module defines type-classes *)
 type typeclass = {
   (* The class implementation: a record parameterized by the context with defs in it or a definition if 
-     the class is a singleton. This acts as the classe's global identifier. *)
+     the class is a singleton. This acts as the class' global identifier. *)
   cl_impl : global_reference; 
 
   (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. 
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 4e87109187..4eca304c24 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -257,7 +257,9 @@ let new_class id par ar sup props =
 type binder_def_list = (identifier located * identifier located list * constr_expr) list
 
 let binders_of_lidents l =
-  List.map (fun (loc, id) -> LocalRawAssum ([loc, Name id], Default Rawterm.Implicit, CHole (loc, None))) l
+  List.map (fun (loc, id) -> 
+    LocalRawAssum ([loc, Name id], Default Rawterm.Explicit, 
+		  CHole (loc, Some (BinderType (Name id))))) l
 
 let type_ctx_instance isevars env ctx inst subst =
   let (s, _) = 
@@ -312,7 +314,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
   let tclass = 
     match bk with
     | Implicit ->
-	Implicit_quantifiers.implicit_application Idset.empty
+	Implicit_quantifiers.implicit_application Idset.empty ~allow_partial:false
 	  (fun avoid (clname, (id, _, t)) -> 
 	    match clname with 
 	    | Some (cl, b) -> 
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index 82a2a84495..094c931968 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -166,8 +166,8 @@ let rec uri_of_constr c =
       uri_of_constr b; url_string " in "; uri_of_constr c
   | RCast (_,c, CastConv (_,t)) ->
       uri_of_constr c; url_string ":"; uri_of_constr t
-  | RRec _ | RIf _ | RLetTuple _ | RCases _ ->
-      error "Whelp does not support pattern-matching and (co-)fixpoint."
+  | RRecord _ | RRec _ | RIf _ | RLetTuple _ | RCases _ ->
+      error "Whelp does not support records, pattern-matching and (co-)fixpoint."
   | RVar _ | RRef _ | RHole _ | REvar _ | RSort _ | RCast (_,_, CastCoerce) ->
       anomaly "Written w/o parenthesis"
   | RPatVar _ | RDynamic _ ->