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, 14 insertions, 17 deletions

diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index d21b83ab65..4bf6e59f13 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -347,20 +347,18 @@ let pr_class_rawexpr = function
   | SortClass -> str"Sortclass"
   | RefClass qid -> pr_smart_global qid
 
-let pr_assumption_token many (l,p,k) = 
-  let s = match l, k with
-    | (Local,Logical) ->
-	str (if many then "Hypotheses" else "Hypothesis")
-    | (Local,Definitional) ->
-	str (if many then "Variables" else "Variable")
-    | (Global,Logical) ->
-	str (if many then "Axioms" else "Axiom")
-    | (Global,Definitional) ->
-	str (if many then "Parameters" else "Parameter")
-    | (Global,Conjectural) -> str"Conjecture"
-    | (Local,Conjectural) ->
-	anomaly "Don't know how to beautify a local conjecture"
-  in if p then str "Polymorphic " ++ s else s
+let pr_assumption_token many = function
+  | (Local,Logical) ->
+      str (if many then "Hypotheses" else "Hypothesis")
+  | (Local,Definitional) ->
+      str (if many then "Variables" else "Variable")
+  | (Global,Logical) ->
+      str (if many then "Axioms" else "Axiom")
+  | (Global,Definitional) ->
+      str (if many then "Parameters" else "Parameter")
+  | (Global,Conjectural) -> str"Conjecture"
+  | (Local,Conjectural) ->
+      anomaly "Don't know how to beautify a local conjecture"
 
 let pr_params pr_c (xl,(c,t)) =
   hov 2 (prlist_with_sep sep pr_lident xl ++ spc() ++
@@ -571,7 +569,7 @@ let rec pr_vernac = function
         | None -> mt()
         | Some cc -> str" :=" ++ spc() ++ cc))
 
-  | VernacStartTheoremProof (ki,p,l,_,_) ->
+  | VernacStartTheoremProof (ki,l,_,_) ->
       hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++
              prlist (pr_statement (spc () ++ str "with")) (List.tl l))
 
@@ -692,11 +690,10 @@ let rec pr_vernac = function
 (* 	  prlist_with_sep (fun () -> str";" ++ spc())  *)
 (* 	  (fun (lid,oc,c) -> pr_lident_constr ((if oc then str" :>" else str" :") ++ spc()) (lid,c)) props ) *)
 
- | VernacInstance (abst,glob,poly,sup,(instid, bk, cl),props,pri) ->
+ | VernacInstance (abst,glob, sup, (instid, bk, cl), props, pri) ->
      hov 1 (
        pr_non_locality (not glob) ++
        (if abst then str"Declare " else mt ()) ++
-       (if poly then str"Polymorphic " else mt ()) ++
        str"Instance" ++ spc () ++
 	 pr_and_type_binders_arg sup ++
 	 str"=>" ++ spc () ++