diff options
| author | Pierre-Marie Pédrot | 2020-09-23 11:00:50 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-23 11:00:50 +0200 |
| commit | bb6e78ef2ca4bf0d686654fa3f66dd780f5be0ac (patch) | |
| tree | ce14f693e58487503870c53d7a186bf7ca66a1f6 /plugins/ssr | |
| parent | 23b0dbb3a0a71edd9ce2137e88b715c3e36e576f (diff) | |
| parent | fb144f860a0034103ad0470b8982639277baac1b (diff) | |
Merge PR #13028: Fixes #9716 and #13004: don't drop the qualifier of quotations at printing time
Reviewed-by: ppedrot
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) ] -> { |