From 956eab0d8af124ef30cb4319f3798f6776919eca Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 6 May 2007 13:00:39 +0000
Subject: Nouveaux changements autour des implicites (notamment suite à
 discussion avec Georges)

- La notion d'insertion maximale n'est plus globale mais attachée à
  chaque implicite
- Correction de petits bugs dans le calcul des implicites
- Raffinement de la notion "sous contexte" pour l'affichage des coercions



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9817 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/xlate.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'contrib/interface')

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 0101b10967..2abdcaa19c 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -2079,10 +2079,10 @@ let rec xlate_vernac =
 	       CT_coerce_ID_LIST_to_ID_LIST_OPT
 	       (CT_id_list
 	       (List.map
-		  (function ExplByPos x
+		  (function ExplByPos x, _
 		       -> xlate_error
 			   "explication argument by rank is obsolete"
-		     | ExplByName id -> CT_ident (string_of_id id)) l)))
+		     | ExplByName id, _ -> CT_ident (string_of_id id)) l)))
   | VernacDeclareImplicits(false, id, opt_positions) ->
       xlate_error "TODO: Implicit Arguments Global"
   | VernacReserve((_,a)::l, f) ->
-- 
cgit v1.2.3