diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-11-07 15:46:24 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-11-07 15:46:24 +0100 |
| commit | b58f5b2b499b687288587837cbf0cfc04a269c75 (patch) | |
| tree | c4186f582884cc7b295eccc163ca893c53009fb6 /parsing/g_vernac.ml4 | |
| parent | 6f30019bfd99a0125fdc12baf8b6c04169701fb7 (diff) | |
| parent | d7cb0e2115ec37eddeeecbb1f2dbdeb7e49aeb7a (diff) | |
Merge remote-tracking branch 'github/pr/339' into v8.6
Was PR#339: Documenting type class options, typeclasses eauto
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 26 |
1 files changed, 17 insertions, 9 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 8f86abcf3..9b52d1bf3 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -588,7 +588,7 @@ let warn_deprecated_arguments_syntax = (* Extensions: implicits, coercions, etc. *) GEXTEND Gram - GLOBAL: gallina_ext instance_name; + GLOBAL: gallina_ext instance_name hint_info; gallina_ext: [ [ (* Transparent and Opaque *) @@ -641,17 +641,20 @@ GEXTEND Gram | IDENT "Instance"; namesup = instance_name; ":"; expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; - pri = OPT [ "|"; i = natural -> i ] ; + info = hint_info ; props = [ ":="; "{"; r = record_declaration; "}" -> Some (true,r) | ":="; c = lconstr -> Some (false,c) | -> None ] -> - VernacInstance (false,snd namesup,(fst namesup,expl,t),props,pri) + VernacInstance (false,snd namesup,(fst namesup,expl,t),props,info) | IDENT "Existing"; IDENT "Instance"; id = global; - pri = OPT [ "|"; i = natural -> i ] -> - VernacDeclareInstances ([id], pri) + info = hint_info -> + VernacDeclareInstances [id, info] + | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global; - pri = OPT [ "|"; i = natural -> i ] -> - VernacDeclareInstances (ids, pri) + pri = OPT [ "|"; i = natural -> i ] -> + let info = { hint_priority = pri; hint_pattern = None } in + let insts = List.map (fun i -> (i, info)) ids in + VernacDeclareInstances insts | IDENT "Existing"; IDENT "Class"; is = global -> VernacDeclareClass is @@ -796,6 +799,11 @@ GEXTEND Gram (Option.default [] sup) | -> ((!@loc, Anonymous), None), [] ] ] ; + hint_info: + [ [ "|"; i = OPT natural; pat = OPT constr_pattern -> + { hint_priority = i; hint_pattern = pat } + | -> { hint_priority = None; hint_pattern = None } ] ] + ; reserv_list: [ [ bl = LIST1 reserv_tuple -> bl | b = simple_reserv -> [b] ] ] ; @@ -817,8 +825,8 @@ GEXTEND Gram (* Hack! Should be in grammar_ext, but camlp4 factorize badly *) | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":"; expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; - pri = OPT [ "|"; i = natural -> i ] -> - VernacInstance (true, snd namesup, (fst namesup, expl, t), None, pri) + info = hint_info -> + VernacInstance (true, snd namesup, (fst namesup, expl, t), None, info) (* System directory *) | IDENT "Pwd" -> VernacChdir None |