diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 4 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 21 |
2 files changed, 17 insertions, 8 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 0ee9ea0841..8aa832da84 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -762,7 +762,7 @@ end = struct (* {{{ *) let fix_exn_ref = ref (fun x -> x) type proof_part = - Proof_global.state * Summary.frozen_bits (* only meta counters *) + Proof_global.t * Summary.frozen_bits (* only meta counters *) type partial_state = [ `Full of Vernacstate.t @@ -1023,7 +1023,7 @@ let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t | VernacShow ShowScript -> ShowScript.show_script (); st | expr -> stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr); - try Vernacentries.interp ?verbosely:(Some verbose) ?proof st (Loc.tag ?loc expr) + try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st (Loc.tag ?loc expr) with e -> let e = CErrors.push e in Exninfo.iraise Hooks.(call_process_error_once e) diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 3aa2cd707e..1ca572a36c 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -103,8 +103,7 @@ let rec classify_vernac e = | VernacUnsetOption (["Default";"Proof";"Using"]) | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow (* StartProof *) - | VernacDefinition ( - (Some Decl_kinds.Discharge,Decl_kinds.Definition),((_,i),_),ProveBody _) -> + | VernacDefinition ((Decl_kinds.DoDischarge,_),((_,i),_),ProveBody _) -> VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity,[i]), VtLater | VernacDefinition (_,((_,i),_),ProveBody _) -> VtStartProof(default_proof_mode (),GuaranteesOpacity,[i]), VtLater @@ -113,19 +112,29 @@ let rec classify_vernac e = CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater | VernacGoal _ -> VtStartProof (default_proof_mode (),GuaranteesOpacity,[]), VtLater - | VernacFixpoint (_,l) -> + | VernacFixpoint (discharge,l) -> + let guarantee = + match discharge with + | Decl_kinds.NoDischarge -> GuaranteesOpacity + | Decl_kinds.DoDischarge -> Doesn'tGuaranteeOpacity + in 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 (default_proof_mode (),GuaranteesOpacity,ids), VtLater + then VtStartProof (default_proof_mode (),guarantee,ids), VtLater else VtSideff ids, VtLater - | VernacCoFixpoint (_,l) -> + | VernacCoFixpoint (discharge,l) -> + let guarantee = + match discharge with + | Decl_kinds.NoDischarge -> GuaranteesOpacity + | Decl_kinds.DoDischarge -> Doesn'tGuaranteeOpacity + in 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 (default_proof_mode (),GuaranteesOpacity,ids), VtLater + then VtStartProof (default_proof_mode (),guarantee,ids), VtLater else VtSideff ids, VtLater (* Sideff: apply to all open branches. usually run on master only *) | VernacAssumption (_,_,l) -> |