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

1 files changed, 20 insertions, 22 deletions

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