diff options
| author | Emilio Jesus Gallego Arias | 2019-02-24 20:27:09 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-17 12:30:13 +0200 |
| commit | 7dc04f0244aeb277b62070f87590cbc2cafd8396 (patch) | |
| tree | a11175ee231e93c351f0a70bece257f6de840c4e /stm | |
| parent | a296e879112f2e88b2fdfbf2fe90f1807f90b890 (diff) | |
[proof] drop parameter from terminator type
This makes the type of terminator simpler, progressing towards its
total reification.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 13 |
1 files changed, 5 insertions, 8 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 4f435f1fa5..13996aca0f 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1532,15 +1532,12 @@ end = struct (* {{{ *) (* Unfortunately close_future_proof and friends are not pure so we need to set the state manually here *) State.unfreeze st; - let pobject, _terminator, _hook = + let pobject, _info = PG_compat.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in - let terminator = (* The one sent by master is an InvalidKey *) - Lemmas.(standard_proof_terminator []) in - let st = Vernacstate.freeze_interp_state ~marshallable:false in stm_vernac_interp stop - ~proof:(pobject, terminator, None) st + ~proof:(pobject, Lemmas.default_info) st { verbose = false; indentation = 0; strlen = 0; expr = CAst.make ?loc @@ VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in ignore(Future.join checked_proof); @@ -1677,10 +1674,10 @@ end = struct (* {{{ *) let opaque = Proof_global.Opaque in (* The original terminator, a hook, has not been saved in the .vio*) - let pterm, _invalid_terminator, _hook = + let pterm, _info = PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in - let proof = pterm , Lemmas.standard_proof_terminator [], None in + let proof = pterm, Lemmas.default_info in (* We jump at the beginning since the kernel handles side effects by also * looking at the ones that happen to be present in the current env *) @@ -1735,7 +1732,7 @@ end = struct (* {{{ *) | `ERROR -> exit 1 | `ERROR_ADMITTED -> cst, false | `OK_ADMITTED -> cst, false - | `OK (po,_,_) -> + | `OK (po,_) -> let con = Nametab.locate_constant (Libnames.qualid_of_ident po.Proof_global.id) in |