Fixed bug #2006 (type constraint on Record was not taken into account) +

slight improving of the printing of record.



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

6 files changed, 39 insertions, 14 deletions

diff --git a/CHANGES b/CHANGES
index c346fc8b3a..e0012e8326 100644
--- a/CHANGES
+++ b/CHANGES
@@ -43,6 +43,7 @@ Language
   As a consequence, Acc_rect has now a more direct proof [possible source
   of easily fixed incompatibility in case of manual definition of a recursor
   in a recursive singleton inductive type].
+- Specific sort constraints on Record now taken into account.
 
 Vernacular commands
 
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 8dc220f65e..3163cfb71b 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -349,10 +349,10 @@ let pr_record (sp,tyi) =
       str ": " ++ pr_lconstr_env envpar arity ++ brk(1,2) ++ 
       str ":= " ++ pr_id cstrnames.(0)) ++ 
     brk(1,2) ++
-    hv 2 (str "{ " ++
-      prlist_with_sep (fun () -> str "; " ++ brk(1,0))
+    hv 2 (str "{" ++
+      prlist_with_sep (fun () -> str ";" ++ brk(1,0))
         (fun (id,b,c) -> 
-	  pr_id id ++ str (if b then " : " else " := ") ++ 
+	  str " " ++ pr_id id ++ str (if b then " : " else " := ") ++ 
 	  pr_lconstr_env envpar c) fields) ++ str" }")
 
 let gallina_print_inductive sp =
diff --git a/test-suite/bugs/closed/shouldfail/2006.v b/test-suite/bugs/closed/shouldfail/2006.v
new file mode 100644
index 0000000000..f67e997e8c
--- /dev/null
+++ b/test-suite/bugs/closed/shouldfail/2006.v
@@ -0,0 +1,23 @@
+(* Take the type constraint on Record into account *)
+
+Definition Type1 := Type.
+Record R : Type1 := { p:Type1 }. (* was accepted before trunk revision 11619 *)
+
+(* 
+Remarks:
+
+- The behaviour was inconsistent with the one of Inductive, e.g.
+
+  Inductive R : Type1 := Build_R : Type1 -> R.
+
+  was correctly refused.
+
+- CoRN makes some use of the following configuration:
+
+  Definition CProp := Type.
+  Record R : CProp := { ... }.
+
+  CoRN may have to change the CProp definition into a notation if the
+  preservation of the former semantics of Record type constraints 
+  turns to be required.
+*)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index f1ee0ab658..59559f9234 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -341,6 +341,13 @@ let declare_class finite id idbuild paramimpls params arity fieldimpls fields
       k.cl_projs coers;
     add_class k; impl
 
+let interp_and_check_sort sort =
+  Option.map (fun sort ->
+    let env = Global.env() and sigma = Evd.empty in
+    let s = interp_constr sigma env sort in
+    if isSort (Reductionops.whd_betadeltaiota env sigma s) then s
+    else user_err_loc (constr_loc sort,"", str"Sort expected.")) sort
+
 open Vernacexpr
 
 (* [fs] corresponds to fields and [ps] to parameters; [coers] is a boolean 
@@ -355,14 +362,14 @@ let definition_structure (kind,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) =
   let allnames =  idstruc::(List.fold_left extract_name [] fs) in
   if not (list_distinct allnames) then error "Two objects have the same name";
   (* Now, younger decl in params and fields is on top *)
-  let sc = Option.map mkSort s in
+  let sc = interp_and_check_sort s in
   let implpars, params, implfs, fields = 
     States.with_heavy_rollback (fun () ->
       typecheck_params_and_fields idstruc sc ps notations fs) ()
   in
     match kind with
     | Record | Structure ->
-	let arity = Option.cata (fun x -> x) (new_Type ()) sc in
+	let arity = Option.default (new_Type ()) sc in
 	let implfs = List.map
 	  (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs
 	in IndRef (declare_structure finite idstruc idbuild implpars params arity implfs fields is_coe coers)
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 8a4ca735c7..b74c1a4af7 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -37,4 +37,5 @@ val declare_structure : bool (*coinductive?*)-> identifier -> identifier ->
 
 val definition_structure :
   record_kind * bool (*coinductive?*)*lident with_coercion * local_binder list *
-  (local_decl_expr with_coercion with_notation) list * identifier * sorts option -> global_reference
+  (local_decl_expr with_coercion with_notation) list * 
+  identifier * constr_expr option -> global_reference
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 4b4f7abb55..36d1e0175e 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -379,20 +379,13 @@ let vernac_record k finite struc binders sort nameopt cfs =
 	Dumpglob.dump_definition lid false "constr"; id in
   let sigma = Evd.empty in
   let env = Global.env() in
-  let s = Option.map (fun x ->
-    let s = Reductionops.whd_betadeltaiota env sigma (interp_constr sigma env x) in
-      match kind_of_term s with
-      | Sort s -> s
-      | _ -> user_err_loc
-          (constr_loc x,"definition_structure", str "Sort expected.")) sort
-  in
     if Dumpglob.dump () then (
       Dumpglob.dump_definition (snd struc) false "rec";
       List.iter (fun ((_, x), _) ->
 	match x with
 	| Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj"
 	| _ -> ()) cfs);
-    ignore(Record.definition_structure (k,finite,struc,binders,cfs,const,s))
+    ignore(Record.definition_structure (k,finite,struc,binders,cfs,const,sort))
       
 let vernac_inductive finite indl = 
   if Dumpglob.dump () then