From 60bc3cbe72083f4fa1aa759914936e4fa3d6b42e Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 13 Apr 2011 14:29:02 +0000
Subject: 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
---
 plugins/funind/recdef.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'plugins/funind/recdef.ml')

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
-- 
cgit v1.2.3