diff options
Diffstat (limited to 'engine/proofview.ml')
-rw-r--r-- | engine/proofview.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index a2838a2de..f2f400515 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -929,6 +929,8 @@ module Unsafe = struct { step with comb = step.comb @ gls } end + let tclSETENV = Env.set + let tclGETGOALS = Comb.get let tclSETGOALS = Comb.set @@ -1129,6 +1131,10 @@ module Goal = struct in tclUNIT (CList.map_filter map step.comb) + let unsolved { self=self } = + tclEVARMAP >>= fun sigma -> + tclUNIT (not (Option.is_empty (advance sigma self))) + (* compatibility *) let goal { self=self } = self |