diff options
| author | Emilio Jesus Gallego Arias | 2020-03-30 18:58:24 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-31 05:17:16 -0400 |
| commit | 7afd5e9fb7ba9e5fc41e41fd54eb90ee8cb13993 (patch) | |
| tree | 1d8ee10d5c7a8f38d79863ca4a99e5d83e612aee /tactics/declare.ml | |
| parent | 0eadf776ba78dcfdcab842f38f5de871ed337376 (diff) | |
[proof] Improve comment and argument name.
As suggested by Gaëtan Gilbert.
Diffstat (limited to 'tactics/declare.ml')
| -rw-r--r-- | tactics/declare.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/declare.ml b/tactics/declare.ml index a149850a64..324007930a 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -188,8 +188,8 @@ let record_aux env s_ty s_bo = let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types - ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) ?(univc=Univ.ContextSet.empty) body = - { proof_entry_body = Future.from_val ?fix_exn ((body,univc), eff); + ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) ?(univsbody=Univ.ContextSet.empty) body = + { proof_entry_body = Future.from_val ?fix_exn ((body,univsbody), eff); proof_entry_secctx = section_vars; proof_entry_type = types; proof_entry_universes = univs; |