From 481db1ce8b0e653c22f332ef7eab5c1fa575b6f4 Mon Sep 17 00:00:00 2001
From: Tej Chajed
Date: Mon, 10 Feb 2020 18:19:45 -0500
Subject: Recognize Default Proof Using in STM

Treat a Set Default Proof Using call the same as having a syntactic
Proof using ... annotation. This ensures that proofs in sections are
skipped in -vos mode when there are enough annotations to determine the
type of the resulting theorem.

Fixes #11342.
---
 stm/stm.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index 4c539684e3..a550020cb3 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2154,6 +2154,7 @@ let collect_proof keep cur hd brkind id =
  let is_defined = function
    | _, { expr = e } -> is_defined_expr e.CAst.v.expr
                         && (not (Vernacprop.has_Fail e)) in
+ let has_default_proof_using = Option.has_some (Proof_using.get_default_proof_using ()) in
  let proof_using_ast = function
    | VernacProof(_,Some _) -> true
    | _ -> false
@@ -2162,7 +2163,7 @@ let collect_proof keep cur hd brkind id =
    | Some (_, v) when proof_using_ast v.expr.CAst.v.expr
                       && (not (Vernacprop.has_Fail v.expr)) -> Some v
    | _ -> None in
- let has_proof_using x = proof_using_ast x <> None in
+ let has_proof_using x = has_default_proof_using || (proof_using_ast x <> None) in
  let proof_no_using = function
    | VernacProof(t,None) -> t
    | _ -> assert false
-- 
cgit v1.2.3