From 954fbd3b102060ed1e2122f571a430f05a174e42 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 9 May 2017 22:14:35 +0200
Subject: Remove the Sigma (monotonous state) API.

Reminder of (some of) the reasons for removal:

- Despite the claim in sigma.mli, it does *not* prevent evar
  leaks, something like:

  fun env evd ->
  let (evd',ev) = new_evar env evd in
  (evd,ev)

  will typecheck even with Sigma-like type annotations (with a proof of
  reflexivity)

- The API stayed embryonic. Even typing functions were not ported to
  Sigma.

- Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly
  less unsafe ones (e.g. s_enter), but those ones were not marked unsafe
  at all (despite still being so).

- There was no good story for higher order functions manipulating evar
  maps. Without higher order, one can most of the time get away with
  reusing the same name for the updated evar map.

- Most of the code doing complex things with evar maps was using unsafe
  casts to sigma. This code should be fixed, but this is an orthogonal
  issue.

Of course, this was showing a nice and elegant use of GADTs, but the
cost/benefit ratio in practice did not seem good.
---
 plugins/romega/const_omega.ml  | 2 +-
 plugins/romega/const_omega.mli | 2 +-
 plugins/romega/refl_omega.ml   | 6 +++---
 3 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'plugins/romega')

diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index fbed1df176..d97dea0397 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -226,7 +226,7 @@ module type Int = sig
 
   val mk : Bigint.bigint -> Term.constr
   val parse_term : Term.constr -> parse_term
-  val parse_rel : ([ `NF ], 'r) Proofview.Goal.t -> Term.constr -> parse_rel
+  val parse_rel : [ `NF ] Proofview.Goal.t -> Term.constr -> parse_rel
   (* check whether t is built only with numbers and + * - *)
   val get_scalar : Term.constr -> Bigint.bigint option
 end
diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli
index ca23ed6c42..a452b1a917 100644
--- a/plugins/romega/const_omega.mli
+++ b/plugins/romega/const_omega.mli
@@ -113,7 +113,7 @@ module type Int =
     (* parsing a term (one level, except if a number is found) *)
     val parse_term : Term.constr -> parse_term
     (* parsing a relation expression, including = < <= >= > *)
-    val parse_rel : ([ `NF ], 'r) Proofview.Goal.t -> Term.constr -> parse_rel
+    val parse_rel : [ `NF ] Proofview.Goal.t -> Term.constr -> parse_rel
     (* Is a particular term only made of numbers and + * - ? *)
     val get_scalar : Term.constr -> Bigint.bigint option
   end
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index fdcd622994..575634174f 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -8,7 +8,6 @@
 
 open Pp
 open Util
-open Proofview.Notations
 open Const_omega
 module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint)
 open OmegaSolver
@@ -1029,7 +1028,7 @@ let resolution unsafe env (reified_concl,reified_hyps) systems_list =
   Tactics.apply (EConstr.of_constr (Lazy.force coq_I))
 
 let total_reflexive_omega_tactic unsafe =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.nf_enter begin fun gl ->
   Coqlib.check_required_library ["Coq";"romega";"ROmega"];
   rst_omega_eq ();
   rst_omega_var ();
@@ -1043,4 +1042,5 @@ let total_reflexive_omega_tactic unsafe =
   if !debug then display_systems systems_list;
   resolution unsafe env reified_goal systems_list
   with NO_CONTRADICTION -> CErrors.user_err Pp.(str "ROmega can't solve this system")
-  end }
+  end
+
-- 
cgit v1.2.3