diff options
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrparser.mlg | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 60af804c1b..b32b58062a 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -219,20 +219,20 @@ let test_ssrslashnum b1 b2 _ strm = match Util.stream_nth 0 strm with | Tok.KEYWORD "/" -> (match Util.stream_nth 1 strm with - | Tok.NUMERAL _ when b1 -> + | Tok.NUMBER _ when b1 -> (match Util.stream_nth 2 strm with | Tok.KEYWORD "=" | Tok.KEYWORD "/=" when not b2 -> () | Tok.KEYWORD "/" -> if not b2 then () else begin match Util.stream_nth 3 strm with - | Tok.NUMERAL _ -> () + | Tok.NUMBER _ -> () | _ -> raise Stream.Failure end | _ -> raise Stream.Failure) | Tok.KEYWORD "/" when not b1 -> (match Util.stream_nth 2 strm with | Tok.KEYWORD "=" when not b2 -> () - | Tok.NUMERAL _ when b2 -> + | Tok.NUMBER _ when b2 -> (match Util.stream_nth 3 strm with | Tok.KEYWORD "=" -> () | _ -> raise Stream.Failure) @@ -243,7 +243,7 @@ let test_ssrslashnum b1 b2 _ strm = | Tok.KEYWORD "//" when not b1 -> (match Util.stream_nth 1 strm with | Tok.KEYWORD "=" when not b2 -> () - | Tok.NUMERAL _ when b2 -> + | Tok.NUMBER _ when b2 -> (match Util.stream_nth 2 strm with | Tok.KEYWORD "=" -> () | _ -> raise Stream.Failure) @@ -1682,7 +1682,7 @@ let set_pr_ssrtac name prec afmt = (* FIXME *) () (* let ssrtac_expr ?loc name args = TacML (CAst.make ?loc (ssrtac_entry name, args)) let tclintros_expr ?loc tac ipats = - let args = [Tacexpr.TacGeneric (in_gen (rawwit wit_ssrintrosarg) (tac, ipats))] in + let args = [Tacexpr.TacGeneric (None, in_gen (rawwit wit_ssrintrosarg) (tac, ipats))] in ssrtac_expr ?loc "tclintros" args } @@ -1777,7 +1777,7 @@ let _ = set_pr_ssrtac "tcldo" 3 [ArgSep "do "; ArgSsr "doarg"] let ssrdotac_expr ?loc n m tac clauses = let arg = ((n, m), tac), clauses in - ssrtac_expr ?loc "tcldo" [Tacexpr.TacGeneric (in_gen (rawwit wit_ssrdoarg) arg)] + ssrtac_expr ?loc "tcldo" [Tacexpr.TacGeneric (None, in_gen (rawwit wit_ssrdoarg) arg)] } @@ -1828,7 +1828,7 @@ let tclseq_expr ?loc tac dir arg = let arg1 = in_gen (rawwit wit_ssrtclarg) tac in let arg2 = in_gen (rawwit wit_ssrseqdir) dir in let arg3 = in_gen (rawwit wit_ssrseqarg) (check_seqtacarg dir arg) in - ssrtac_expr ?loc "tclseq" (List.map (fun x -> Tacexpr.TacGeneric x) [arg1; arg2; arg3]) + ssrtac_expr ?loc "tclseq" (List.map (fun x -> Tacexpr.TacGeneric (None, x)) [arg1; arg2; arg3]) } @@ -2451,7 +2451,7 @@ GRAMMAR EXTEND Gram tactic_expr: LEVEL "3" [ RIGHTA [ IDENT "abstract"; gens = ssrdgens -> { ssrtac_expr ~loc "abstract" - [Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit wit_ssrdgens) gens)] } ]]; + [Tacexpr.TacGeneric (None, Genarg.in_gen (Genarg.rawwit wit_ssrdgens) gens)] } ]]; END TACTIC EXTEND ssrabstract | [ "abstract" ssrdgens(gens) ] -> { |