More Proofview.Goal.enter.

Proofview.Goal.enter is meant to eventually replace the Goal.sensitive monad.

This commit changes the type of Proofview.Goal.enter from taking a four argument function (environment, evar_map, hyps, concl) from a one argument function of abstract type Proofview.Goal.t. It will be both more extensible and more akin to old-style tactics.

This commit also changes the type of Proofview.Goal.{concl,hyps,env} from monadic operations to projection from a Proofview.Goal.t.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17000 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 37 insertions, 33 deletions

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 440309284..8232604f7 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -217,41 +217,45 @@ module Btauto = struct
     Tacticals.tclFAIL 0 msg gl
 
   let try_unification env =
-    Proofview.Goal.concl >>= fun concl ->
-    let eq = Lazy.force eq in
-    let t = decomp_term concl in
-    match t with
-    | Term.App (c, [|typ; p; _|]) when c === eq ->
+    Proofview.Goal.enter begin fun gl ->
+      let concl = Proofview.Goal.concl gl in
+      let eq = Lazy.force eq in
+      let t = decomp_term concl in
+      match t with
+      | Term.App (c, [|typ; p; _|]) when c === eq ->
       (* should be an equality [@eq poly ?p (Cst false)] *)
-      let tac = Tacticals.New.tclORELSE0 Tactics.reflexivity (Proofview.V82.tactic (print_counterexample p env)) in
-      tac
-    | _ ->
-      let msg = str "Btauto: Internal error" in
-      Tacticals.New.tclFAIL 0 msg
+          let tac = Tacticals.New.tclORELSE0 Tactics.reflexivity (Proofview.V82.tactic (print_counterexample p env)) in
+          tac
+      | _ ->
+          let msg = str "Btauto: Internal error" in
+          Tacticals.New.tclFAIL 0 msg
+    end
 
   let tac =
-    Proofview.Goal.concl >>= fun concl ->
-    let eq = Lazy.force eq in
-    let bool = Lazy.force Bool.typ in
-    let t = decomp_term concl in
-    match t with
-    | Term.App (c, [|typ; tl; tr|])
-        when typ === bool && c === eq ->
-      let env = Env.empty () in
-      let fl = Bool.quote env tl in
-      let fr = Bool.quote env tr in
-      let env = Env.to_list env in
-      let fl = reify env fl in
-      let fr = reify env fr in
-      let changed_gl = Term.mkApp (c, [|typ; fl; fr|]) in
-      Tacticals.New.tclTHENLIST [
-        Proofview.V82.tactic (Tactics.change_in_concl None changed_gl);
-        Proofview.V82.tactic (Tactics.apply (Lazy.force soundness));
-        Proofview.V82.tactic (Tactics.normalise_vm_in_concl);
-        try_unification env
-      ]
-    | _ ->
-      let msg = str "Cannot recognize a boolean equality" in
-      Tacticals.New.tclFAIL 0 msg
+    Proofview.Goal.enter begin fun gl ->
+      let concl = Proofview.Goal.concl gl in
+      let eq = Lazy.force eq in
+      let bool = Lazy.force Bool.typ in
+      let t = decomp_term concl in
+      match t with
+      | Term.App (c, [|typ; tl; tr|])
+          when typ === bool && c === eq ->
+          let env = Env.empty () in
+          let fl = Bool.quote env tl in
+          let fr = Bool.quote env tr in
+          let env = Env.to_list env in
+          let fl = reify env fl in
+          let fr = reify env fr in
+          let changed_gl = Term.mkApp (c, [|typ; fl; fr|]) in
+          Tacticals.New.tclTHENLIST [
+            Proofview.V82.tactic (Tactics.change_in_concl None changed_gl);
+            Proofview.V82.tactic (Tactics.apply (Lazy.force soundness));
+            Proofview.V82.tactic (Tactics.normalise_vm_in_concl);
+            try_unification env
+          ]
+      | _ ->
+          let msg = str "Cannot recognize a boolean equality" in
+          Tacticals.New.tclFAIL 0 msg
+    end
 
 end