diff options
| author | Emilio Jesus Gallego Arias | 2019-05-22 05:33:10 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-24 20:54:43 +0200 |
| commit | fd2d2a8178d78e441fb3191cf112ed517dc791af (patch) | |
| tree | 8a85d441d2a25ad1ee4f46ef498694be9e9a8a12 /plugins/funind/recdef.ml | |
| parent | fb92bcc7830a084a4a204c4f58c44e83c180a9c9 (diff) | |
[proof] Remove duplicated universe polymorphic from decl_kinds
This information is already present on `Proof.t`, so we extract it
form there.
Moreover, this information is essential to the lower-level proof, as
opposed to the "kind" information which is only relevant to the vernac
layer; we will move it thus to its proper layer in subsequent commits.
Diffstat (limited to 'plugins/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index c97b39ff79..187d907dc5 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1370,7 +1370,8 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) () in let lemma = Lemmas.start_lemma ~name:na - ~kind:Decl_kinds.(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma) ~info + ~poly:false (* FIXME *) + ~kind:Decl_kinds.(Global ImportDefaultBehavior, Proof Lemma) ~info sigma gls_type in let lemma = if Indfun_common.is_strict_tcc () then @@ -1411,7 +1412,8 @@ let com_terminate let start_proof env ctx (tac_start:tactic) (tac_end:tactic) = let info = Lemmas.Info.make ~hook () in let lemma = Lemmas.start_lemma ~name:thm_name - ~kind:(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma) + ~poly:false (*FIXME*) + ~kind:(Global ImportDefaultBehavior, Proof Lemma) ~sign:(Environ.named_context_val env) ~info ctx @@ -1460,7 +1462,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation let evd = Evd.from_ctx uctx in let f_constr = constr_of_monomorphic_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in - let lemma = Lemmas.start_lemma ~name:eq_name ~kind:(Global ImportDefaultBehavior, false, Proof Lemma) ~sign evd + let lemma = Lemmas.start_lemma ~name:eq_name ~poly:false ~kind:(Global ImportDefaultBehavior, Proof Lemma) ~sign evd (EConstr.of_constr equation_lemma_type) in let lemma = fst @@ Lemmas.by (Proofview.V82.tactic (start_equation f_ref terminate_ref |