improved auto goal selection (see coq/#16293) (#39)

adampetcher · Jul 13, 2022 · 53ecd2e · 53ecd2e
1 parent 97071c5
commit 53ecd2e
Show file tree

Hide file tree

Showing 4 changed files with 10 additions and 10 deletions.
diff --git a/src/FCF/Fold.v b/src/FCF/Fold.v
@@ -3216,7 +3216,7 @@ Lemma firstn_ge_all : forall n (A : Set) (ls : list A),
   n >= length ls ->
   firstn n ls = ls.
 
-  induction n; intuition; simpl in *.
+  induction n; intuition idtac; simpl in *.
   destruct ls; simpl in *.
   trivial.
   lia.
@@ -3904,7 +3904,7 @@ Theorem app_cons_eq :
   forall (A : Type) ls2 ls1 (a : A),
     ls2 ++ (a :: ls1) = (ls2 ++ (a :: nil)) ++ ls1.
 
-  induction ls2; intuition; simpl in *.
+  induction ls2; intuition idtac; simpl in *.
   f_equal.
   eauto.
 

diff --git a/src/FCF/OracleHybrid.v b/src/FCF/OracleHybrid.v
@@ -559,7 +559,7 @@ Section OracleMapHybrid.
     rewrite firstn_skipn.
     fcf_skip.
     eapply (compFold_spec' (fun a b c d => a = b /\ snd c = snd d /\ l0++ (fst d) = (fst c)));
-      intuition.
+      intuition idtac.
     simpl.
     eapply app_nil_r.
     simpl in *.

diff --git a/src/FCF/ProgramLogic.v b/src/FCF/ProgramLogic.v
@@ -273,7 +273,7 @@ Theorem comp_spec_seq :
   rewrite ratMult_1_r.
   eapply ratMult_eqRat_compat; intuition.
   specialize (H2 a).
-  intuition.
+  intuition idtac.
   rewrite H2.
 
   unfold marginal_l.
@@ -320,7 +320,7 @@ Theorem comp_spec_seq :
   rewrite H5.
   rewrite ratMult_1_r.
   eapply ratMult_eqRat_compat; intuition.
-  specialize (H2 a); intuition.
+  specialize (H2 a); intuition idtac.
   rewrite H6.
   unfold marginal_r; intuition.
 
@@ -1719,13 +1719,13 @@ Theorem comp_spec_irr_r :
   unfold marginal_l.
   dist_inline_first.
   dist_irr_r.
-  specialize (H0 x0); intuition.
+  specialize (H0 x0); intuition idtac.
   eapply H0.
 
   unfold marginal_r.
   dist_inline_first.
   dist_skip.
-  specialize (H0 x0); intuition.
+  specialize (H0 x0); intuition idtac.
   apply H2.
   repeat simp_in_support.
   specialize (H0 x0); intuition.
@@ -1748,13 +1748,13 @@ Theorem comp_spec_irr_l :
   unfold marginal_l.
   dist_inline_first.
   dist_skip.
-  specialize (H0 x0); intuition.
+  specialize (H0 x0); intuition idtac.
   eapply H0.
 
   unfold marginal_r.
   dist_inline_first.
   dist_irr_r.
-  specialize (H0 x0); intuition.
+  specialize (H0 x0); intuition idtac.
   apply H2.
   repeat simp_in_support.
   specialize (H0 x0); intuition.

diff --git a/src/FCF/RndNat.v b/src/FCF/RndNat.v
@@ -32,7 +32,7 @@ Lemma well_formed_RndNat : forall n,
   unfold RndNat.
   eapply (well_formed_Repeat).
   unfold eq_dec.
-  intuition.
+  intuition idtac.
   eapply eq_nat_dec.
   unfold RndNat_unchecked.
   eapply well_formed_Bind.