diff options
| author | Emilio Jesus Gallego Arias | 2018-10-10 23:35:47 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-11 22:52:32 +0200 |
| commit | c8883873426c92778a1cac02da17e3d123beb394 (patch) | |
| tree | 9ffcf82e3787d11c447851dd850ec1cdd4d3611d /vernac/comProgramFixpoint.ml | |
| parent | 27fd525445e8ab37e67eebfb2bca1963e33c7f64 (diff) | |
[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.
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 |