diff options
Diffstat (limited to 'tuto1/src')
| -rw-r--r-- | tuto1/src/simple_declare.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tuto1/src/simple_declare.ml b/tuto1/src/simple_declare.ml index af4dd5bddf..50fd170663 100644 --- a/tuto1/src/simple_declare.ml +++ b/tuto1/src/simple_declare.ml @@ -1,10 +1,10 @@ +(* Ideally coq/coq#8811 would get merged and then this function could be much simpler. *) let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook = - let open EConstr in let sigma = Evd.minimize_universes sigma in - let body = to_constr sigma body in - let tyopt = Option.map (to_constr sigma) tyopt in + let body = EConstr.to_constr sigma body in + let tyopt = Option.map (EConstr.to_constr sigma) tyopt in let uvars_fold uvars c = - Univ.LSet.union uvars (Univops.universes_of_constr c) in + Univ.LSet.union uvars (Vars.universes_of_constr c) in let uvars = List.fold_left uvars_fold Univ.LSet.empty (Option.List.cons tyopt [body]) in let sigma = Evd.restrict_universe_context sigma uvars in |