diff options
| author | msozeau | 2011-04-13 14:29:02 +0000 |
|---|---|---|
| committer | msozeau | 2011-04-13 14:29:02 +0000 |
| commit | 60bc3cbe72083f4fa1aa759914936e4fa3d6b42e (patch) | |
| tree | 0eeffe9b7b098ad653ffeb6ad963c62223245d0e /plugins/funind/recdef.ml | |
| parent | 3b11686e4f78f6d166f84d990ac4fedb4d3e800a (diff) | |
Revert "Add [Polymorphic] flag for defs"
This reverts commit 33434695615806a85cec88452c93ea69ffc0e719.
Conflicts:
kernel/term_typing.ml
test-suite/success/polymorphism.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13998 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 24379e7b4e..11fbc01baf 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1021,7 +1021,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ in start_proof na - (Decl_kinds.Global, false, Decl_kinds.Proof Decl_kinds.Lemma) + (Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma) sign gls_type hook ; @@ -1071,7 +1071,7 @@ let com_terminate let start_proof (tac_start:tactic) (tac_end:tactic) = let (evmap, env) = Lemmas.get_current_context() in start_proof thm_name - (Global, false, Proof Lemma) (Environ.named_context_val env) + (Global, Proof Lemma) (Environ.named_context_val env) (hyp_terminates nb_args fonctional_ref) hook; by (observe_tac "starting_tac" tac_start); @@ -1140,7 +1140,6 @@ let (declare_fun : identifier -> logical_kind -> constr -> global_reference) = fun f_id kind value -> let ce = {const_entry_body = value; const_entry_type = None; - const_entry_polymorphic = false; const_entry_opaque = false } in ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; @@ -1350,7 +1349,7 @@ let (com_eqn : int -> identifier -> let (evmap, env) = Lemmas.get_current_context() in let f_constr = (constr_of_global f_ref) in let equation_lemma_type = subst1 f_constr equation_lemma_type in - (start_proof eq_name (Global, false, Proof Lemma) + (start_proof eq_name (Global, Proof Lemma) (Environ.named_context_val env) equation_lemma_type (fun _ _ -> ()); by (start_equation f_ref terminate_ref |