Remove use of beta in reification of Let_In

1 files changed, 13 insertions, 9 deletions

diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v
index 545614301..8fef7d410 100644
--- a/src/Experiments/SimplyTypedArithmetic.v
+++ b/src/Experiments/SimplyTypedArithmetic.v
@@ -90,9 +90,9 @@ Module Associational.
 
     Definition carryterm (w fw:Z) (t:Z * Z) :=
       if (Z.eqb (fst t) w)
-      then dlet t2 := snd t in
-           dlet d2 := div t2 fw in
-           dlet m2 := modulo t2 fw in
+      then dlet_nd t2 := snd t in
+           dlet_nd d2 := div t2 fw in
+           dlet_nd m2 := modulo t2 fw in
            [(w * fw, d2);(w,m2)]
       else [t].
 
@@ -661,11 +661,13 @@ Module Compilers.
           | @List.repeat ?A
             => let rA := type.reify A in
                constr:(@ident.List_repeat rA)
-          | @LetIn.Let_In ?A ?B
-            => let B := lazymatch (eval cbv beta in B) with fun _ => ?B => B end in
-               let rA := type.reify A in
+          | @LetIn.Let_In ?A (fun _ => ?B)
+            => let rA := type.reify A in
                let rB := type.reify B in
                constr:(@ident.Let_In rA rB)
+          | @LetIn.Let_In ?A ?B
+            => let dummy := match goal with _ => fail 1 "Let_In contains a dependent type λ as its second argument:" B end in
+               constr:(I : I)
           | @combine ?A ?B
             => let rA := type.reify A in
                let rB := type.reify B in
@@ -866,11 +868,13 @@ Module Compilers.
             => let rT := type.reify T in
                constr:(@ident.nat_rect rT)
           | Nat.pred => ident.pred
-          | @LetIn.Let_In ?A ?B
-            => let B := lazymatch (eval cbv beta in B) with fun _ => ?B => B end in
-               let rA := type.reify A in
+          | @LetIn.Let_In ?A (fun _ => ?B)
+            => let rA := type.reify A in
                let rB := type.reify B in
                constr:(@ident.Let_In rA rB)
+          | @LetIn.Let_In ?A ?B
+            => let dummy := match goal with _ => fail 1 "Let_In contains a dependent type λ as its second argument:" B end in
+               constr:(I : I)
           | @Datatypes.list_rect ?A (fun _ => ?B)
             => let rA := type.reify A in
                let rB := type.reify B in