diff options
| author | Emilio Jesus Gallego Arias | 2018-10-11 00:20:24 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-30 23:14:55 +0100 |
| commit | 3429abee7c572676fa1155bf1620386bdf10d798 (patch) | |
| tree | b85975f0e1e9115ab65902463af9aff356b15c72 /vernac/comFixpoint.ml | |
| parent | acd0c18829a03159c489d908ce8f5f510de2f347 (diff) | |
[vernac] [hooks] Refactor towards optional hooks.
We make `declaration_hook`s optional arguments everywhere, and thus we
avoid some "fake" functions having to be passed.
This identifies positively the code really using hooks [funind,
rewrite, coercions, program, and canonicals] and helps moving toward
some hope of reification.
Diffstat (limited to 'vernac/comFixpoint.ml')
| -rw-r--r-- | vernac/comFixpoint.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 274c99107f..77227b64e6 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -261,7 +261,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind fixdefs) in let evd = Evd.from_ctx ctx in Lemmas.start_proof_with_initialization (local,poly,DefinitionBody Fixpoint) - evd pl (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) + evd pl (Some(false,indexes,init_tac)) thms None else begin (* We shortcut the proof process *) let fixdefs = List.map Option.get fixdefs in @@ -296,7 +296,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n fixdefs) in let evd = Evd.from_ctx ctx in Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint) - evd pl (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) + evd pl (Some(true,[],init_tac)) thms None else begin (* We shortcut the proof process *) let fixdefs = List.map Option.get fixdefs in |