diff options
| author | Pierre-Marie Pédrot | 2015-10-17 18:55:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-17 21:51:34 +0200 |
| commit | d558bf5289e87899a850dda410a3a3c4de1ce979 (patch) | |
| tree | 318a03a94298a40d1d9e5afc0653a336dec42918 /stm | |
| parent | 68863acca9abf4490c651df889721ef7f6a4d375 (diff) | |
Clarifying and documenting the UState API.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/lemmas.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/lemmas.ml b/stm/lemmas.ml index d26af04baa..5f034e361e 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -428,7 +428,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook = let body,opaq = retrieve_first_recthm ref in let subst = Evd.evar_universe_context_subst ctx in let norm c = Universes.subst_opt_univs_constr subst c in - let ctx = Evd.evar_universe_context_set (*FIXME*) Univ.UContext.empty ctx in + let ctx = UState.context_set (*FIXME*) ctx in let body = Option.map norm body in List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in let thms_data = (strength,ref,imps)::other_thms_data in |