diff options
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 |