Using hashes instead of strings in dynamic tags. In case of collision, an

anomaly is raised. As there are very few tags defined in Coq code, this is
very unlikely to appear, and can be fixed by tweaking the name of the
dynamic argument.

This should be more efficient, as we did compare equal strings each time.

1 files changed, 6 insertions, 5 deletions

diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 1bba78334f..261e8583e1 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -689,11 +689,12 @@ and intern_tacarg strict onlytac ist = function
     let (_, arg) = Genintern.generic_intern ist arg in
     TacGeneric arg
   | TacDynamic(loc,t) as x ->
-      (match Dyn.tag t with
-	| "tactic" | "value" -> x
-        | "constr" -> if onlytac then error_tactic_expected loc else x
-	| s -> anomaly ~loc
-                 (str "Unknown dynamic: <" ++ str s ++ str ">"))
+    if Dyn.has_tag t "tactic" || Dyn.has_tag t "value" then x
+    else if Dyn.has_tag t "constr" then
+      if onlytac then error_tactic_expected loc else x
+    else
+      let tag = Dyn.tag t in
+      anomaly ~loc (str "Unknown dynamic: <" ++ str tag ++ str ">")
 
 (* Reads the rules of a Match Context or a Match *)
 and intern_match_rule onlytac ist = function