diff options
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index b04aaa7e6f..37615fa09c 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -262,7 +262,8 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = let uctx = Evd.evar_universe_context sigma in let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ () in let info = Declare.Info.make ~udecl ~poly ~hook () in - let _ : Declare.progress = Declare.Obls.add_definition ~cinfo ~info ~term:evars_def ~uctx evars in + let _ : Declare.Obls.progress = + Declare.Obls.add_definition ~cinfo ~info ~term:evars_def ~uctx evars in () let out_def = function |