From 8abacf00c6c39ec98085d531737d18edc9c19b2a Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 2 May 2019 19:46:02 +0200 Subject: Proof_global: pass only 1 pstate when we don't want the proof stack Typically instead of [start_proof : ontop:Proof_global.t option -> bla -> Proof_global.t] we have [start_proof : bla -> Proof_global.pstate] and the pstate is pushed on the stack by a caller around the vernacentries/mlg level. Naming can be a bit awkward, hopefully it can be improved (maybe in a followup PR). We can see some patterns appear waiting for nicer combinators, eg in mlg we often only want to work with the current proof, not the stack. Behaviour should be similar modulo bugs, let's see what CI says. --- plugins/extraction/extract_env.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/extraction/extract_env.mli') diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 7ba7e05019..efd5b5575f 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 option -> unit +val show_extraction : pstate:Proof_global.pstate -> unit -- cgit v1.2.3 From 99154fcb97653c606d2e62e0a0521c4afddff44c Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 20 May 2019 17:11:00 +0200 Subject: Rename Proof_global.{pstate -> t} --- plugins/extraction/extract_env.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/extraction/extract_env.mli') diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index efd5b5575f..7d04fee7c1 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.pstate -> unit +val show_extraction : pstate:Proof_global.t -> unit -- cgit v1.2.3