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

6 files changed, 10 insertions, 12 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index c1b3c0b849..4f32bbd99d 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -973,7 +973,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
       Ensures by: obvious
       i*)
     (mk_equation_id f_id)
-    (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem))
+    (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
     lemma_type
     (fun _ _ -> ());
   Pfedit.by (prove_replacement);
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index d3949731bc..2ba29ced7a 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -333,7 +333,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
   begin
     Lemmas.start_proof
       new_princ_name
-      (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem))
+      (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
       new_principle_type
       (hook new_principle_type)
     ;
@@ -382,7 +382,6 @@ let generate_functional_principle
 	let ce =
 	  { const_entry_body = value;
 	    const_entry_type = None;
-	    const_entry_polymorphic = false;
 	    const_entry_opaque = false }
 	in
 	ignore(
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 0e4dd12896..dd48765fb5 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -351,9 +351,9 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
     | [((_,fname),_,bl,ret_type,body),_] when not is_rec ->
       let body = match body with | Some body -> body | None -> user_err_loc (dummy_loc,"Function",str "Body of Function must be given") in 
 	let ce,imps =
-	  Command.interp_definition bl false None body (Some ret_type)
+	  Command.interp_definition bl None body (Some ret_type)
 	in
-	Command.declare_definition 
+	Command.declare_definition
 	  fname (Decl_kinds.Global,Decl_kinds.Definition)
 	  ce imps (fun _ _ -> ())
     | _ ->
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index a0d2061bcd..094d2e50fd 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -156,7 +156,7 @@ let definition_message id =
   Flags.if_verbose message ((string_of_id id) ^ " is defined")
 
 
-let save with_clean id const (locality,p,kind) hook =
+let save with_clean id const (locality,kind) hook =
   let {const_entry_body = pft;
        const_entry_type = tpo;
        const_entry_opaque = opacity } = const in
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index ce484ca236..426b496dd1 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -788,7 +788,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	     Ensures by: obvious
 	     i*)
 	   (mk_correct_id f_id)
-	   (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem))
+	   (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
 	   (fst lemmas_types_infos.(i))
 	   (fun _ _ -> ());
 	 Pfedit.by (observe_tac ("prove correctness ("^(string_of_id f_id)^")") (proving_tac i));
@@ -840,7 +840,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	     Ensures by: obvious
 	     i*)
 	   (mk_complete_id f_id)
-	   (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem))
+	   (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
 	   (fst lemmas_types_infos.(i))
 	   (fun _ _ -> ());
 	 Pfedit.by (observe_tac ("prove completeness ("^(string_of_id f_id)^")") (proving_tac i));
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