diff options
| author | Emilio Jesus Gallego Arias | 2018-07-11 01:33:53 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-07-11 01:33:53 +0200 |
| commit | e372f0e5f0646eb4209baa06c874b4f041ed6574 (patch) | |
| tree | 0eb3b9bc736d4e5cdcd022b315cf7c2a4f0731a0 /plugins/ssr | |
| parent | d47ddf56bc93ae16280ce8a845a4b004fef52fb8 (diff) | |
| parent | a9728d5a43e5c82fed9cac25e841107c4c95fc35 (diff) | |
Merge PR #7898: Remove camlp4 remains
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrparser.ml4 | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrparser.mli | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 6b183dab1c..8b9c94f2db 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -1408,7 +1408,7 @@ let check_seqtacarg dir arg = match snd arg, dir with CErrors.user_err ?loc (str "expected \"first\"") | _, _ -> arg -let ssrorelse = Gram.entry_create "ssrorelse" +let ssrorelse = Entry.create "ssrorelse" GEXTEND Gram GLOBAL: ssrorelse ssrseqarg; ssrseqidx: [ diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index 7cd3751cef..862a93765d 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -12,11 +12,11 @@ open Ltac_plugin -val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry +val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type val pr_ssrtacarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c) -> 'c -val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry +val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type val pr_ssrtclarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c -> 'd) -> 'c -> 'd |