diff options
| author | Erik Martin-Dorel | 2019-02-24 18:30:00 +0100 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-04-23 12:54:43 +0200 |
| commit | 1a5a4c9c8cacea6e6ed7ced8766cadb0195655d9 (patch) | |
| tree | 59a11ed356a3fedf837d7d555bc4011345086e15 /plugins | |
| parent | 527e6a97d1429a58273ddc6b4ce2826df0dba1c6 (diff) | |
[ssr] under: Add support for one-liners "under (…) by [tac1|tac2]."
Supported syntax:
under i: eq_bigr by rewrite adnnC. (* ensure 1 Under subogal is created *)
under i: eq_big by [rewrite adnnC | rewrite addnC]. (* 2 Under subgoals *)
Equivalent, expanded form:
under i: eq_bigr; [rewrite adnnC; over | idtac].
under i: eq_big; [rewrite adnnC; over | rewrite adnnC; over | idtac].
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssr/ssrfwd.ml | 18 | ||||
| -rw-r--r-- | plugins/ssr/ssrfwd.mli | 3 | ||||
| -rw-r--r-- | plugins/ssr/ssrparser.mlg | 4 |
3 files changed, 19 insertions, 6 deletions
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 29983e7504..570b5a8c61 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -393,7 +393,9 @@ let rec pretty_rename evar_map term = function ppdebug(lazy Pp.(str"under: cannot pretty-rename all bound variables with destLambda")); term -let undertac ist varnames ((dir,mult),_ as rule) = +let overtac gl = ssr_n_tac "over" ~-1 gl + +let undertac ist varnames ((dir,mult),_ as rule) hint = if mult <> Ssrequality.nomult then Ssrcommon.errorstrm Pp.(str"Multiplicity not supported"); @@ -418,5 +420,15 @@ let undertac ist varnames ((dir,mult),_ as rule) = ppdebug(lazy Pp.(str"under: to:" ++ pr_econstr_env env evar_map new_t)); evar_map, new_t in - Proofview.V82.tactic (Ssrequality.ssrrewritetac ~under:true ~map_redex ist [rule]) <*> - intro_lock varnames + let undertacs = + if hint = nohint then + Proofview.tclUNIT () + else + Proofview.tclDISPATCH + ((List.map (function None -> Proofview.V82.tactic overtac + | Some e -> ssrevaltac ist e <*> + Proofview.V82.tactic overtac) + (if hint = nullhint then [None] else snd hint)) @ [Proofview.tclUNIT ()]) + in + (Proofview.V82.tactic (Ssrequality.ssrrewritetac ~under:true ~map_redex ist [rule]) <*> + intro_lock varnames <*> undertacs) diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli index fe7d84871e..63df8f5349 100644 --- a/plugins/ssr/ssrfwd.mli +++ b/plugins/ssr/ssrfwd.mli @@ -59,4 +59,5 @@ val sufftac : val undertac : Ltac_plugin.Tacinterp.interp_sign -> - Names.Id.t list -> Ssrequality.ssrrwarg -> unit Proofview.tactic + Names.Id.t list -> Ssrequality.ssrrwarg -> + Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint -> unit Proofview.tactic diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index e63d1e5562..507cf8db70 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -2651,8 +2651,8 @@ TACTIC EXTEND ssrgenhave2 END TACTIC EXTEND under - | [ "under" ne_ident_list(names) ":" ssrrwarg(r) ] -> - { Ssrfwd.undertac ist names r } + | [ "under" ne_ident_list(names) ":" ssrrwarg(r) ssrhint(hint) ] -> + { Ssrfwd.undertac ist names r hint } END { |