diff options
| author | Maxime Dénès | 2016-09-20 09:11:09 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-09-20 17:18:36 +0200 |
| commit | aa29c92dfa395e2f369e81bd72cef482cdf90c65 (patch) | |
| tree | fbffe7f83d1d76a21d39bf90b93d8f948aa42143 /plugins/funind/recdef.ml | |
| parent | 424de98770e1fd8c307a7cd0053c268a48532463 (diff) | |
Stylistic improvements in intf/decl_kinds.mli.
We get rid of tuples containing booleans (typically for universe
polymorphism) by replacing them with records.
The previously common idom:
if pi2 kind (* polymorphic *) then ... else ...
becomes:
if kind.polymorphic then ... else ...
To make the construction and destruction of these records lightweight,
the labels of boolean arguments for universe polymorphism are now
usually also called "polymorphic".
Diffstat (limited to 'plugins/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index f43251bc50..75495ed989 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1348,7 +1348,9 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp in Lemmas.start_proof na - (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma) + { locality = Decl_kinds.Global; + polymorphic = false (* FIXME *); + object_kind = Decl_kinds.Proof Decl_kinds.Lemma } sigma gls_type (Lemmas.mk_hook hook); if Indfun_common.is_strict_tcc () @@ -1394,8 +1396,12 @@ let com_terminate hook = let start_proof ctx (tac_start:tactic) (tac_end:tactic) = let (evmap, env) = Lemmas.get_current_context() in + let goal_kind = { locality = Global; + polymorphic = false; (* FIXME *) + object_kind = Proof Lemma } + in Lemmas.start_proof thm_name - (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) + goal_kind ~sign:(Environ.named_context_val env) ctx (compute_terminate_type nb_args fonctional_ref) hook; ignore (by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start))); @@ -1445,7 +1451,11 @@ let (com_eqn : int -> Id.t -> let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in let f_constr = constr_of_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in - (Lemmas.start_proof eq_name (Global, false, Proof Lemma) + let goal_kind = { locality = Global; + polymorphic = false; + object_kind = Proof Lemma } + in + (Lemmas.start_proof eq_name goal_kind ~sign:(Environ.named_context_val env) evmap equation_lemma_type |