diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/reduction.ml | 24 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 17 |
2 files changed, 24 insertions, 17 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 427ce04c55..b6786c045c 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -356,17 +356,17 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let (app1,app2) = if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then match unfold_reference infos fl1 with - | Some def1 -> ((lft1, whd def1 v1), appr2) + | Some def1 -> ((lft1, (def1, v1)), appr2) | None -> (match unfold_reference infos fl2 with - | Some def2 -> (appr1, (lft2, whd def2 v2)) + | Some def2 -> (appr1, (lft2, (def2, v2))) | None -> raise NotConvertible) else match unfold_reference infos fl2 with - | Some def2 -> (appr1, (lft2, whd def2 v2)) + | Some def2 -> (appr1, (lft2, (def2, v2))) | None -> (match unfold_reference infos fl1 with - | Some def1 -> ((lft1, whd def1 v1), appr2) + | Some def1 -> ((lft1, (def1, v1)), appr2) | None -> raise NotConvertible) in eqappr cv_pb l2r infos app1 app2 cuniv) @@ -377,11 +377,11 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = form *) (match unfold_projection infos p1 c1 with | Some (def1,s1) -> - eqappr cv_pb l2r infos (lft1, whd def1 (s1 :: v1)) appr2 cuniv + eqappr cv_pb l2r infos (lft1, (def1, s1 :: v1)) appr2 cuniv | None -> match unfold_projection infos p2 c2 with | Some (def2,s2) -> - eqappr cv_pb l2r infos appr1 (lft2, whd def2 (s2 :: v2)) cuniv + eqappr cv_pb l2r infos appr1 (lft2, (def2, s2 :: v2)) cuniv | None -> if Constant.equal (Projection.constant p1) (Projection.constant p2) && compare_stack_shape v1 v2 then @@ -393,26 +393,26 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (FProj (p1,c1), t2) -> (match unfold_projection infos p1 c1 with | Some (def1,s1) -> - eqappr cv_pb l2r infos (lft1, whd def1 (s1 :: v1)) appr2 cuniv + eqappr cv_pb l2r infos (lft1, (def1, s1 :: v1)) appr2 cuniv | None -> (match t2 with | FFlex fl2 -> (match unfold_reference infos fl2 with | Some def2 -> - eqappr cv_pb l2r infos appr1 (lft2, whd def2 v2) cuniv + eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv | None -> raise NotConvertible) | _ -> raise NotConvertible)) | (t1, FProj (p2,c2)) -> (match unfold_projection infos p2 c2 with | Some (def2,s2) -> - eqappr cv_pb l2r infos appr1 (lft2, whd def2 (s2 :: v2)) cuniv + eqappr cv_pb l2r infos appr1 (lft2, (def2, s2 :: v2)) cuniv | None -> (match t1 with | FFlex fl1 -> (match unfold_reference infos fl1 with | Some def1 -> - eqappr cv_pb l2r infos (lft1, whd def1 v1) appr2 cuniv + eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv | None -> raise NotConvertible) | _ -> raise NotConvertible)) @@ -458,7 +458,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (FFlex fl1, c2) -> (match unfold_reference infos fl1 with | Some def1 -> - eqappr cv_pb l2r infos (lft1, whd def1 v1) appr2 cuniv + eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv | None -> match c2 with | FConstruct ((ind2,j2),u2) -> @@ -472,7 +472,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (c1, FFlex fl2) -> (match unfold_reference infos fl2 with | Some def2 -> - eqappr cv_pb l2r infos appr1 (lft2, whd def2 v2) cuniv + eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv | None -> match c1 with | FConstruct ((ind1,j1),u1) -> diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index eeb9c421a1..bdfd00a8d3 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -344,11 +344,18 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) if not (Id.Set.subset inferred_set declared_set) then let l = Id.Set.elements (Idset.diff inferred_set declared_set) in let n = List.length l in - user_err (Pp.(str "The following section " ++ - str (String.plural n "variable") ++ - str " " ++ str (String.conjugate_verb_to_be n) ++ - str " used but not declared:" ++ - fnl () ++ pr_sequence Id.print (List.rev l) ++ str ".")) in + let declared_vars = Pp.pr_sequence Id.print (Idset.elements declared_set) in + let inferred_vars = Pp.pr_sequence Id.print (Idset.elements inferred_set) in + let missing_vars = Pp.pr_sequence Id.print (List.rev l) in + user_err Pp.(prlist str + ["The following section "; (String.plural n "variable"); " "; + (String.conjugate_verb_to_be n); " used but not declared:"] ++ fnl () ++ + missing_vars ++ str "." ++ fnl () ++ fnl () ++ + str "You can either update your proof to not depend on " ++ missing_vars ++ + str ", or you can update your Proof line from" ++ fnl () ++ + str "Proof using " ++ declared_vars ++ fnl () ++ + str "to" ++ fnl () ++ + str "Proof using " ++ inferred_vars) in let sort evn l = List.filter (fun decl -> let id = NamedDecl.get_id decl in |