From 2194292dbe88674fd9a606bb22f28d332f670f77 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 9 Jun 2016 23:24:57 +0200
Subject: Revise syntax of Hint Cut

As noticed by C. Cohen it was confusingly different from standard
notation.
---
 ltac/g_auto.ml4 | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'ltac')

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
-- 
cgit v1.2.3