diff options
| author | Hugo Herbelin | 2020-09-15 21:24:39 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-09-22 18:22:12 +0200 |
| commit | d286c3601e24afe0a681d092cbd880773872b980 (patch) | |
| tree | cad1afcff0fbfbcb3c91a82fc3cf75bdee6e73d8 /plugins/ssr | |
| parent | c3a73c5e923953efea016a81d380e58b2cccb4f9 (diff) | |
Fixes #9716, #13004: don't drop the qualifier of quotations at printing time.
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrparser.mlg | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 98439e27a1..b32b58062a 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -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) ] -> { |