From cc42541eeaaec0371940e07efdb009a4ee74e468 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 20 Oct 2015 13:04:45 +0200
Subject: Boxing the Goal.enter primitive into a record type.

---
 plugins/fourier/fourierR.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'plugins/fourier')

diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 7a56cd6657..e5c9b27075 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -19,6 +19,7 @@ open Globnames
 open Tacmach
 open Fourier
 open Contradiction
+open Proofview.Notations
 
 (******************************************************************************
 Opérations sur les combinaisons linéaires affines.
@@ -462,7 +463,7 @@ exception GoalDone
 
 (* Résolution d'inéquations linéaires dans R *)
 let rec fourier () =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     Coqlib.check_required_library ["Coq";"fourier";"Fourier"];
     let goal = strip_outer_cast concl in
@@ -622,7 +623,7 @@ let rec fourier () =
 (*    ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *))) gl) *)
       !tac
 (*      ((tclABSTRACT None !tac) gl) *)
-  end
+  end }
 ;;
 
 (*
-- 
cgit v1.2.3