diff options
| author | Emilio Jesus Gallego Arias | 2019-06-21 20:56:33 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-01 19:34:58 +0200 |
| commit | 0bc7e7405553dc63d9693e85c3ce1485b5e8fe23 (patch) | |
| tree | 29a75b9b4edf5e20e939ab9c5779c5516294517d /plugins/funind/recdef.ml | |
| parent | fa1782e05eeb6f18871d26cc43670d35ed73bf23 (diff) | |
[declare] Separate kinds from entries in constant declaration
They are clearly not at the same importance level, thus we use a named
parameter and isolate the kinds as to allow further improvements and
refactoring.
Diffstat (limited to 'plugins/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 0398acf242..a05feed1d1 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -65,9 +65,9 @@ let find_reference sl s = let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in locate (make_qualid dp (Id.of_string s)) -let declare_fun f_id kind ?univs value = +let declare_fun name kind ?univs value = let ce = definition_entry ?univs value (*FIXME *) in - ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; + ConstRef(declare_constant ~name ~kind (DefinitionEntry ce)) let defined lemma = Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None |