only cbn in hyps

a150e592 · Michael Sammler · e4b924f3 · a150e592
Commit a150e592 authored Nov 17, 2021 by Michael Sammler
--- a/theories/typing/automation.v
+++ b/theories/typing/automation.v
@@ -308,9 +308,9 @@ Ltac liRSplitBlocksIntro :=

 (* TODO: don't use i... tactics here *)
 Ltac split_blocks Pfull Ps :=
-  (* cbn in * is important here to simplify the types of local
+  (* cbn in *|- is important here to simplify the types of local
  variables, otherwise unification gets confused later *)
-  cbn -[union] in *;
+  cbn -[union] in * |-;
  let rec pose_Ps Ps :=
      lazymatch Ps with
      | <[?bid:=?P]>?m =>