diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-05-10 13:13:41 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-05-10 13:13:41 +0200 |
| commit | 6be542f4ccb1d7fe95a65f4600f202a2424370d9 (patch) | |
| tree | b831564bca815ab2b0695abea35744b13e9b5c7d /stm/vernac_classifier.ml | |
| parent | c4be3f4051761769676fc00e0fad9069710159c6 (diff) | |
Proof_global, STM: cleanup + use default_proof_mode instead of "Classic"
The "Classic" string is still hard coded here in there in the system, but
not in STM.
BTW, the use of an hard coded "Classic" value suggests nobody really uses
"Set Default Proof Mode" in .v files.
Diffstat (limited to 'stm/vernac_classifier.ml')
| -rw-r--r-- | stm/vernac_classifier.ml | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index ecaf0fb7c..b1df3c9ca 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -10,6 +10,8 @@ open Vernacexpr open Errors open Pp +let default_proof_mode () = Proof_global.get_default_proof_mode_name () + let string_of_in_script b = if b then " (inside script)" else "" let string_of_vernac_type = function @@ -115,27 +117,27 @@ let rec classify_vernac e = (* StartProof *) | VernacDefinition ( (Some Decl_kinds.Discharge,Decl_kinds.Definition),((_,i),_),ProveBody _) -> - VtStartProof("Classic",Doesn'tGuaranteeOpacity,[i]), VtLater + VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity,[i]), VtLater | VernacDefinition (_,((_,i),_),ProveBody _) -> - VtStartProof("Classic",GuaranteesOpacity,[i]), VtLater + VtStartProof(default_proof_mode (),GuaranteesOpacity,[i]), VtLater | VernacStartTheoremProof (_,l,_) -> let ids = CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in - VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater - | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater + VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater + | VernacGoal _ -> VtStartProof (default_proof_mode (),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",GuaranteesOpacity,ids), VtLater + then VtStartProof (default_proof_mode (),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",GuaranteesOpacity,ids), VtLater + then VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater else VtSideff ids, VtLater (* Sideff: apply to all open branches. usually run on master only *) | VernacAssumption (_,_,l) -> |