aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMatthieu Sozeau2019-02-08 11:28:43 +0100
committerMatthieu Sozeau2019-02-08 11:28:43 +0100
commitab6397730354d6048062568c87a7d971f20934c0 (patch)
tree231d5b120373f6b58471018db6728fb91f907b70
parentb74aaa4ce0191b92837a15773ae23e53abd22bd9 (diff)
evarsolve transp_state and comments fixes
-rw-r--r--pretyping/evarsolve.ml10
-rw-r--r--pretyping/evarsolve.mli6
2 files changed, 8 insertions, 8 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index cdaf66f119..e5f2207333 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 ce803fe254..ebf8230bbd 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;