Skip to content

Commit c8944dc

Browse files
committed
Fix checker after addition of a universe context in with t := c constraints.
1 parent 6fcfa31 commit c8944dc

File tree

3 files changed

+4
-4
lines changed

3 files changed

+4
-4
lines changed

checker/cic.mli

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -333,7 +333,7 @@ type ('ty,'a) functorize =
333333

334334
type with_declaration =
335335
| WithMod of Id.t list * module_path
336-
| WithDef of Id.t list * constr
336+
| WithDef of Id.t list * (constr * Univ.universe_context)
337337

338338
type module_alg_expr =
339339
| MEident of module_path

checker/declarations.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -583,7 +583,7 @@ let implem_map fs fa = function
583583

584584
let subst_with_body sub = function
585585
| WithMod(id,mp) -> WithMod(id,subst_mp sub mp)
586-
| WithDef(id,c) -> WithDef(id,subst_mps sub c)
586+
| WithDef(id,(c,ctx)) -> WithDef(id,(subst_mps sub c,ctx))
587587

588588
let rec subst_expr sub = function
589589
| MEident mp -> MEident (subst_mp sub mp)

checker/values.ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@
1313
To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
1414
with a copy we maintain here:
1515
16-
MD5 0fbea8efeae581d87d977faa9eb2f421 checker/cic.mli
16+
MD5 0a174243f8b06535c9eecbbe8d339fe1 checker/cic.mli
1717
1818
*)
1919

@@ -270,7 +270,7 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
270270
let v_with =
271271
Sum ("with_declaration_body",0,
272272
[|[|List v_id;v_mp|];
273-
[|List v_id;v_constr|]|])
273+
[|List v_id;v_tuple "with_def" [|v_constr;v_context|]|]|])
274274

275275
let rec v_mae =
276276
Sum ("module_alg_expr",0,

0 commit comments

Comments
 (0)