diff options
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index c33e6b72c6..ab898644c0 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -192,7 +192,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let name = add_suffix recname "_func" in (* XXX: Mutating the evar_map in the hook! *) (* XXX: Likely the sigma is out of date when the hook is called .... *) - let hook sigma l gr _ = + let hook sigma _ l gr = let sigma, h_body = Evarutil.new_global sigma gr in let body = it_mkLambda_or_LetIn (mkApp (h_body, [|make|])) binders_rel in let ty = it_mkProd_or_LetIn top_arity binders_rel in @@ -211,13 +211,13 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = hook, name, typ else let typ = it_mkProd_or_LetIn top_arity binders_rel in - let hook sigma l gr _ = + let hook sigma _ l gr = if Impargs.is_implicit_args () || not (List.is_empty impls) then Impargs.declare_manual_implicits false gr [impls] in hook, recname, typ in (* XXX: Capturing sigma here... bad bad *) - let hook = Lemmas.mk_hook (hook sigma) in + let hook = Obligations.mk_univ_hook (hook sigma) in (* XXX: Grounding non-ground terms here... bad bad *) let fullcoqc = EConstr.to_constr ~abort_on_undefined_evars:false sigma def in let fullctyp = EConstr.to_constr sigma typ in |