From 599f61a45769d5938758e0fcbd479b9c8f493a58 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 9 Jun 2019 18:51:39 +0200 Subject: [lemmas] Reify info for implicits, univ_decls, prepare for rec_thms. Key information about an interactive lemma proof was stored as a closure on an ad-hoc hook, then later made available to the hook closing actions. Instead, we put this information in the lemma state and incorporate these declarations into the normal save path. We prepare to put the information about rec_thms in the state too. --- stm/stm.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 89d95d0cc9..2fefb7fbb3 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1537,7 +1537,7 @@ end = struct (* {{{ *) let st = Vernacstate.freeze_interp_state ~marshallable:false in stm_vernac_interp stop - ~proof:(pobject, Lemmas.default_info) st + ~proof:(pobject, Lemmas.default_lemma_info) st { verbose = false; indentation = 0; strlen = 0; expr = CAst.make ?loc @@ VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in ignore(Future.join checked_proof); @@ -1677,7 +1677,7 @@ end = struct (* {{{ *) let pterm, _info = PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in - let proof = pterm, Lemmas.default_info in + let proof = pterm, Lemmas.default_lemma_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 *) -- cgit v1.2.3 From 17ba18d81e5fe3dc153b1c12ac1b8daeb5474d48 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 2 May 2019 06:10:29 +0200 Subject: [lemmas] Turn Lemmas.info into a proper type with constructor. Lemmas.info was a bit out of hand, as well as the parameters to the `start_*` family. Most of the info is not needed and should hopefully remain constrained to special cases, most callers only set the hook, and obligations should be better served by a `start_obligation` function soon. --- stm/stm.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 2fefb7fbb3..b73d3dcdeb 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1537,7 +1537,7 @@ end = struct (* {{{ *) let st = Vernacstate.freeze_interp_state ~marshallable:false in stm_vernac_interp stop - ~proof:(pobject, Lemmas.default_lemma_info) st + ~proof:(pobject, Lemmas.Info.make ()) st { verbose = false; indentation = 0; strlen = 0; expr = CAst.make ?loc @@ VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in ignore(Future.join checked_proof); @@ -1677,7 +1677,7 @@ end = struct (* {{{ *) let pterm, _info = PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in - let proof = pterm, Lemmas.default_lemma_info in + let proof = pterm, Lemmas.Info.make () 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 *) -- cgit v1.2.3 From da5bbda84bd22b87a6057175c9d4d2391808e294 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 6 Jun 2019 17:28:26 +0200 Subject: [api] [proof] Move `discharge` type to vernac_ast where it is used. This seems like the right location, a bit more refactoring should be possible. --- stm/vernac_classifier.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'stm') diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 4e7f6a0ac6..aaba36287a 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -87,7 +87,7 @@ let classify_vernac e = VtProofStep { parallel = `No; proof_block_detection = Some "curly" } (* StartProof *) - | VernacDefinition ((Decl_kinds.DoDischarge,_),({v=i},_),ProveBody _) -> + | VernacDefinition ((DoDischarge,_),({v=i},_),ProveBody _) -> VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i) | VernacDefinition (_,({v=i},_),ProveBody _) -> @@ -102,7 +102,7 @@ let classify_vernac e = | VernacFixpoint (discharge,l) -> let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in let guarantee = - if discharge = Decl_kinds.DoDischarge || polymorphic then Doesn'tGuaranteeOpacity + if discharge = DoDischarge || polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in let ids, open_proof = @@ -114,7 +114,7 @@ let classify_vernac e = | VernacCoFixpoint (discharge,l) -> let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in let guarantee = - if discharge = Decl_kinds.DoDischarge || polymorphic then Doesn'tGuaranteeOpacity + if discharge = DoDischarge || polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in let ids, open_proof = -- cgit v1.2.3 From 0c47ebf825690675cbb71153b8c9e4f7f6858984 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 11 Jun 2019 02:02:15 +0200 Subject: [proof] API Documentation fixes. --- stm/stm.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index b73d3dcdeb..28d5447c44 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1735,7 +1735,7 @@ end = struct (* {{{ *) | `OK (po,_) -> let con = Nametab.locate_constant - (Libnames.qualid_of_ident po.Proof_global.id) in + (Libnames.qualid_of_ident po.Proof_global.name) in let c = Global.lookup_constant con in let o = match c.Declarations.const_body with | Declarations.OpaqueDef o -> o -- cgit v1.2.3