diff options
| author | Emilio Jesus Gallego Arias | 2020-05-25 14:13:54 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-26 14:38:10 +0200 |
| commit | 2ac5353d24133cbca97a85617942d38aed0cc9a3 (patch) | |
| tree | f20d64ad3dba698c30ddfb2c53a6d64fcdd0eeab /vernac/comFixpoint.ml | |
| parent | 43d381ab20035f64ce2edea8639fcd9e1d0453bc (diff) | |
[declare] Remove mutual internals from Info.t structure.
We move the advanced proof initialization routine to Declare, and stop
exposing implementation internals in `Info.t` constructor.
Diffstat (limited to 'vernac/comFixpoint.ml')
| -rw-r--r-- | vernac/comFixpoint.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 2995df4a66..5bf3350777 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -271,7 +271,7 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs let init_terms = Some fixdefs in let evd = Evd.from_ctx ctx in let lemma = - Lemmas.start_lemma_with_initialization ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl + Declare.start_proof_with_initialization ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl evd (Some(cofix,indexes,init_terms)) thms None in (* Declare notations *) List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; |