diff options
Diffstat (limited to 'toplevel/vernac_classifier.ml')
| -rw-r--r-- | toplevel/vernac_classifier.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/toplevel/vernac_classifier.ml b/toplevel/vernac_classifier.ml index 2e04d14302..4ef157a64a 100644 --- a/toplevel/vernac_classifier.ml +++ b/toplevel/vernac_classifier.ml @@ -94,23 +94,23 @@ let rec classify_vernac e = | VernacSolveExistential _ -> VtProofStep, VtLater (* StartProof *) | VernacDefinition (_,(_,i),ProveBody _) -> - VtStartProof("Classic",[i]), VtLater + VtStartProof("Classic",GuaranteesOpacity,[i]), VtLater | VernacStartTheoremProof (_,l,_) -> let ids = CList.map_filter (function (Some(_,i), _) -> Some i | _ -> None) l in - VtStartProof ("Classic", ids), VtLater - | VernacGoal _ -> VtStartProof ("Classic",[]), VtLater + VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater + | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater | VernacFixpoint (_,l) -> let ids, open_proof = List.fold_left (fun (l,b) (((_,id),_,_,_,p),_) -> id::l, b || p = None) ([],false) l in - if open_proof then VtStartProof ("Classic",ids), VtLater + if open_proof then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater else VtSideff ids, VtLater | VernacCoFixpoint (_,l) -> let ids, open_proof = List.fold_left (fun (l,b) (((_,id),_,_,p),_) -> id::l, b || p = None) ([],false) l in - if open_proof then VtStartProof ("Classic",ids), VtLater + if open_proof then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater else VtSideff ids, VtLater (* Sideff: apply to all open branches. usually run on master only *) | VernacAssumption (_,_,l) -> |