1 files changed, 0 insertions, 117 deletions
diff --git a/engine/sigma.ml b/engine/sigma.ml
deleted file mode 100644
index 9381a33a..00000000
--- a/engine/sigma.ml
+++ /dev/null
@@ -1,117 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-type 'a t = Evd.evar_map
-
-type ('a, 'b) le = unit
-
-let refl = ()
-let cons _ _  = ()
-let (+>) = fun _ _ -> ()
-
-type ('a, 'r) sigma = Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma
-
-type 'a evar = Evar.t
-
-let lift_evar evk () = evk
-
-let to_evar_map evd = evd
-let to_evar evk = evk
-
-let here x s = Sigma (x, s, ())
-
-(** API *)
-
-type 'r fresh = Fresh : 's evar * 's t * ('r, 's) le -> 'r fresh
-
-let new_evar sigma ?naming info =
-  let (sigma, evk) = Evd.new_evar sigma ?naming info in
-  Fresh (evk, sigma, ())
-
-let define evk c sigma =
-  Sigma ((), Evd.define evk c sigma, ())
-
-let new_univ_level_variable ?loc ?name rigid sigma =
-  let (sigma, u) = Evd.new_univ_level_variable ?loc ?name rigid sigma in
-  Sigma (u, sigma, ())
-
-let new_univ_variable ?loc ?name rigid sigma =
-  let (sigma, u) = Evd.new_univ_variable ?loc ?name rigid sigma in
-  Sigma (u, sigma, ())
-
-let new_sort_variable ?loc ?name rigid sigma =
-  let (sigma, u) = Evd.new_sort_variable ?loc ?name rigid sigma in
-  Sigma (u, sigma, ())
-
-let fresh_sort_in_family ?loc ?rigid env sigma s =
-  let (sigma, s) = Evd.fresh_sort_in_family ?loc ?rigid env sigma s in
-  Sigma (s, sigma, ())
-
-let fresh_constant_instance ?loc env sigma cst =
-  let (sigma, cst) = Evd.fresh_constant_instance ?loc env sigma cst in
-  Sigma (cst, sigma, ())
-
-let fresh_inductive_instance ?loc env sigma ind =
-  let (sigma, ind) = Evd.fresh_inductive_instance ?loc env sigma ind in
-  Sigma (ind, sigma, ())
-
-let fresh_constructor_instance ?loc env sigma pc =
-  let (sigma, c) = Evd.fresh_constructor_instance ?loc env sigma pc in
-  Sigma (c, sigma, ())
-
-let fresh_global ?loc ?rigid ?names env sigma r =
-  let (sigma, c) = Evd.fresh_global ?loc ?rigid ?names env sigma r in
-  Sigma (c, sigma, ())
-
-(** Run *)
-
-type 'a run = { run : 'r. 'r t -> ('a, 'r) sigma }
-
-let run sigma f : 'a * Evd.evar_map =
-  let Sigma (x, sigma, ()) = f.run sigma in
-  (x, sigma)
-
-(** Monotonic references *)
-
-type evdref = Evd.evar_map ref
-
-let apply evdref f =
-  let Sigma (x, sigma, ()) = f.run !evdref in
-  evdref := sigma;
-  x
-
-let purify f =
-  let f (sigma : Evd.evar_map) =
-    let evdref = ref sigma in
-    let ans = f evdref in
-    Sigma (ans, !evdref, ())
-  in
-  { run = f }
-
-(** Unsafe primitives *)
-
-module Unsafe =
-struct
-
-let le = ()
-let of_evar_map sigma = sigma
-let of_evar evk = evk
-let of_ref ref = ref
-let of_pair (x, sigma) = Sigma (x, sigma, ())
-
-end
-
-module Notations =
-struct
-  type ('a, 'r) sigma_ = ('a, 'r) sigma =
-    Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma_
-
-  let (+>) = fun _ _ -> ()
-
-  type 'a run_ = 'a run = { run : 'r. 'r t -> ('a, 'r) sigma }
-end