bugs avec Pose et Assert

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

2 files changed, 10 insertions, 10 deletions

diff --git a/toplevel/record.ml b/toplevel/record.ml
index a2a679cb19..89cb35b74b 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -32,17 +32,15 @@ open Topconstr
 
 (********** definition d'un record (structure) **************)
 
-let name_of id = if id = wildcard then Anonymous else Name id
-
 let interp_decl sigma env = function
-  | Vernacexpr.AssumExpr((_,id),t) -> (name_of id,None,interp_type Evd.empty env t)
+  | Vernacexpr.AssumExpr((_,id),t) -> (id,None,interp_type Evd.empty env t)
   | Vernacexpr.DefExpr((_,id),c,t) ->
       let c = match t with
 	| None -> c
 	| Some t -> mkCastC (c,t)
       in
       let j = judgment_of_rawconstr Evd.empty env c in
-      (Name id,Some j.uj_val, j.uj_type)
+      (id,Some j.uj_val, j.uj_type)
 
 let typecheck_params_and_fields ps fs =
   let env0 = Global.env () in
@@ -210,10 +208,11 @@ let declare_projections indsp coers fields =
 let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
   let coers,fs = List.split cfs in
   let nparams = local_binders_length ps in
-  let extract_name = function
-      Vernacexpr.AssumExpr((_,id),_) -> id
-    | Vernacexpr.DefExpr ((_,id),_,_) -> id in
-  let allnames =  idstruc::(List.map extract_name fs) in
+  let extract_name acc = function
+      Vernacexpr.AssumExpr((_,Name id),_) -> id::acc
+    | Vernacexpr.DefExpr ((_,Name id),_,_) -> id::acc
+    | _ -> acc in
+  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 params,fields = typecheck_params_and_fields ps fs in
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index fe07a53d50..9fd934d563 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -26,6 +26,7 @@ open Libnames
 open Nametab
 
 type lident = identifier located
+type lname = name located
 type lstring = string
 type lreference = reference
 
@@ -147,8 +148,8 @@ type definition_expr =
       * constr_expr option
 
 type local_decl_expr =
-  | AssumExpr of lident * constr_expr
-  | DefExpr of lident * constr_expr * constr_expr option
+  | AssumExpr of lname * constr_expr
+  | DefExpr of lname * constr_expr * constr_expr option
 
 type module_binder = lident list * module_type_ast