Use eexact in weaksauce_einsum (#5)

cf coq/coq#18157
JasonGross · Oct 24, 2023 · 78daaa8 · 78daaa8
1 parent 4fe4f07
commit 78daaa8
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/Torch/Einsum.v b/theories/Torch/Einsum.v
@@ -263,7 +263,7 @@ Notation "'weaksauce_einsum' x"
                     let z := (eval cbn beta iota delta [Nat.radd] in z) in
                     let z := (eval cbn beta iota zeta delta [Shape.snoc Shape.nil] in z) in
                     (*let z := (eval cbn beta iota zeta delta [PrimitiveProd.Primitive.fst PrimitiveProd.Primitive.snd Shape.snoc Shape.nil] in z) in*)
-                    exact $z)
+                    eexact $z)
       end)
        (x custom einsum_args at level 10, at level 10, only parsing).
 (*