Remove the local polymorphic flag hack.

Some code in typeclasses was even breaking the invariant that
use_polymorphic_flag should not be called twice, but that code was
morally dead it seems, so we remove it.

2 files changed, 10 insertions, 11 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 6914f899b..4a2dba859 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -69,8 +69,7 @@ let existing_instance glob g info =
   let instance, _ = Global.type_of_global_in_context (Global.env ()) c in
   let _, r = Term.decompose_prod_assum instance in
     match class_of_constr Evd.empty (EConstr.of_constr r) with
-      | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob
-  (*FIXME*) (Flags.use_polymorphic_flag ()) c)
+      | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob c)
       | None -> user_err ?loc:(loc_of_reference g)
                          ~hdr:"declare_instance"
                          (Pp.str "Constant does not build instances of a declared type class.")
@@ -393,8 +392,7 @@ let context poly l =
       let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
         match class_of_constr sigma (of_constr t) with
 	| Some (rels, ((tc,_), args) as _cl) ->
-	    add_instance (Typeclasses.new_instance tc Hints.empty_hint_info false (*FIXME*)
-			    poly (ConstRef cst));
+            add_instance (Typeclasses.new_instance tc Hints.empty_hint_info false (ConstRef cst));
             status
 	    (* declare_subclasses (ConstRef cst) cl *)
 	| None -> status
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index aa6121c39..270e440e1 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2132,10 +2132,6 @@ let check_vernac_supports_polymorphism c p =
     | VernacExtend _ | VernacUniverse _ | VernacConstraint _) -> ()
   | Some _, _ -> user_err Pp.(str "This command does not support Polymorphism")
 
-let enforce_polymorphism = function
-  | None   -> Flags.is_universe_polymorphism ()
-  | Some b -> Flags.make_polymorphic_flag b; b
-
 (** A global default timeout, controlled by option "Set Default Timeout n".
     Use "Unset Default Timeout" to deactivate it (or set it to 0). *)
 
@@ -2202,6 +2198,7 @@ let with_fail st b f =
   end
 
 let interp ?(verbosely=true) ?proof ~st (loc,c) =
+  let orig_univ_poly = Flags.is_universe_polymorphism () in
   let orig_program_mode = Flags.is_program_mode () in
   let rec control = function
   | VernacExpr v ->
@@ -2241,7 +2238,8 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
     | c ->
       check_vernac_supports_locality c atts.locality;
       check_vernac_supports_polymorphism c polymorphism;
-      let polymorphic = enforce_polymorphism polymorphism in
+      let polymorphic = Option.default (Flags.is_universe_polymorphism ()) polymorphism in
+      Flags.make_universe_polymorphism polymorphic;
       Obligations.set_program_mode isprogcmd;
       try
         vernac_timeout begin fun () ->
@@ -2249,9 +2247,12 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
           if verbosely
           then Flags.verbosely (interp ?proof ~atts ~st) c
           else Flags.silently  (interp ?proof ~atts ~st) c;
+          (* If the command is `(Un)Set Program Mode` or `(Un)Set Universe Polymorphism`,
+             we should not restore the previous state of the flag... *)
           if orig_program_mode || not !Flags.program_mode || isprogcmd then
             Flags.program_mode := orig_program_mode;
-          ignore (Flags.use_polymorphic_flag ())
+          if (Flags.is_universe_polymorphism() = polymorphic) then
+            Flags.make_universe_polymorphism orig_univ_poly;
           end
         with
         | reraise when
@@ -2262,8 +2263,8 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
             let e = CErrors.push reraise in
             let e = locate_if_not_already ?loc e in
             let () = restore_timeout () in
+            Flags.make_universe_polymorphism orig_univ_poly;
             Flags.program_mode := orig_program_mode;
-	    ignore (Flags.use_polymorphic_flag ());
             iraise e
   in
   if verbosely