diff options
| author | Pierre-Marie Pédrot | 2016-05-02 11:34:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-02 11:34:40 +0200 |
| commit | 35d6aa4bc7c2d39bbd55d2ff5d114a03e1f284f2 (patch) | |
| tree | 613f0924d8e1004174a7658c3fd414ecf8afdb69 /mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | |
| parent | 374222f28aea5f8cdce246fb9e7b68b612a4349e (diff) | |
Fixing compilation after the merge of ML-tactic-notation branch.
Diffstat (limited to 'mathcomp/ssreflect/plugin/trunk/ssreflect.ml4')
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 14 |
1 files changed, 2 insertions, 12 deletions
diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 index f1b6766..6d512b1 100644 --- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 +++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 @@ -1035,11 +1035,7 @@ let set_pr_ssrtac name prec afmt = | ArgSep s -> Egramml.GramTerminal s | ArgSsr s -> Egramml.GramTerminal s | ArgCoq at -> Egramml.GramTerminal "COQ_ARG") afmt in - let tacname = ssrtac_name name in - Pptactic.declare_ml_tactic_pprule tacname [| - { Pptactic.pptac_level = prec; - Pptactic.pptac_prods = fmt } - |] + let tacname = ssrtac_name name in () let ssrtac_atom loc name args = TacML (loc, ssrtac_entry name 0, args) let ssrtac_expr = ssrtac_atom @@ -1725,9 +1721,8 @@ ARGUMENT EXTEND ssrhint TYPED AS ssrhintarg PRINTED BY pr_ssrhint END TACTIC EXTEND ssrtclby -| [ "YouShouldNotTypeThis" ssrhint(tac) ] -> [ Proofview.V82.tactic (hinttac ist true tac) ] +| [ "by" ssrhintarg(tac) ] -> [ Proofview.V82.tactic (hinttac ist true tac) ] END -set_pr_ssrtac "tclby" 0 [ArgSsr "hint"] (* We can't parse "by" in ARGUMENT EXTEND because it will only be made *) (* into a keyword in ssreflect.v; so we anticipate this in GEXTEND. *) @@ -1735,11 +1730,6 @@ set_pr_ssrtac "tclby" 0 [ArgSsr "hint"] GEXTEND Gram GLOBAL: ssrhint simple_tactic; ssrhint: [[ "by"; arg = ssrhintarg -> arg ]]; - simple_tactic: [ - [ "by"; arg = ssrhintarg -> - let garg = TacGeneric (in_gen (rawwit wit_ssrhint) arg) in - ssrtac_atom !@loc "tclby" [garg] - ] ]; END (* }}} *) |