diff options
| author | Pierre-Marie Pédrot | 2018-11-19 08:12:28 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-19 13:29:55 +0100 |
| commit | 733cb74a2038ff92156b7209713fc2ea741ccca6 (patch) | |
| tree | ee664936850ce6160d9e3fc3219b9dba7b7ea096 /vernac | |
| parent | ad5aea737ecc639c31dda84322b3550a4d380b47 (diff) | |
Rename TranspState into TransparentState.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/assumptions.ml | 2 | ||||
| -rw-r--r-- | vernac/assumptions.mli | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index b51b6cedfb..3ca2a4ad6b 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -315,7 +315,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = let t = type_of_constant cb in let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in ContextObjectMap.add (Axiom (Constant kn,l)) t accu - else if add_opaque && (Declareops.is_opaque cb || not (TranspState.is_transparent_constant st kn)) then + else if add_opaque && (Declareops.is_opaque cb || not (TransparentState.is_transparent_constant st kn)) then let t = type_of_constant cb in ContextObjectMap.add (Opaque kn) t accu else if add_transparent then diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli index 56d6202194..536185f4aa 100644 --- a/vernac/assumptions.mli +++ b/vernac/assumptions.mli @@ -28,5 +28,5 @@ val traverse : on which a term relies (together with their type). The above warning of {!traverse} also applies. *) val assumptions : - ?add_opaque:bool -> ?add_transparent:bool -> TranspState.t -> + ?add_opaque:bool -> ?add_transparent:bool -> TransparentState.t -> GlobRef.t -> constr -> types ContextObjectMap.t diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 34ddf3377f..7765f5b417 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1096,7 +1096,7 @@ let vernac_restore_state file = (* Commands *) let vernac_create_hintdb ~module_local id b = - Hints.create_hint_db module_local id TranspState.full b + Hints.create_hint_db module_local id TransparentState.full b let vernac_remove_hints ~module_local dbs ids = Hints.remove_hints module_local dbs (List.map Smartlocate.global_with_alias ids) |