diff options
| author | Emilio Jesus Gallego Arias | 2020-04-02 01:41:20 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-15 11:12:10 -0400 |
| commit | 0c748e670ef1a81cb35c1cc55892dba141c25930 (patch) | |
| tree | d90cc4362019557a74d6d1ac46701e0d6178e8ce /plugins/extraction | |
| parent | 9908ce57e15a316ff692ce31f493651734998ded (diff) | |
[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.
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/extract_env.ml | 6 | ||||
| -rw-r--r-- | plugins/extraction/extract_env.mli | 2 |
2 files changed, 4 insertions, 4 deletions
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 |