diff options
| author | Emilio Jesus Gallego Arias | 2019-06-21 20:14:46 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-01 19:34:58 +0200 |
| commit | 66e52c88076ba830c8c8b3cf8e4bb77959fb7843 (patch) | |
| tree | ebb11957cdbad0e418ef7bb69cb75489c47ba6f6 /vernac/comFixpoint.ml | |
| parent | b78a4f8afc6180c1d435258af681d354e211cab2 (diff) | |
[api] Refactor most of `Decl_kinds`
We move the bulk of `Decl_kinds` to a better place [namely
`interp/decls`] and refactor the use of this information quite a bit.
The information seems to be used almost only for `Dumpglob`, so it
certainly should end there to achieve a cleaner core.
Note the previous commits, as well as the annotations regarding the
dubious use of the "variable" data managed by the `Decls` file.
IMO this needs more work, but this should be a good start.
Diffstat (limited to 'vernac/comFixpoint.ml')
| -rw-r--r-- | vernac/comFixpoint.ml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index e3428d6afc..cc2f7d9f70 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -20,7 +20,6 @@ open Names open Constrexpr open Constrexpr_ops open Constrintern -open Decl_kinds open Pretyping open Evarutil open Evarconv @@ -257,8 +256,8 @@ let interp_fixpoint ~cofix l ntns = let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns = let fix_kind, cofix, indexes = match indexes with - | Some indexes -> Fixpoint, false, indexes - | None -> CoFixpoint, true, [] + | Some indexes -> Decls.Fixpoint, false, indexes + | None -> Decls.CoFixpoint, true, [] in let thms = List.map3 (fun name t (ctx,impargs,_) -> @@ -269,7 +268,7 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in let evd = Evd.from_ctx ctx in let lemma = - Lemmas.start_lemma_with_initialization ~poly ~scope ~kind:(DefinitionBody fix_kind) ~udecl + Lemmas.start_lemma_with_initialization ~poly ~scope ~kind:(Decls.DefinitionBody fix_kind) ~udecl evd (Some(cofix,indexes,init_tac)) thms None in (* Declare notations *) List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; @@ -278,8 +277,8 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns = let indexes, cofix, fix_kind = match indexes with - | Some indexes -> indexes, false, Fixpoint - | None -> [], true, CoFixpoint + | Some indexes -> indexes, false, Decls.Fixpoint + | None -> [], true, Decls.CoFixpoint in (* We shortcut the proof process *) let fixdefs = List.map Option.get fixdefs in |