From f3d34e3e3add974d79d14f043c19a6d76c2b71b7 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 23 Sep 2003 11:22:20 +0000
Subject: Utilisation de noms dans 'Implicit Arguments [...]'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4459 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernacexpr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 3d50683040..d142f1d878 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -234,7 +234,7 @@ type vernac_expr =
   | VernacHintDestruct of locality_flag *
       identifier * (bool,unit) location * constr_expr * int * raw_tactic_expr
   | VernacSyntacticDefinition of identifier * constr_expr * int option
-  | VernacDeclareImplicits of reference * int list option
+  | VernacDeclareImplicits of reference * explicitation list option
   | VernacReserve of identifier list * constr_expr
   | VernacSetOpacity of opacity_flag * reference list
   | VernacUnsetOption of Goptions.option_name
-- 
cgit v1.2.3