diff options
| author | Maxime Dénès | 2017-06-06 17:18:59 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-06 17:18:59 +0200 |
| commit | e5581b2a1e5b3d9fc5dc7fe95ee4ba121f5d42cd (patch) | |
| tree | 1a0d0b7d693c37ca8712057e946587584687208e /plugins/firstorder/ground.ml | |
| parent | 2f23c27e08f66402b8fba4745681becd402f4c5c (diff) | |
| parent | 0ce9cef0ac431e184c870617841bedc3f427396d (diff) | |
Merge PR#623: Remove the Sigma (monotonous state) API.
Diffstat (limited to 'plugins/firstorder/ground.ml')
| -rw-r--r-- | plugins/firstorder/ground.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index ab1dd07c11..0fa3089e73 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -14,7 +14,6 @@ open Instances open Term open Tacmach.New open Tacticals.New -open Proofview.Notations let update_flags ()= let predref=ref Names.Cpred.empty in @@ -31,10 +30,10 @@ let update_flags ()= (Names.Id.Pred.full,Names.Cpred.complement !predref) let ground_tac solver startseq = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> update_flags (); let rec toptac skipped seq = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let () = if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 then @@ -127,7 +126,7 @@ let ground_tac solver startseq = end with Heap.EmptyHeap->solver end - end } in + end in let n = List.length (Proofview.Goal.hyps gl) in startseq (fun seq -> wrap n true (toptac []) seq) - end } + end |