diff options
| author | Emilio Jesus Gallego Arias | 2020-03-15 17:52:16 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-07-08 15:12:46 +0200 |
| commit | 54788df72ce79998ee27db362401a56bda4daceb (patch) | |
| tree | fd81263a9139e00eea38e678f62f106f4da81e4c /vernac/comProgramFixpoint.mli | |
| parent | e0474577f9b83249d69b0f5b5942d6a6bbb1055b (diff) | |
[obligations] Functionalize Program state
In our quest to unify all the declaration paths, an important step
is to account for the state pertaining to `Program` declarations.
Whereas regular proofs keep are kept in a stack-like structure;
obligations for constants defined by `Program` are stored in a global
map which is manipulated by almost regular open/close proof primitives.
We make this manipulation explicit by handling the program state
functionally, in a similar way than we already do for lemmas.
This requires to extend the proof DSL a bit; but IMO changes are
acceptable given the gain.
Most of the PR is routine; only remarkable change is that the hook is
called explicitly in `finish_admitted` as it had to learn about the
different types of proof_endings.
Note that we could have gone deeper and use the type system to refine
the core proof type; IMO it is still too preliminary so it is better
to do this step as an intermediate one towards a deeper unification.
Diffstat (limited to 'vernac/comProgramFixpoint.mli')
| -rw-r--r-- | vernac/comProgramFixpoint.mli | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli index e39f62c348..7935cf27fb 100644 --- a/vernac/comProgramFixpoint.mli +++ b/vernac/comProgramFixpoint.mli @@ -11,11 +11,16 @@ open Vernacexpr (** Special Fixpoint handling when command is activated. *) - val do_fixpoint : - (* When [false], assume guarded. *) - scope:Locality.locality -> poly:bool -> fixpoint_expr list -> unit + pm:Declare.OblState.t + -> scope:Locality.locality + -> poly:bool + -> fixpoint_expr list + -> Declare.OblState.t val do_cofixpoint : - (* When [false], assume guarded. *) - scope:Locality.locality -> poly:bool -> cofixpoint_expr list -> unit + pm:Declare.OblState.t + -> scope:Locality.locality + -> poly:bool + -> cofixpoint_expr list + -> Declare.OblState.t |