diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-05-15 13:39:08 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-06-22 11:07:08 +0200 |
| commit | a9dc951e9068b18ee1cf0e51b2c4ae7a7c40354a (patch) | |
| tree | a1a4073e5cab0d9af97c129a1574b0549464cc6d /plugins/ssr/ssripats.ml | |
| parent | 7721aeeede9c5578f29e7f37a5ea2005c7d9ce1b (diff) | |
[ssr] implement {}/v as a short hand for {v}/v when v is an id
Diffstat (limited to 'plugins/ssr/ssripats.ml')
| -rw-r--r-- | plugins/ssr/ssripats.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 09f3899ec..46fde4115 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -212,8 +212,8 @@ let tclLOG p t = let rec ipat_tac1 ipat : unit tactic = match ipat with - | IPatView l -> - Ssrview.tclIPAT_VIEWS ~views:l + | IPatView (clear_if_id,l) -> + Ssrview.tclIPAT_VIEWS ~views:l ~clear_if_id ~conclusion:(fun ~to_clear:clr -> intro_clear clr) | IPatDispatch ipatss -> tclEXTEND (List.map ipat_tac ipatss) (tclUNIT ()) [] @@ -588,7 +588,7 @@ let ssrmovetac = function (tacVIEW_THEN_GRAB view ~conclusion) <*> tclIPAT (IPatClear clr :: ipats) | _::_ as view, (_, ({ gens = []; clr }, ipats)) -> - tclIPAT (IPatView view :: IPatClear clr :: ipats) + tclIPAT (IPatView (false,view) :: IPatClear clr :: ipats) | _, (Some pat, (dgens, ipats)) -> let dgentac = with_dgens dgens eqmovetac in dgentac <*> tclIPAT (eqmoveipats pat ipats) |