diff options
| author | Matthieu Sozeau | 2016-06-09 23:24:57 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-06-16 18:21:08 +0200 |
| commit | 2194292dbe88674fd9a606bb22f28d332f670f77 (patch) | |
| tree | 21c2e91b13a5de21856554b17f5dfaa61101e253 /ltac | |
| parent | af7a9a4e44739968b68aeb1cb0a1f70a1aa34e88 (diff) | |
Revise syntax of Hint Cut
As noticed by C. Cohen it was confusingly different from standard
notation.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/g_auto.ml4 | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4 index df7e763470..8bc2ffd654 100644 --- a/ltac/g_auto.ml4 +++ b/ltac/g_auto.ml4 @@ -175,8 +175,8 @@ let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom ARGUMENT EXTEND hints_path_atom PRINTED BY pr_hints_path_atom -| [ global_list(g) ] -> [ Hints.PathHints (List.map Nametab.global g) ] -| [ "*" ] -> [ Hints.PathAny ] +| [ ne_global_list(g) ] -> [ Hints.PathHints (List.map Nametab.global g) ] +| [ "_" ] -> [ Hints.PathAny ] END let pr_hints_path prc prx pry c = Hints.pp_hints_path c @@ -184,12 +184,12 @@ let pr_hints_path prc prx pry c = Hints.pp_hints_path c ARGUMENT EXTEND hints_path PRINTED BY pr_hints_path | [ "(" hints_path(p) ")" ] -> [ p ] -| [ "!" hints_path(p) ] -> [ Hints.PathStar p ] +| [ hints_path(p) "*" ] -> [ Hints.PathStar p ] | [ "emp" ] -> [ Hints.PathEmpty ] | [ "eps" ] -> [ Hints.PathEpsilon ] -| [ hints_path_atom(a) ] -> [ Hints.PathAtom a ] | [ hints_path(p) "|" hints_path(q) ] -> [ Hints.PathOr (p, q) ] -| [ hints_path(p) ";" hints_path(q) ] -> [ Hints.PathSeq (p, q) ] +| [ hints_path_atom(a) ] -> [ Hints.PathAtom a ] +| [ hints_path(p) hints_path(q) ] -> [ Hints.PathSeq (p, q) ] END let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases |