Merge PR #6405: Remove the local polymorphic flag hack.

12 files changed, 64 insertions, 69 deletions

diff --git a/API/API.mli b/API/API.mli
index 1d0c32273..2beebba32 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4331,7 +4331,7 @@ sig
   val class_info : Globnames.global_reference -> typeclass
   val mark_resolvables : ?filter:evar_filter -> Evd.evar_map -> Evd.evar_map
   val add_instance : instance -> unit
-  val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool -> Decl_kinds.polymorphic ->
+  val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool ->
                      Globnames.global_reference -> instance
 end
 
@@ -5798,7 +5798,7 @@ sig
   val lemInv_clause :
     Misctypes.quantified_hypothesis -> EConstr.constr -> Names.Id.t list -> unit Proofview.tactic
   val add_inversion_lemma_exn :
-    Names.Id.t -> Constrexpr.constr_expr -> Sorts.family -> bool -> (Names.Id.t -> unit Proofview.tactic) ->
+    poly:bool -> Names.Id.t -> Constrexpr.constr_expr -> Sorts.family -> bool -> (Names.Id.t -> unit Proofview.tactic) ->
     unit
 end
 
diff --git a/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh b/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh
new file mode 100644
index 000000000..c2e367038
--- /dev/null
+++ b/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh
@@ -0,0 +1,4 @@
+if [ "$CI_PULL_REQUEST" = "6405" ] || [ "$CI_BRANCH" = "rm-local-polymorphic-flag" ]; then
+    Equations_CI_BRANCH=rm-local-polymorphic-flag
+    Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
+fi
diff --git a/lib/flags.ml b/lib/flags.ml
index cd4a22d58..ee4c0734a 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -108,14 +108,6 @@ let universe_polymorphism = ref false
 let make_universe_polymorphism b = universe_polymorphism := b
 let is_universe_polymorphism () = !universe_polymorphism
 
-let local_polymorphic_flag = ref None
-let use_polymorphic_flag () = 
-  match !local_polymorphic_flag with 
-  | Some p -> local_polymorphic_flag := None; p
-  | None -> is_universe_polymorphism ()
-let make_polymorphic_flag b =
-  local_polymorphic_flag := Some b
-
 let polymorphic_inductive_cumulativity = ref false
 let make_polymorphic_inductive_cumulativity b = polymorphic_inductive_cumulativity := b
 let is_polymorphic_inductive_cumulativity () = !polymorphic_inductive_cumulativity
diff --git a/lib/flags.mli b/lib/flags.mli
index 62328e3d3..33d281798 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -74,10 +74,6 @@ val is_program_mode : unit -> bool
 val make_universe_polymorphism : bool -> unit
 val is_universe_polymorphism : unit -> bool
 
-(** Local universe polymorphism flag. *)
-val make_polymorphic_flag : bool -> unit
-val use_polymorphic_flag : unit -> bool
-
 (** Global polymorphic inductive cumulativity flag. *)
 val make_polymorphic_inductive_cumulativity : bool -> unit
 val is_polymorphic_inductive_cumulativity : unit -> bool
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 982fc7cc3..cf5125757 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -25,6 +25,7 @@ open Termops
 open Equality
 open Misctypes
 open Proofview.Notations
+open Vernacinterp
 
 DECLARE PLUGIN "ltac_plugin"
 
@@ -249,11 +250,10 @@ TACTIC EXTEND rewrite_star
 (**********************************************************************)
 (* Hint Rewrite                                                       *)
 
-let add_rewrite_hint bases ort t lcsr =
+let add_rewrite_hint ~poly bases ort t lcsr =
   let env = Global.env() in
   let sigma = Evd.from_env env in
-  let poly = Flags.use_polymorphic_flag () in
-  let f ce = 
+  let f ce =
     let c, ctx = Constrintern.interp_constr env sigma ce in
     let ctx =
       let ctx = UState.context_set ctx in
@@ -270,16 +270,16 @@ let add_rewrite_hint bases ort t lcsr =
 
 let classify_hint _ = Vernacexpr.VtSideff [], Vernacexpr.VtLater
 
-VERNAC COMMAND EXTEND HintRewrite CLASSIFIED BY classify_hint
+VERNAC COMMAND FUNCTIONAL EXTEND HintRewrite CLASSIFIED BY classify_hint
   [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] ->
-  [ add_rewrite_hint bl o None l ]
+  [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic bl o None l; st ]
 | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
     ":" preident_list(bl) ] ->
-  [ add_rewrite_hint bl o (Some t) l ]
+  [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic bl o (Some t) l; st ]
 | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] ->
