From 8239ab05c0281dc01817ee9e932e9958dc5e32e1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 24 Nov 2016 09:12:12 +0100
Subject: [PATCH] ProofMode intro patterns: accept _ as part of variable names

---
 proofmode/intro_patterns.v | 5 ++---
 proofmode/spec_patterns.v  | 1 +
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/proofmode/intro_patterns.v b/proofmode/intro_patterns.v
index b999e0be3..54a95c724 100644
--- a/proofmode/intro_patterns.v
+++ b/proofmode/intro_patterns.v
@@ -29,7 +29,6 @@ Module intro_pat.
 Inductive token :=
   | TName : string → token
   | TAnom : token
-  | TDrop : token
   | TFrame : token
   | TBar : token
   | TBracketL : token
@@ -55,7 +54,6 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
   match s with
   | "" => rev (cons_name kn k)
   | String "?" s => tokenize_go s (TAnom :: cons_name kn k) ""
-  | String "_" s => tokenize_go s (TDrop :: cons_name kn k) ""
   | String "$" s => tokenize_go s (TFrame :: cons_name kn k) ""
   | String "[" s => tokenize_go s (TBracketL :: cons_name kn k) ""
   | String "]" s => tokenize_go s (TBracketR :: cons_name kn k) ""
@@ -77,6 +75,7 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
   | String a s =>
      if is_space a then tokenize_go s (cons_name kn k) ""
      else tokenize_go s k (String a kn)
+  (* TODO: Complain about invalid characters, to future-proof this against making more characters special. *)
   end.
 Definition tokenize (s : string) : list token := tokenize_go s [] "".
 
@@ -129,9 +128,9 @@ Fixpoint close_conj_list (k : stack)
 Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
   match ts with
   | [] => Some k
+  | TName "_" :: ts => parse_go ts (SPat IDrop :: k)
   | TName s :: ts => parse_go ts (SPat (IName s) :: k)
   | TAnom :: ts => parse_go ts (SPat IAnom :: k)
-  | TDrop :: ts => parse_go ts (SPat IDrop :: k)
   | TFrame :: ts => parse_go ts (SPat IFrame :: k)
   | TBracketL :: ts => parse_go ts (SList :: k)
   | TBar :: ts => parse_go ts (SBar :: k)
diff --git a/proofmode/spec_patterns.v b/proofmode/spec_patterns.v
index 25c548311..d482d245b 100644
--- a/proofmode/spec_patterns.v
+++ b/proofmode/spec_patterns.v
@@ -42,6 +42,7 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
   | String a s =>
      if is_space a then tokenize_go s (cons_name kn k) ""
      else tokenize_go s k (String a kn)
+  (* TODO: Complain about invalid characters, to future-proof this against making more characters special. *)
   end.
 Definition tokenize (s : string) : list token := tokenize_go s [] "".
 
-- 
GitLab