diff options
Diffstat (limited to 'plugins/fourier')
| -rw-r--r-- | plugins/fourier/fourierR.ml | 14 |
1 files changed, 4 insertions, 10 deletions
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 7a56cd6657..b1f642c1d2 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. @@ -412,13 +413,6 @@ let tac_zero_infeq_false gl (n,d) = (tac_zero_inf_pos gl (-n,d))) ;; -let create_meta () = mkMeta(Evarutil.new_meta());; - -let my_cut c gl= - let concl = pf_concl gl in - apply_type (mkProd(Anonymous,c,concl)) [create_meta()] gl -;; - let exact = exact_check;; let tac_use h = @@ -462,7 +456,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 @@ -586,7 +580,7 @@ let rec fourier () = then tac_zero_inf_false gl (rational_to_fraction cres) else tac_zero_infeq_false gl (rational_to_fraction cres) in - tac:=(Tacticals.New.tclTHENS (Proofview.V82.tactic (my_cut ineq)) + tac:=(Tacticals.New.tclTHENS (cut ineq) [Tacticals.New.tclTHEN (change_concl (mkAppL [| get coq_not; ineq|] )) @@ -622,7 +616,7 @@ let rec fourier () = (* ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *))) gl) *) !tac (* ((tclABSTRACT None !tac) gl) *) - end + end } ;; (* |