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, 24 insertions, 20 deletions

diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index 0a6e7a0724..a0e8fcb884 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -130,16 +130,18 @@ let solveArg eqonleft op a1 a2 tac =
 let solveEqBranch rectype =
   Proofview.tclORELSE
     begin
-      Proofview.Goal.concl >>= fun concl ->
-      match_eqdec concl >= fun (eqonleft,op,lhs,rhs,_) ->
-      let (mib,mip) = Global.lookup_inductive rectype in
-      let nparams   = mib.mind_nparams in
-      let getargs l = List.skipn nparams (snd (decompose_app l)) in
-      let rargs   = getargs rhs
-      and largs   = getargs lhs in
-      List.fold_right2
-        (solveArg eqonleft op) largs rargs
-        (Tacticals.New.tclTHEN (choose_eq eqonleft) h_reflexivity)
+      Proofview.Goal.enter begin fun gl ->
+        let concl = Proofview.Goal.concl gl in
+        match_eqdec concl >= fun (eqonleft,op,lhs,rhs,_) ->
+          let (mib,mip) = Global.lookup_inductive rectype in
+          let nparams   = mib.mind_nparams in
+          let getargs l = List.skipn nparams (snd (decompose_app l)) in
+          let rargs   = getargs rhs
+          and largs   = getargs lhs in
+          List.fold_right2
+            (solveArg eqonleft op) largs rargs
+            (Tacticals.New.tclTHEN (choose_eq eqonleft) h_reflexivity)
+      end
     end
     begin function
       | PatternMatchingFailure -> Proofview.tclZERO (UserError ("",Pp.str"Unexpected conclusion!"))
@@ -155,16 +157,18 @@ let hd_app c = match kind_of_term c with
 let decideGralEquality =
   Proofview.tclORELSE
     begin
-      Proofview.Goal.concl >>= fun concl ->
-      match_eqdec concl >= fun eqonleft,_,c1,c2,typ ->
-      Tacmach.New.of_old (fun g -> hd_app (pf_compute g typ)) >>= fun headtyp ->
-      begin match kind_of_term headtyp with
-      | Ind mi -> Proofview.tclUNIT mi
-      | _ -> Proofview.tclZERO (UserError ("",Pp.str"This decision procedure only works for inductive objects."))
-      end >= fun rectype ->
-      (Tacticals.New.tclTHEN
-         (mkBranches c1 c2)
-         (Tacticals.New.tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype)))
+      Proofview.Goal.enter begin fun gl ->
+        let concl = Proofview.Goal.concl gl in
+        match_eqdec concl >= fun eqonleft,_,c1,c2,typ ->
+        Tacmach.New.of_old (fun g -> hd_app (pf_compute g typ)) >>= fun headtyp ->
+        begin match kind_of_term headtyp with
+        | Ind mi -> Proofview.tclUNIT mi
+        | _ -> Proofview.tclZERO (UserError ("",Pp.str"This decision procedure only works for inductive objects."))
+        end >= fun rectype ->
+          (Tacticals.New.tclTHEN
+             (mkBranches c1 c2)
+             (Tacticals.New.tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype)))
+      end
     end
     begin function
       | PatternMatchingFailure ->