diff options
| author | Emilio Jesus Gallego Arias | 2020-06-23 23:07:04 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-26 14:38:13 +0200 |
| commit | 4ad9fa2b257184f9955216fc8345508c217c762d (patch) | |
| tree | 30d0b141653fbd6340535246420febbb44dc7f39 /vernac/comProgramFixpoint.ml | |
| parent | d9dca86f798ce11861f1a4715763cad1aae28e5a (diff) | |
[declare] Some more cleanup on unused functions after the last commits.
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 |