From ab6397730354d6048062568c87a7d971f20934c0 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Fri, 8 Feb 2019 11:28:43 +0100
Subject: [PATCH] evarsolve transp_state and comments fixes

---
 pretyping/evarsolve.ml  | 10 +++++-----
 pretyping/evarsolve.mli |  6 +++---
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index cdaf66f11992..e5f2207333dd 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -26,9 +26,9 @@ open Pretype_errors
 
 type unify_flags = {
   modulo_betaiota: bool;
-  open_ts : transparent_state;
-  closed_ts : transparent_state;
-  subterm_ts : transparent_state;
+  open_ts : TransparentState.t;
+  closed_ts : TransparentState.t;
+  subterm_ts : TransparentState.t;
   frozen_evars : Evar.Set.t;
   allow_K_at_toplevel : bool;
   with_cs : bool }
@@ -1442,8 +1442,8 @@ let occur_evar_upto_types sigma n c =
   try occur_rec c; false with Occur -> true
 
 let instantiate_evar unify flags evd evk body =
-  (** Check instance freezing the evar to be defined, as
-      checking could involve the same evar definition problem again otherwise *)
+  (* Check instance freezing the evar to be defined, as
+     checking could involve the same evar definition problem again otherwise *)
   let flags = { flags with frozen_evars = Evar.Set.add evk flags.frozen_evars } in
   let evd' = check_evar_instance unify flags evd evk body in
   Evd.define evk body evd'
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index ce803fe25496..ebf8230bbd1a 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -19,11 +19,11 @@ val of_alias : alias -> EConstr.t
 type unify_flags = {
   modulo_betaiota : bool;
   (* Enable beta-iota reductions during unification *)
-  open_ts : Names.transparent_state;
+  open_ts : TransparentState.t;
   (* Enable delta reduction according to open_ts for open terms *)
-  closed_ts : Names.transparent_state;
+  closed_ts : TransparentState.t;
   (* Enable delta reduction according to closed_ts for closed terms (when calling conversion) *)
-  subterm_ts : Names.transparent_state;
+  subterm_ts : TransparentState.t;
   (* Enable delta reduction according to subterm_ts for selection of subterms during higher-order
      unifications. *)
   frozen_evars : Evar.Set.t;