diff options
| author | Matthieu Sozeau | 2019-02-08 11:28:43 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-02-08 11:28:43 +0100 |
| commit | ab6397730354d6048062568c87a7d971f20934c0 (patch) | |
| tree | 231d5b120373f6b58471018db6728fb91f907b70 | |
| parent | b74aaa4ce0191b92837a15773ae23e53abd22bd9 (diff) | |
evarsolve transp_state and comments fixes
| -rw-r--r-- | pretyping/evarsolve.ml | 10 | ||||
| -rw-r--r-- | pretyping/evarsolve.mli | 6 |
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; |
