2 files changed, 20 insertions, 10 deletions
diff --git a/src/Experiments/Ed25519Extraction.v b/src/Experiments/Ed25519Extraction.v
index 20a76f17f..eaa00bea4 100644
--- a/src/Experiments/Ed25519Extraction.v
+++ b/src/Experiments/Ed25519Extraction.v
@@ -233,7 +233,7 @@ Extraction Implicit Word.split1 [ 2 ].
 Extraction Implicit Word.split2 [ 2 ].
 Extraction Implicit WordUtil.cast_word [1 2 3].
 Extraction Implicit WordUtil.wfirstn [ 2 4 ].
-Extract Inlined Constant WordUtil.cast_word => "".
+Extraction Inline WordUtil.cast_word.
 Extract Inductive Word.word => "[Prelude.Bool]" [ "[]" "(:)" ]
   "(\fWO fWS w -> {- match_on_word -} case w of {[] -> fWO (); (b:w') -> fWS b w' } )".
 
@@ -296,4 +296,4 @@ True
 
 Import Crypto.Spec.MxDH.
 Extraction Inline MxDH.ladderstep MxDH.montladder.
-Extraction "src/Experiments/X25519_noimports.hs" Crypto.Experiments.Ed25519.x25519.
-\ No newline at end of file
+Extraction "src/Experiments/X25519_noimports.hs" Crypto.Experiments.Ed25519.x25519.
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index 7a856f1e9..d4bc73aeb 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -83,16 +83,26 @@ Ltac wordsize_eq_tac := cbv beta delta [wordsize_eq] in *; omega*.
 Ltac gt84_abstract t := t. (* TODO: when we drop Coq 8.4, use [abstract] here *)
 Hint Extern 100 (wordsize_eq _ _) => gt84_abstract wordsize_eq_tac : typeclass_instances.
 
-Program Fixpoint cast_word {n m} : forall {pf:wordsize_eq n m}, word n -> word m :=
-  match n, m return wordsize_eq n m -> word n -> word m with
-  | O, O => fun _ _ => WO
-  | S n', S m' => fun _ w => WS (whd w) (@cast_word _ _ _ (wtl w))
-  | _, _ => fun _ _ => !
+Fixpoint correct_wordsize_eq (x y : nat) : wordsize_eq x y -> x = y
+  := match x, y with
+     | O, O => fun _ => eq_refl
+     | S x', S y' => fun pf => f_equal S (correct_wordsize_eq x' y' (f_equal pred pf))
+     | _, _ => fun x => x
+     end.
+
+Lemma correct_wordsize_eq_refl n pf : correct_wordsize_eq n n pf = eq_refl.
+Proof.
+  induction n; [ reflexivity | simpl ].
+  rewrite IHn; reflexivity.
+Qed.
+
+Definition cast_word {n m} {pf:wordsize_eq n m} : word n -> word m :=
+  match correct_wordsize_eq n m pf in _ = y return word n -> word y with
+  | eq_refl => fun w => w
   end.
-Global Arguments cast_word {_ _ _} _. (* 8.4 does not pick up the forall braces *)
 
 Lemma cast_word_refl {n} pf (w:word n) : @cast_word n n pf w = w.
-Proof. induction w; simpl; auto using f_equal. Qed.
+Proof. unfold cast_word; rewrite correct_wordsize_eq_refl; reflexivity. Qed.
 
 Lemma wordToNat_cast_word {n} (w:word n) m pf :
   wordToNat (@cast_word n m pf w) = wordToNat w.
@@ -317,4 +327,4 @@ Axiom winit : forall sz, word (sz+1) -> word sz. Arguments winit {_} _.
 Axiom combine_winit_wlast : forall {sz} a b (c:word (sz+1)),
     @combine sz a 1 b = c <-> a = winit c /\ b = (WS (wlast c) WO).
 Axiom winit_combine : forall sz a b, @winit sz (combine a b) = a.
-Axiom wlast_combine : forall sz a b, @wlast sz (combine a (WS b WO)) = b.
-\ No newline at end of file
+Axiom wlast_combine : forall sz a b, @wlast sz (combine a (WS b WO)) = b.