diff options
| author | Pierre-Marie Pédrot | 2019-06-25 17:26:44 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-25 17:26:44 +0200 |
| commit | 7dfcb0f7c817e66280ab37b6c653b5596a16c249 (patch) | |
| tree | f59cbad4ef2e56070fe32fefcc5f7a3f8c6b7a4a /stm | |
| parent | 7024688c4e20fa7b70ac1c550c166d02fce8d15c (diff) | |
| parent | c2abcaefd796b7f430f056884349b9d959525eec (diff) | |
Merge PR #10316: [lemmas] Reify info for implicits, universe decls, and rec theorems.
Reviewed-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: gares
Reviewed-by: ppedrot
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 6 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 6 |
2 files changed, 6 insertions, 6 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 89d95d0cc9..28d5447c44 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.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_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 *) @@ -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 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 = |