diff --git a/proofmode/sel_patterns.v b/proofmode/sel_patterns.v index 1f1f9229d0b8490df5119f0f97d939f81b08d4d5..75aa2ee4934497054f859ca2bbe0a76131f40d69 100644 --- a/proofmode/sel_patterns.v +++ b/proofmode/sel_patterns.v @@ -24,8 +24,8 @@ Fixpoint parse_go (s : string) (k : list sel_pat) (kn : string) : list sel_pat : | String "%" s => parse_go s (SelPure :: cons_name kn k) "" | String "#" s => parse_go s (SelPersistent :: cons_name kn k) "" | String (Ascii.Ascii false true false false false true true true) (* unicode ∗ *) - (String (Ascii.Ascii false false false true true false false true) - (String (Ascii.Ascii true false true false false false false true) s)) => + (String (Ascii.Ascii false false false true false false false true) + (String (Ascii.Ascii true true true false true false false true) s)) => parse_go s (SelSpatial :: cons_name kn k) "" | String a s => parse_go s k (String a kn) end.