-  [ add_rewrite_hint ["core"] o None l ]
+  [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic ["core"] o None l; st ]
 | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] ->
-  [ add_rewrite_hint ["core"] o (Some t) l ]
+  [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic ["core"] o (Some t) l; st ]
 END
 
 (**********************************************************************)
@@ -290,7 +290,7 @@ open EConstr
 open Vars
 open Coqlib
 
-let project_hint pri l2r r =
+let project_hint ~poly pri l2r r =
   let gr = Smartlocate.global_with_alias r in
   let env = Global.env() in
   let sigma = Evd.from_env env in
@@ -313,30 +313,28 @@ let project_hint pri l2r r =
   let id =
     Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l"))
   in
-  let poly = Flags.use_polymorphic_flag () in
   let ctx = Evd.const_univ_entry ~poly sigma in
   let c = EConstr.to_constr sigma c in
   let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in
   let info = {Vernacexpr.hint_priority = pri; hint_pattern = None} in
     (info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c))
 
-let add_hints_iff ?locality l2r lc n bl =
-  Hints.add_hints (Locality.make_module_locality locality) bl
-    (Hints.HintsResolveEntry (List.map (project_hint n l2r) lc))
+let add_hints_iff ~atts l2r lc n bl =
+  let open Vernacinterp in
+  Hints.add_hints (Locality.make_module_locality atts.locality) bl
+    (Hints.HintsResolveEntry (List.map (project_hint ~poly:atts.polymorphic n l2r) lc))
 
 VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF
   [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n)
     ":" preident_list(bl) ] ->
   [ fun ~atts ~st -> begin
-        let open Vernacinterp in
-        add_hints_iff ?locality:atts.locality true lc n bl;
+        add_hints_iff ~atts true lc n bl;
         st
       end
   ]
 | [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ] ->
   [ fun ~atts ~st -> begin
-        let open Vernacinterp in
-        add_hints_iff ?locality:atts.locality true lc n ["core"];
+        add_hints_iff ~atts true lc n ["core"];
         st
       end
   ]
@@ -346,15 +344,13 @@ VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffRL CLASSIFIED AS SIDEFF
   [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n)
     ":" preident_list(bl) ] ->
   [ fun ~atts ~st -> begin
-        let open Vernacinterp in
-        add_hints_iff ?locality:atts.locality false lc n bl;
+        add_hints_iff ~atts false lc n bl;
         st
       end
   ]
 | [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) ] ->
   [ fun ~atts ~st -> begin
-        let open Vernacinterp in
-        add_hints_iff ?locality:atts.locality false lc n ["core"];
+        add_hints_iff ~atts false lc n ["core"];
         st
       end
   ]
@@ -430,34 +426,46 @@ let seff id = Vernacexpr.VtSideff [id], Vernacexpr.VtLater
 | [ "Type" ] -> [ InType ]
 END*)
 
-VERNAC COMMAND EXTEND DeriveInversionClear
+VERNAC COMMAND FUNCTIONAL EXTEND DeriveInversionClear
 | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
   => [ seff na ]
-  -> [ add_inversion_lemma_exn na c s false inv_clear_tac ]
+  -> [ fun ~atts ~st ->
+      let open Vernacinterp in
+      add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_clear_tac; st ]
 
 | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => [ seff na ]
-  -> [ add_inversion_lemma_exn na c Sorts.InProp false inv_clear_tac ]
+  -> [ fun ~atts ~st ->
+      let open Vernacinterp in
+      add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_clear_tac; st ]
 END
 
