diff options
| author | Hugo Herbelin | 2020-10-31 14:06:12 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-04 16:56:49 +0100 |
| commit | 78e600ac5f8aa9609cac4347c7a694428ae9d7cc (patch) | |
| tree | 54ddd0faba729e23d3cfc06c8d6457bb420a2d72 /vernac/comFixpoint.ml | |
| parent | 404a041fce68b4f7072de0b91b4e136f04250482 (diff) | |
Moving interpretation of user-level universes in constrintern.ml.
Diffstat (limited to 'vernac/comFixpoint.ml')
| -rw-r--r-- | vernac/comFixpoint.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 29bf5fbcc2..dd6c985bf9 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -176,7 +176,7 @@ let interp_recursive ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_expr_gen lis if not (CList.for_all2eq (fun x y -> Id.equal x.CAst.v y.CAst.v) lsu usu) then CErrors.user_err Pp.(str "(co)-recursive definitions should all have the same universe binders"); Some us) fixl None in - let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env all_universes in + let sigma, decl = interp_univ_decl_opt env all_universes in let sigma, (fixctxs, fiximppairs, fixannots) = on_snd List.split3 @@ List.fold_left_map (fun sigma -> interp_fix_context ~program_mode env sigma ~cofix) sigma fixl in |