From e87288450d4d9e49ac91d179714a73bd0147c0d7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 19 May 2018 16:51:55 +0200 Subject: [api] Move `opacity_flag` to `Proof_global`. `Proof_global` is the main consumer of the flag, which doesn't seem to belong to the AST as plugins show. This will allow the vernac AST to be placed in `vernac` indeed. --- parsing/g_proofs.ml4 | 1 + 1 file changed, 1 insertion(+) (limited to 'parsing') diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index e393c2bbf..4f3d83a8a 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -10,6 +10,7 @@ open Constrexpr open Vernacexpr +open Proof_global open Misctypes open Pcoq -- cgit v1.2.3