-VERNAC COMMAND EXTEND DeriveInversion
+VERNAC COMMAND FUNCTIONAL EXTEND DeriveInversion
 | [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
   => [ seff na ]
-  -> [ add_inversion_lemma_exn na c s false inv_tac ]
+  -> [ fun ~atts ~st ->
+      let open Vernacinterp in
+      add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_tac; st ]
 
 | [ "Derive" "Inversion" ident(na) "with" constr(c) ] => [ seff na ]
-  -> [ add_inversion_lemma_exn na c Sorts.InProp false inv_tac ]
+  -> [ fun ~atts ~st ->
+      let open Vernacinterp in
+      add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_tac; st ]
 END
 
-VERNAC COMMAND EXTEND DeriveDependentInversion
+VERNAC COMMAND FUNCTIONAL EXTEND DeriveDependentInversion
 | [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
   => [ seff na ]
-  -> [ add_inversion_lemma_exn na c s true dinv_tac ]
+  -> [  fun ~atts ~st ->
+      let open Vernacinterp in
+      add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_tac; st ]
 END
 
-VERNAC COMMAND EXTEND DeriveDependentInversionClear
+VERNAC COMMAND FUNCTIONAL EXTEND DeriveDependentInversionClear
 | [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
   => [ seff na ]
-  -> [ add_inversion_lemma_exn na c s true dinv_clear_tac ]
+  -> [  fun ~atts ~st ->
+      let open Vernacinterp in
+      add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_clear_tac; st ]
 END
 
 (**********************************************************************)
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index a698b05dd..3cbb11001 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1981,8 +1981,7 @@ let add_morphism_infer glob m n =
 				 Decl_kinds.IsAssumption Decl_kinds.Logical)
       in
 	add_instance (Typeclasses.new_instance 
-			(Lazy.force PropGlobal.proper_class) Hints.empty_hint_info glob
-			poly (ConstRef cst));
+                        (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info glob (ConstRef cst));
 	declare_projection n instance_id (ConstRef cst)
     else
       let kind = Decl_kinds.Global, poly, 
@@ -1993,7 +1992,7 @@ let add_morphism_infer glob m n =
 	| Globnames.ConstRef cst ->
 	  add_instance (Typeclasses.new_instance 
 			  (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info
-			  glob poly (ConstRef cst));
+                          glob (ConstRef cst));
 	  declare_projection n instance_id (ConstRef cst)
 	| _ -> assert false
       in
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index bc9990d02..f153b6341 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -87,7 +87,6 @@ type instance = {
   (* Sections where the instance should be redeclared,
      None for discard, Some 0 for none. *)
   is_global: int option;
-  is_poly: bool;
   is_impl: global_reference;
 }
 
@@ -97,7 +96,7 @@ let instance_impl is = is.is_impl
 
 let hint_priority is = is.is_info.Vernacexpr.hint_priority
 
-let new_instance cl info glob poly impl =
+let new_instance cl info glob impl =
   let global =
     if glob then Some (Lib.sections_depth ())
     else None
@@ -107,7 +106,6 @@ let new_instance cl info glob poly impl =
     { is_class = cl.cl_impl;
       is_info = info ;
       is_global = global ;
-      is_poly = poly;
       is_impl = impl }
 
 (*
@@ -420,7 +418,7 @@ let declare_instance info local glob =
     match class_of_constr Evd.empty (EConstr.of_constr ty) with
     | Some (rels, ((tc,_), args) as _cl) ->
       assert (not (isVarRef glob) || local);
-      add_instance (new_instance tc info (not local) (Flags.use_polymorphic_flag ()) glob)
+      add_instance (new_instance tc info (not local) glob)
     | None -> ()
 
 let add_class cl =
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 0cbe1c71c..ee28ec173 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -53,7 +53,7 @@ val all_instances : unit -> instance list
 
 val add_class : typeclass -> unit
 
-val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool -> Decl_kinds.polymorphic ->
+val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool ->
   global_reference -> instance
 val add_instance : instance -> unit
 val remove_instance : instance -> unit
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 01065868d..197b3030d 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -234,10 +234,9 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   let p = Evarutil.nf_evars_universes sigma invProof in
     p, sigma
 
-let add_inversion_lemma name env sigma t sort dep inv_op =
+let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
   let invProof, sigma = inversion_scheme env sigma t sort dep inv_op in
   let univs =
-    let poly = Flags.use_polymorphic_flag () in
     Evd.const_univ_entry ~poly sigma
   in
   let entry = definition_entry ~univs invProof in
@@ -247,13 +246,13 @@ let add_inversion_lemma name env sigma t sort dep inv_op =
 (* inv_op = Inv (derives de complete inv. lemma)
  * inv_op = InvNoThining (derives de semi inversion lemma) *)
 
-let add_inversion_lemma_exn na com comsort bool tac =
+let add_inversion_lemma_exn ~poly na com comsort bool tac =
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let sigma, c = Constrintern.interp_type_evars env sigma com in
   let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid env sigma comsort in
   try
-    add_inversion_lemma na env sigma c sort bool tac
+    add_inversion_lemma ~poly na env sigma c sort bool tac
   with
     |   UserError (Some "Case analysis",s) -> (* Reference to Indrec *)
 	  user_err ~hdr:"Inv needs Nodep Prop Set" s
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index 8745ad397..f221b1fd9 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -14,6 +14,6 @@ open Misctypes
 val lemInv_clause :
   quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic
 
-val add_inversion_lemma_exn :
+val add_inversion_lemma_exn : poly:bool ->
   Id.t -> constr_expr -> Sorts.family -> bool -> (Id.t -> unit Proofview.tactic) ->
     unit
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 7aa27dcdf..ded0d97e6 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