From c8883873426c92778a1cac02da17e3d123beb394 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 10 Oct 2018 23:35:47 +0200 Subject: [vernac] Remove unused abstraction from declaration_hook type. "Declaration" hooks can be polymorphic on their return type, however this facility doesn't seem used in the codebase. We thus remove the polymorphism with the hope to be able to reify the control later on. --- vernac/comProgramFixpoint.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'vernac/comProgramFixpoint.ml') 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 -- cgit v1.2.3