- Remove useless grammar rule

- Better printing of unif constraints in evar_map's

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

2 files changed, 22 insertions, 13 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 15f81c7237..f405600064 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -46,7 +46,6 @@ let class_rawexpr = Gram.entry_create "vernac:class_rawexpr"
 let thm_token = Gram.entry_create "vernac:thm_token"
 let def_body = Gram.entry_create "vernac:def_body"
 let decl_notation = Gram.entry_create "vernac:decl_notation"
-let typeclass_context = Gram.entry_create "vernac:typeclass_context"
 let record_field = Gram.entry_create "vernac:record_field"
 let of_type_with_opt_coercion = Gram.entry_create "vernac:of_type_with_opt_coercion"
 let subgoal_command = Gram.entry_create "proof_mode:subgoal_command"
@@ -139,7 +138,7 @@ let test_plurial_form_types = function
 (* Gallina declarations *)
 GEXTEND Gram
   GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion
-    typeclass_context typeclass_constraint record_field decl_notation rec_definition;
+    typeclass_constraint record_field decl_notation rec_definition;
 
   gallina:
       (* Definition, Theorem, Variable, Axiom, ... *)
@@ -179,10 +178,6 @@ GEXTEND Gram
 	    VernacInductive (indf,infer,[((oc,name),ps,s,recf,cfs),[]])
   ] ]
   ;
-  typeclass_context:
-    [ [ "["; l=LIST1 typeclass_constraint SEP ","; "]" -> l
-    | -> [] ] ]
-  ;
   thm_token:
     [ [ "Theorem" -> Theorem
       | IDENT "Lemma" -> Lemma
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 4e1795a978..838f204257 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -142,7 +142,10 @@ module EvarInfoMap = struct
   let define (def,undef) evk body =
     let oldinfo =
       try ExistentialMap.find evk undef
-      with Not_found -> anomaly "Evd.define: cannot define undeclared evar" in
+      with Not_found -> 
+	try ExistentialMap.find evk def
+	with Not_found -> 
+	  anomaly "Evd.define: cannot define undeclared evar" in
     let newinfo =
       { oldinfo with
 	  evar_body = Evar_defined body } in
@@ -772,14 +775,25 @@ let pr_evar_map_t (evars,(uvs,univs) as sigma) =
       h 0 (Univ.pr_universes univs)++fnl()
   in evs ++ svs ++ cs
 
+let print_env_short env =
+  let pr_body = function None -> mt () | Some b -> str " := " ++ print_constr b in
+  let pr_named_decl (n, b, _) = pr_id n ++ pr_body b in
+  let pr_rel_decl (n, b, _) = pr_name n ++ pr_body b in
+  let nc = List.rev (named_context env) in
+  let rc = List.rev (rel_context env) in
+    str "[" ++ prlist_with_sep pr_spc pr_named_decl nc ++ str "]" ++ spc () ++
+    str "[" ++ prlist_with_sep pr_spc pr_rel_decl rc ++ str "]"
+
 let pr_constraints pbs =
   h 0
-    (prlist_with_sep pr_fnl (fun (pbty,_,t1,t2) ->
-      print_constr t1 ++ spc() ++
-      str (match pbty with
-	| Reduction.CONV -> "=="
-	| Reduction.CUMUL -> "<=") ++
-      spc() ++ print_constr t2) pbs)
+    (prlist_with_sep pr_fnl 
+       (fun (pbty,env,t1,t2) ->
+	  print_env_short env ++ spc () ++ str "|-" ++ spc () ++
+	    print_constr t1 ++ spc() ++
+	    str (match pbty with
+		 | Reduction.CONV -> "=="
+		 | Reduction.CUMUL -> "<=") ++
+	    spc() ++ print_constr t2) pbs)
 
 let pr_evar_map_constraints evd =
   if evd.conv_pbs = [] then mt()