STM: fix very simple demo

2 files changed, 8 insertions, 84 deletions

diff --git a/test-suite/interactive/Paral-ITP.v b/test-suite/interactive/Paral-ITP.v
index 55ca52bef..658e6856f 100644
--- a/test-suite/interactive/Paral-ITP.v
+++ b/test-suite/interactive/Paral-ITP.v
@@ -7,19 +7,12 @@ Fixpoint fib n := match n with
 Ltac sleep n :=
   try (cut (fib n = S (fib n)); reflexivity).
 
-Let time := 15.
-
-(* BEGIN MINI DEMO *)
-(* JUMP TO "JUMP HERE" *)
-
-Require Import ZArith Psatz.
+Let time := 18.
 
 Lemma a : True.
 Proof.
   sleep time.
   idtac.
-  assert(forall n m : Z, n + m = m + n)%Z.
-    intros; lia.
   sleep time.
   exact (I I).
 Qed.
@@ -29,80 +22,10 @@ Proof.
   do 11 (cut Type; [ intro foo; clear foo | exact Type]).
   sleep time.
   idtac.
-  assert(forall n m : Z, n + m = m + n)%Z.
-    intros; lia.
- (* change in semantics: Print a. *)
   sleep time.
   exact a.
-Qed. (* JUMP HERE *)
-
-Lemma work_here : True.
-Proof.
-cut True.
-Print b.
-Abort.
-
-(* END MINI DEMO *)
-
-
-
-Require Import Unicode.Utf8.
-Notation "a ⊃ b" := (a → b) (at level 91, left associativity).
-
-Definition untrue := False.
-
-Section Ex.
-Variable P Q : Prop.
-Implicit Types X Y : Prop.
-Hypothesis CL : forall X Y, (X → ¬Y → untrue) → (¬X ∨ Y).
-
-Lemma  Peirce : P ⊃ Q ⊃ P ⊃ P.
-Proof (* using P Q CL. *).   (* Uncomment -> more readable *)
-intro pqp.
-
-  Remark EM : ¬P ∨ P.
-  Proof using P CL.
-  intros; apply CL; intros p np.
-  Fail progress auto.  (* Missing hint *)
-
-  (* Try commenting this out *)
-  Hint Extern 0 => match goal with
-    p : P, np : ¬P |- _ => case (np p)
-  end.
-
-  auto.  (* This line requires the hint above *)
-  Qed.
-
-case EM; auto.  (* This line requires the hint above *)
 Qed.
 
-End Ex.
-
-Check EM. (* Print EM. *)
-
-
-Axiom exM : forall P, P \/ ~P.
-
-Lemma CPeirce (P Q : Prop) : P ⊃ Q ⊃ P ⊃ P.
-Proof.
-apply Peirce.
-intros.
-case (exM X); auto.
-intro; right.
-case (exM Y); auto; intro.
-case H; auto.
-Qed.
-
-Require Import Recdef.
-
-Definition m (n : nat) := n.
-
-Function f (n : nat) {measure m n} : bool :=
-  match n with
-  | O => true
-  | S x => f (x + 0)
-  end.
+Lemma work_here : True.
 Proof.
-intros x y _. unfold m.
-rewrite <- plus_n_O. auto.
-Qed.
+exact I.
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 8dec95322..521af61e3 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -1119,7 +1119,7 @@ let delegate_policy_check () =
   else if !Flags.compilation_mode = Flags.BuildVi then true
   else !Flags.async_proofs_mode <> Flags.APoff
 
-let collect_proof cur hd id =
+let collect_proof cur hd brkind id =
  prerr_endline ("Collecting proof ending at "^Stateid.to_string id);
  let loc = (snd cur).loc in
  let is_defined = function
@@ -1156,9 +1156,10 @@ let collect_proof cur hd id =
     | _, `Sideff (`Ast (x,_)) -> collect (Some (id,x)) (id::accn) view.next
     | _, `Sideff (`Id _) -> `Sync `NestedProof
     | _ -> `Sync `Unknown in
- match cur, (VCS.visit id).step with
- | (parent, { expr = VernacExactProof _ }), `Fork _ ->
+ match cur, (VCS.visit id).step, brkind with
+ |( parent, { expr = VernacExactProof _ }), `Fork _, _ ->
      `Sync `Immediate
+ | _, _, { VCS.kind = `Edit _ }  -> collect (Some cur) [] id
  | _ ->
      if State.is_cached id then `Sync `AlreadyEvaluated
      else if is_defined cur then `Sync `Transparent
@@ -1286,7 +1287,7 @@ let known_state ?(redefine_qed=false) ~cache id =
                   fst (aux (`Sync `Unknown)) ()
               ), if redefine_qed then `No else `Yes
           in
-          aux (collect_proof (view.next, x) brname eop)
+          aux (collect_proof (view.next, x) brname brinfo eop)
       | `Sideff (`Ast (x,_)) -> (fun () ->
             reach view.next; vernac_interp id x
           ), cache