From 9908ce57e15a316ff692ce31f493651734998ded Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 2 Apr 2020 01:08:24 -0400 Subject: [proof] Move proof_global functionality to Proof_global from Pfedit This actually gets `Pfedit` out of the dependency picture [can be almost merged with `Proof` now, as it is what it manipulates] and would allow to reduce the exported low-level API from `Proof_global`, as `map_fold_proof` is not used anymore. --- plugins/extraction/extract_env.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 3a90d24c97..40dbf8bea4 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -729,7 +729,7 @@ let extract_and_compile l = let show_extraction ~pstate = init ~inner:true false false; let prf = Proof_global.get_proof pstate in - let sigma, env = Pfedit.get_current_context pstate in + let sigma, env = Proof_global.get_current_context pstate in let trms = Proof.partial_proof prf in let extr_term t = let ast, ty = extract_constr env sigma t in -- cgit v1.2.3 From 0c748e670ef1a81cb35c1cc55892dba141c25930 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 2 Apr 2020 01:41:20 -0400 Subject: [proof] Merge `Proof_global` into `Declare` We place creation and saving of interactive proofs in the same module; this will allow to make `proof_entry` private, improving invariants and control over clients, and to reduce the API [for example next commit will move abstract declaration into this module, removing the exported ad-hoc `build_constant_by_tactic`] Next step will be to unify all the common code in the interactive / non-interactive case; but we need to tweak the handling of obligations first. --- plugins/extraction/extract_env.ml | 6 +++--- plugins/extraction/extract_env.mli | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 40dbf8bea4..7f8e8b36ad 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -728,13 +728,13 @@ let extract_and_compile l = (* Show the extraction of the current ongoing proof *) let show_extraction ~pstate = init ~inner:true false false; - let prf = Proof_global.get_proof pstate in - let sigma, env = Proof_global.get_current_context pstate in + let prf = Declare.get_proof pstate in + let sigma, env = Declare.get_current_context pstate in let trms = Proof.partial_proof prf in let extr_term t = let ast, ty = extract_constr env sigma t in let mp = Lib.current_mp () in - let l = Label.of_id (Proof_global.get_proof_name pstate) in + let l = Label.of_id (Declare.get_proof_name pstate) in let fake_ref = GlobRef.ConstRef (Constant.make2 mp l) in let decl = Dterm (fake_ref, ast, ty) in print_one_decl [] mp decl diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index edbc1f5ea7..2e1509c5cc 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -40,4 +40,4 @@ val structure_for_compute : (* Show the extraction of the current ongoing proof *) -val show_extraction : pstate:Proof_global.t -> unit +val show_extraction : pstate:Declare.t -> unit -- cgit v1.2.3 From 1dc70876b4a5ad027b3b73aa6ba741e89320d17d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 11 Apr 2020 17:14:38 -0400 Subject: [declare] Rename `Declare.t` to `Declare.Proof.t` This still needs API cleanup but we defer it to the moment we are ready to make the internals private. --- plugins/extraction/extract_env.ml | 4 ++-- plugins/extraction/extract_env.mli | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 7f8e8b36ad..02383799a9 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -728,13 +728,13 @@ let extract_and_compile l = (* Show the extraction of the current ongoing proof *) let show_extraction ~pstate = init ~inner:true false false; - let prf = Declare.get_proof pstate in + let prf = Declare.Proof.get_proof pstate in let sigma, env = Declare.get_current_context pstate in let trms = Proof.partial_proof prf in let extr_term t = let ast, ty = extract_constr env sigma t in let mp = Lib.current_mp () in - let l = Label.of_id (Declare.get_proof_name pstate) in + let l = Label.of_id (Declare.Proof.get_proof_name pstate) in let fake_ref = GlobRef.ConstRef (Constant.make2 mp l) in let decl = Dterm (fake_ref, ast, ty) in print_one_decl [] mp decl diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 2e1509c5cc..06cc475200 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -40,4 +40,4 @@ val structure_for_compute : (* Show the extraction of the current ongoing proof *) -val show_extraction : pstate:Declare.t -> unit +val show_extraction : pstate:Declare.Proof.t -> unit -- cgit v1.2.3