Move Record desugaring to constrintern and add ability to use notations

for record fields (using "someproj : sometype where not := constr" syntax). Only one
notation allowed currently and no redeclaration after the record
declaration either (will be done for typeclasses).


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

6 files changed, 2 insertions, 54 deletions

diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 320bac830..b6b2cbd11 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -212,7 +212,6 @@ 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)  -> 
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index 48a96f8b6..c16e645c7 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -583,7 +583,6 @@ 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 *) 
 
@@ -686,7 +685,6 @@ 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"
@@ -1026,7 +1024,7 @@ let rec compute_cst_params relnames params = function
 		 discriminitation ones *)
   | RSort _ -> params
   | RHole _ -> params
-  | RIf _ | RRecord _ | RRec _ | RCast _ | RDynamic _  ->
+  | RIf _ | 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 ffd7cd007..92396af59 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -176,7 +176,6 @@ 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 
@@ -359,7 +358,6 @@ 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)) -> 
@@ -411,7 +409,6 @@ 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
@@ -510,7 +507,6 @@ 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)) -> 
@@ -608,8 +604,6 @@ 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 *)
@@ -667,7 +661,6 @@ 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 
@@ -712,7 +705,6 @@ 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 e7c6c5bcb..203bc9e3d 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -210,8 +210,6 @@ 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/interface/xlate.ml b/contrib/interface/xlate.ml
index 2b6f681f1..73acbf0f3 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1501,7 +1501,7 @@ let build_constructors l =
  CT_constr_list (List.map f l)
 
 let build_record_field_list l =
- let build_record_field (coe,d) = match d with
+ let build_record_field ((coe,d),not) = match d with
   | AssumExpr (id,c) ->
       if coe then CT_recconstr_coercion (xlate_id_opt id, xlate_formula c)
       else
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 3c32c4068..8201e8fdc 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -501,45 +501,6 @@ 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)