diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-13 17:33:04 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-30 19:23:04 +0100 |
| commit | bad3f3b784d3de8851615b8f4b7afba734232d8e (patch) | |
| tree | be6a12a50d3bf6b73ea7866334585f694370e630 /tactics/ind_tables.ml | |
| parent | 441bea723c511ed9e18ef005678bd01242b45c49 (diff) | |
Moving some universe substitution code out of the kernel.
This code was not used at all inside the kernel, it was related to universe
unification that happens in the upper layer. It makes more sense to put it
somewhere upper.
Diffstat (limited to 'tactics/ind_tables.ml')
| -rw-r--r-- | tactics/ind_tables.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index e1bf32f3c..bc2fea2bd 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -121,8 +121,7 @@ let define internal id c p univs = let fd = declare_constant ~internal in let id = compute_name internal id in let ctx = Evd.normalize_evar_universe_context univs in - let c = Vars.subst_univs_fn_constr - (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in + let c = Universes.subst_opt_univs_constr (Evd.evar_universe_context_subst ctx) c in let univs = if p then Polymorphic_const_entry (UState.context ctx) else Monomorphic_const_entry (UState.context_set ctx) |