diff options
| author | Pierre Letouzey | 2014-12-09 12:48:32 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2014-12-09 14:27:21 +0100 |
| commit | af84e080ff674a3d5cf2cf88874ddb6ebaf38ecf (patch) | |
| tree | b8325cd8ce34dd2dcfba2792a0123cf8c46ab703 /parsing | |
| parent | 9c24cecec3a7381cd924c56ca50c77a49750e2e5 (diff) | |
Switch the few remaining iso-latin-1 files to utf8
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index a6eefd3755..07ce048ead 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -817,7 +817,7 @@ GEXTEND Gram | IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path"; dir = ne_string -> VernacAddMLPath (true, dir) - (* Pour intervenir sur les tables de paramètres *) + (* For acting on parameter tables *) | "Set"; table = option_table; v = option_value -> VernacSetOption (table,v) | "Set"; table = option_table -> @@ -830,10 +830,10 @@ GEXTEND Gram | IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 option_ref_value -> VernacAddOption ([table;field], v) - (* Un value global ci-dessous va être caché par un field au dessus! *) - (* En fait, on donne priorité aux tables secondaires *) - (* Pas de syntaxe pour les tables tertiaires pour cause de conflit *) - (* (mais de toutes façons, pas utilisées) *) + (* A global value below will be hidden by a field above! *) + (* In fact, we give priority to secondary tables *) + (* No syntax for tertiary tables due to conflict *) + (* (but they are unused anyway) *) | IDENT "Add"; table = IDENT; v = LIST1 option_ref_value -> VernacAddOption ([table], v) |