diff options
| author | Enrico Tassi | 2019-01-17 18:00:08 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-01-18 19:05:36 +0100 |
| commit | 762a47bce085bf1606a05c7b59c8a59803730eeb (patch) | |
| tree | 7af15d2d6e045d73fe36de5e57267536d9f80831 /plugins | |
| parent | 2f3db0b605b3aa345c1fea26c263ba6793a0fa51 (diff) | |
[ssr] compile "=> {x..}/v" as "/v{x..v}"
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssr/ssripats.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index ce5fccec96..f10a25dac8 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -439,7 +439,8 @@ let rec ipat_tac1 ipat : bool tactic = ~conclusion:(fun ~to_clear:clr -> let inter = CList.intersect Id.equal clr extra_clear in List.iter duplicate_clear inter; - intro_clear (clr @ extra_clear)) + let cl = CList.union Id.equal clr extra_clear in + intro_clear cl) | IOpDispatchBranches ipatss -> tclDISPATCH (List.map ipat_tac ipatss) <*> notTAC @@ -525,10 +526,8 @@ and split_at_first_case ipats = let tclCompileIPats l = let rec elab = function - | (IPatClear []) :: (IPatView v) :: rest -> - (IOpView(Some [],v)) :: elab rest | (IPatClear cl) :: (IPatView v) :: rest -> - (IOpView(None,v)) :: IOpClear cl :: elab rest + (IOpView(Some cl,v)) :: elab rest | (IPatClear []) :: (IPatId id) :: rest -> (IOpClear [SsrHyp(None,id)]) :: IOpId id :: elab rest |