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

1 files changed, 4 insertions, 7 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index ea606210bd..90376a4311 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -64,7 +64,7 @@ let red_constant_entry n ce = function
       { ce with const_entry_body =
 	under_binders (Global.env()) (fst (reduction_of_red_expr red)) n body }
 
-let interp_definition bl p red_option c ctypopt =
+let interp_definition bl red_option c ctypopt =
   let env = Global.env() in
   let evdref = ref Evd.empty in
   let impls, ((env_bl, ctx), imps1) = interp_context_evars evdref env bl in
@@ -78,7 +78,6 @@ let interp_definition bl p red_option c ctypopt =
 	imps1@(Impargs.lift_implicits nb_args imps2),
 	{ const_entry_body = body;
 	  const_entry_type = None;
-	  const_entry_polymorphic = p;
           const_entry_opaque = false }
     | Some ctyp ->
 	let ty, impsty = interp_type_evars_impls ~impls ~evdref ~fail_evar:false env_bl ctyp in
@@ -90,7 +89,6 @@ let interp_definition bl p red_option c ctypopt =
 	imps1@(Impargs.lift_implicits nb_args imps2),
 	{ const_entry_body = body;
 	  const_entry_type = Some typ;
-	  const_entry_polymorphic = p;
           const_entry_opaque = false }
   in
   red_constant_entry (rel_context_length ctx) ce red_option, imps
@@ -128,7 +126,7 @@ let declare_definition ident (local,k) ce imps hook =
 
 (* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
 
-let declare_assumption is_coe (local,p,kind) c imps impl nl (_,ident) =
+let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) =
   let r = match local with
     | Local when Lib.sections_are_opened () ->
         let _ =
@@ -474,7 +472,6 @@ let declare_fix kind f def t imps =
   let ce = {
     const_entry_body = def;
     const_entry_type = Some t;
-    const_entry_polymorphic = false;
     const_entry_opaque = false }
   in
   let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in
@@ -554,7 +551,7 @@ let declare_fixpoint ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns =
     let init_tac =
       Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
         fixdefs) in
-    Lemmas.start_proof_with_initialization (Global,false,DefinitionBody Fixpoint)
+    Lemmas.start_proof_with_initialization (Global,DefinitionBody Fixpoint)
       (Some(false,indexes,init_tac)) thms None (fun _ _ -> ())
   else begin
     (* We shortcut the proof process *)
@@ -579,7 +576,7 @@ let declare_cofixpoint ((fixnames,fixdefs,fixtypes),fiximps) ntns =
     let init_tac =
       Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
         fixdefs) in
-    Lemmas.start_proof_with_initialization (Global,false,DefinitionBody CoFixpoint)
+    Lemmas.start_proof_with_initialization (Global,DefinitionBody CoFixpoint)
       (Some(true,[],init_tac)) thms None (fun _ _ -> ())
   else begin
     (* We shortcut the proof process *)