diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-10-14 17:58:31 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-10-14 17:58:31 +0200 |
| commit | d06cea3ce4526736b5d32ba1780dbbc87c37c981 (patch) | |
| tree | 2c2ea5a4633a41cfd4451e1eefb79c171312c881 /toplevel/vernacexpr.ml | |
| parent | aae7cec8d7f5048215b7ed06a8e94cb032bfd21a (diff) | |
| parent | 8f4d4c66134804bbf2d2fe65c893b68387272d31 (diff) | |
Merge commit 'upstream/8.3+dfsg' into experimental/master
Diffstat (limited to 'toplevel/vernacexpr.ml')
| -rw-r--r-- | toplevel/vernacexpr.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 5eb220cb..b5af665c 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacexpr.ml 13332 2010-07-26 22:12:43Z msozeau $ i*) +(*i $Id: vernacexpr.ml 13492 2010-10-04 21:20:01Z herbelin $ i*) open Util open Names @@ -313,7 +313,7 @@ type vernac_expr = | VernacSyntacticDefinition of identifier located * (identifier list * constr_expr) * locality_flag * onlyparsing_flag | VernacDeclareImplicits of locality_flag * reference or_by_notation * - (explicitation * bool * bool) list option + (explicitation * bool * bool) list list | VernacReserve of simple_binder list | VernacGeneralizable of locality_flag * (lident list) option | VernacSetOpacity of |