error if binder was already defined

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

3 files changed, 55 insertions, 32 deletions

diff --git a/Makefile b/Makefile
index 5064709709..45d4b9b710 100644
--- a/Makefile
+++ b/Makefile
@@ -1307,7 +1307,7 @@ GRAMMARNEEDEDCMO=\
   parsing/coqast.cmo parsing/ast.cmo \
   parsing/ast.cmo parsing/lexer.cmo parsing/q_util.cmo parsing/extend.cmo \
   toplevel/vernacexpr.cmo parsing/pcoq.cmo parsing/q_coqast.cmo \
-  parsing/egrammar.cmo \
+  parsing/egrammar.cmo
 
 CAMLP4EXTENSIONSCMO=\
   parsing/argextend.cmo parsing/tacextend.cmo parsing/vernacextend.cmo 
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 35de784e78..1214663346 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -284,7 +284,7 @@ let meta_of_binder clause loc b t mvs =
 	  errorlabstrm "clenv_match_args" 
 	    (str "The variable " ++ pr_id s ++ 
 	     str " occurs more than once in binding");
-	meta_with_name clause.env s
+        meta_with_name clause.env s
     | AnonHyp n ->
 	if List.exists (fun (_,b',_) -> b=b') t then
 	  errorlabstrm "clenv_match_args"
@@ -294,29 +294,45 @@ let meta_of_binder clause loc b t mvs =
 	with (Failure _|Invalid_argument _) ->
           errorlabstrm "clenv_match_args" (str "No such binder")
 
+let error_already_defined b =
+  match b with
+      NamedHyp id ->
+        errorlabstrm "clenv_match_args"
+          (str "Binder name \"" ++ pr_id id ++
+           str"\" already defined with incompatible value")
+    | AnonHyp n ->
+        anomalylabstrm "clenv_match_args"
+          (str "Position " ++ int n ++ str" already defined")
+
 let clenv_match_args s clause =
   let mvs = clenv_independent clause in 
   let rec matchrec clause = function
     | [] -> clause
     | (loc,b,c)::t ->
 	let k = meta_of_binder clause loc b t mvs in
-	let k_typ = clenv_hnf_constr clause (clenv_meta_type clause k)
-	(* nf_betaiota was before in type_of - useful to reduce types like *)
-	(* (x:A)([x]P u) *)
-	and c_typ =
-          clenv_hnf_constr clause (nf_betaiota (clenv_get_type_of clause c)) in
-	let cl =
-	  (* Try to infer some Meta/Evar from the type of [c] *)
-	  try clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause)
-	  with e when precatchable_exception e ->
-	  (* Try to coerce to the type of [k]; cannot merge with the
-	     previous case because Coercion does not handle Meta *)
-            let (_,c') = w_coerce (cl_env clause) c c_typ k_typ clause.env in
-	    try clenv_unify true CONV (mkMeta k) c' clause
-	    with PretypeError (env,CannotUnify (m,n)) ->
-	      Stdpp.raise_with_loc loc
- 	        (PretypeError (env,CannotUnifyBindingType (m,n)))
-	in matchrec cl t
+        if meta_defined clause.env k then
+          if eq_constr (meta_fvalue clause.env k).rebus c then
+            matchrec clause t
+          else error_already_defined b
+        else
+	  let k_typ = clenv_hnf_constr clause (clenv_meta_type clause k)
+	    (* nf_betaiota was before in type_of - useful to reduce
+               types like (x:A)([x]P u) *)
+	  and c_typ =
+            clenv_hnf_constr clause
+              (nf_betaiota (clenv_get_type_of clause c)) in
+	  let cl =
+	    (* Try to infer some Meta/Evar from the type of [c] *)
+	    try clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause)
+	    with e when precatchable_exception e ->
+	      (* Try to coerce to the type of [k]; cannot merge with the
+	         previous case because Coercion does not handle Meta *)
+              let (_,c') = w_coerce (cl_env clause) c c_typ k_typ clause.env in
+	      try clenv_unify true CONV (mkMeta k) c' clause
+	      with PretypeError (env,CannotUnify (m,n)) ->
+	        Stdpp.raise_with_loc loc
+ 	          (PretypeError (env,CannotUnifyBindingType (m,n)))
+	  in matchrec cl t
   in 
   matchrec clause s
 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 9799989870..e9c60e18ec 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -173,8 +173,8 @@ let map_clb f = function
 
 (* name of defined is erased (but it is pretty-printed) *)
 let clb_name = function
-    Cltyp(na,_) -> na
-  | Clval _ -> Anonymous
+    Cltyp(na,_) -> (na,false)
+  | Clval (na,_,_) -> (na,true)
 
 (***********************)
                                                                                
@@ -293,25 +293,32 @@ let meta_assign mv v evd =
           metas = Metamap.add mv (Clval(na,mk_freelisted v, ty)) evd.metas }
     | _ -> anomaly "meta_assign: already defined"
 
+(* If the meta is defined then forget its name *)
 let meta_name evd mv =
-  try clb_name (Metamap.find mv evd.metas)
+  try
+    let (na,def) = clb_name (Metamap.find mv evd.metas) in
+    if def then Anonymous else na
   with Not_found -> Anonymous
 
 let meta_with_name evd id =
   let na = Name id in
-  let mvl =
-    Metamap.fold (fun n clb l -> if clb_name clb = na then n::l else l)
-      evd.metas [] in
-  match mvl with
-    | []  -> 
+  let (mvl,mvnodef) =
+    Metamap.fold
+      (fun n clb (l1,l2 as l) ->
+        let (na',def) = clb_name clb in
+        if na = na' then if def then (n::l1,l2) else (n::l1,n::l2)
+        else l)
+      evd.metas ([],[]) in
+  match mvnodef, mvl with
+    | _,[]  -> 
 	errorlabstrm "Evd.meta_with_name"
           (str"No such bound variable " ++ pr_id id)
-    | [n] -> 
+    | ([n],_|_,[n]) -> 
 	n
-    |  _  -> 
-	 errorlabstrm "Evd.meta_with_name"
-           (str "Binder name \"" ++ pr_id id ++
-            str"\" occurs more than once in clause")
+    | _  -> 
+	errorlabstrm "Evd.meta_with_name"
+          (str "Binder name \"" ++ pr_id id ++
+           str"\" occurs more than once in clause")
 
 
 let meta_merge evd1 evd2 =