diff options
| author | Erik Martin-Dorel | 2019-03-04 01:25:39 +0100 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-04-23 20:22:05 +0200 |
| commit | bb6dc2355bcd027a3a89c40629b82eb2019eff6a (patch) | |
| tree | 97495eceee09a17c9739f8e1db532ccde54e203c /plugins/ssr/ssrcommon.ml | |
| parent | 7c598f9f1f6da2cecc70557f9f436392322fc6d9 (diff) | |
[ssr] under: Add iff support in side-conditions
Diffstat (limited to 'plugins/ssr/ssrcommon.ml')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 0b3bfab366..a05b1e3d81 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -828,10 +828,12 @@ let view_error s gv = open Locus (****************************** tactics ***********************************) -let rewritetac dir c = +let rewritetac ?(under=false) dir c = (* Due to the new optional arg ?tac, application shouldn't be too partial *) + let open Proofview.Notations in Proofview.V82.of_tactic begin - Equality.general_rewrite (dir = L2R) AllOccurrences true false c + Equality.general_rewrite (dir = L2R) AllOccurrences true false c <*> + if under then Proofview.cycle 1 else Proofview.tclUNIT () end (**********************`:********* hooks ************************************) @@ -1542,6 +1544,7 @@ end let is_construct_ref sigma c r = EConstr.isConstruct sigma c && GlobRef.equal (ConstructRef (fst(EConstr.destConstruct sigma c))) r let is_ind_ref sigma c r = EConstr.isInd sigma c && GlobRef.equal (IndRef (fst(EConstr.destInd sigma c))) r - +let is_const_ref sigma c r = + EConstr.isConst sigma c && GlobRef.equal (ConstRef (fst(EConstr.destConst sigma c))) r (* vim: set filetype=ocaml foldmethod=marker: *) |