Commit 82945e24 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Coq menhirlib : in cast, make sure we do reprove the equality in the extracted code.

parent cc4aaa06
Pipeline #64829 passed with stages
in 20 seconds
...@@ -72,9 +72,9 @@ Definition reprove {P} `{Decidable P} (p : thunkP P) : P := ...@@ -72,9 +72,9 @@ Definition reprove {P} `{Decidable P} (p : thunkP P) : P :=
(** Combination of reprove with eq_rect. *) (** Combination of reprove with eq_rect. *)
Definition cast {T : Type} (F : T -> Type) {x y : T} (eq : thunkP (x = y)) Definition cast {T : Type} (F : T -> Type) {x y : T} (eq : thunkP (x = y))
`{Decidable (x = y)}: {DEC : unit -> Decidable (x = y)}:
F x -> F y := F x -> F y :=
fun a => eq_rect x F a y (reprove eq). fun a => eq_rect x F a y (@reprove _ (DEC ()) eq).
Lemma cast_eq T F (x : T) (eq : thunkP (x = x)) `{forall x y, Decidable (x = y)} a : Lemma cast_eq T F (x : T) (eq : thunkP (x = x)) `{forall x y, Decidable (x = y)} a :
cast F eq a = a. cast F eq a = a.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment