Adapt to coq/coq#18327 (projection opacity)

src/equations.ml

@@ -45,7 +45,7 @@ let define_unfolding_eq ~pm env evd flags p unfp prog prog' ei hook =
   let funfc = e_new_global evd info'.term_id in
   let unfold_eq_id = add_suffix (program_id unfp) "_eq" in
   let hook_eqs _ pm =
-    Global.set_strategy (ConstKey funf_cst) Conv_oracle.transparent;
+    Global.set_strategy (Evaluable.EvalConstRef funf_cst) Conv_oracle.transparent;
     let () = (* Declare the subproofs of unfolding for where as rewrite rules *)
       let decl _ (_, id, _) =
         let gr =

src/equations_common.ml

@@ -434,7 +434,7 @@ let coq_ImpossibleCall evd = find_constant "impossiblecall.class" evd
 
 let unfold_add_pattern =
   lazy (Tactics.unfold_in_concl [(Locus.AllOccurrences,
-			     Tacred.EvalConstRef (Globnames.destConstRef (Lazy.force coq_add_pattern)))])
+			     Evaluable.EvalConstRef (Globnames.destConstRef (Lazy.force coq_add_pattern)))])
 
 let subterm_relation_base = "subterm_relation"
 
@@ -516,14 +516,19 @@ let lift_list l = List.map (Vars.lift 1) l
 (*     | _ -> pars *)
 (*   in aux init n c *)
 
-let unfold_head env sigma (ids, csts) c = 
+let is_transparent_constant csts ps c =
+  match Structures.PrimitiveProjections.find_opt c with
+  | None -> Cset.mem c csts
+  | Some p -> PRset.mem p ps
+
+let unfold_head env sigma (ids, csts, ps) c = 
   let rec aux c = 
     match kind sigma c with
     | Var id when Id.Set.mem id ids ->
       (match Environ.named_body id env with
       | Some b -> true, of_constr b
       | None -> false, c)
-    | Const (cst,u) when Cset.mem cst csts ->
+    | Const (cst,u) when is_transparent_constant csts ps cst ->
 	    true, of_constr (Environ.constant_value_in env (cst, EInstance.kind sigma u))
     | App (f, args) ->
       (match aux f with
@@ -552,12 +557,12 @@ open CErrors
 
 let unfold_head env sigma db t =
   let st =
-    List.fold_left (fun (i,c) dbname -> 
+    List.fold_left (fun (i,c,p) dbname -> 
       let db = try Hints.searchtable_map dbname 
         with Not_found -> user_err (str "Unknown database " ++ str dbname)
       in
-      let (ids, csts) = Hints.Hint_db.unfolds db in
-        (Id.Set.union ids i, Cset.union csts c)) (Id.Set.empty, Cset.empty) db
+      let (ids, csts, ps) = Hints.Hint_db.unfolds db in
+        (Id.Set.union ids i, Cset.union csts c, PRset.union ps p)) (Id.Set.empty, Cset.empty, PRset.empty) db
   in
   unfold_head env sigma st t
 
@@ -1028,7 +1033,7 @@ let evar_absorb_arguments = Evardefine.evar_absorb_arguments
 let hintdb_set_transparency cst b db =
   let locality = if Global.sections_are_opened () then Hints.Local else Hints.SuperGlobal in
   Hints.add_hints ~locality [db] 
-    (Hints.HintsTransparencyEntry (Hints.HintsReferences [Tacred.EvalConstRef cst], b))
+    (Hints.HintsTransparencyEntry (Hints.HintsReferences [Evaluable.EvalConstRef cst], b))
 
 (* Call the really unsafe is_global test, we use this on evar-open terms too *)
 let is_global = EConstr.isRefX

src/noconf_hom.ml

@@ -268,7 +268,7 @@ let derive_no_confusion_hom ~pm env sigma0 ~poly (ind,u as indu) =
      * let _fixprots = [s] in *)
     (* let () = Equations.define_principles flags None fixprots [proginfo, compiled_info] in *)
     (* The principles are now shown, let's prove this forms an equivalence *)
-    Global.set_strategy (ConstKey program_cst) Conv_oracle.transparent;
+    Global.set_strategy (Evaluable.EvalConstRef program_cst) Conv_oracle.transparent;
     let env = Global.env () in
     let sigma = Evd.from_env env in
     let sigma, indu = Evd.fresh_global

src/principles.ml

@@ -74,7 +74,7 @@ let inRewRule =
 let add_rew_rule ~l2r ~base ref = Lib.add_leaf (inRewRule (base,ref,l2r))
 
 let cache_opacity cst =
-  Global.set_strategy (ConstKey cst) Conv_oracle.Opaque
+  Global.set_strategy (Evaluable.EvalConstRef cst) Conv_oracle.Opaque
 
 let subst_opacity (subst, cst) =
   let gr' = Mod_subst.subst_constant subst cst in
@@ -617,7 +617,7 @@ let where_instance w =
 let arguments sigma c = snd (decompose_app sigma c)
 
 let unfold_constr sigma c =
-  Tactics.unfold_in_concl [(Locus.OnlyOccurrences [1], Tacred.EvalConstRef (fst (destConst sigma c)))]
+  Tactics.unfold_in_concl [(Locus.OnlyOccurrences [1], Evaluable.EvalConstRef (fst (destConst sigma c)))]
 
 let extend_prob_ctx delta (ctx, pats, ctx') =
   (delta @ ctx, Context_map.lift_pats (List.length delta) pats, ctx')
@@ -1376,10 +1376,10 @@ let declare_funind ~pm info alias env evd is_rec protos progs
     (* If desired the definitions should be made transparent again. *)
     begin
     if !Equations_common.equations_transparent then
-      (Global.set_strategy (ConstKey (fst (destConst evd f))) Conv_oracle.transparent;
+      (Global.set_strategy (Evaluable.EvalConstRef (fst (destConst evd f))) Conv_oracle.transparent;
        match alias with
        | None -> ()
-       | Some ((f, _), _, _) -> Global.set_strategy (ConstKey (fst (destConst evd f))) Conv_oracle.transparent)
+       | Some ((f, _), _, _) -> Global.set_strategy (Evaluable.EvalConstRef (fst (destConst evd f))) Conv_oracle.transparent)
     else
       ((* Otherwise we turn them opaque and let that information be discharged as well *)
         Lib.add_leaf (inOpacity (fst (destConst evd f)));
@@ -1769,16 +1769,16 @@ let build_equations ~pm with_ind env evd ?(alias:alias option) rec_info progs =
           let locality = if Global.sections_are_opened () then Hints.Local else Hints.SuperGlobal in
           (* From now on, we don't need the reduction behavior of the constant anymore *)
           Hints.(add_hints ~locality [info.base_id]
-            (HintsTransparencyEntry (HintsReferences [Tacred.EvalConstRef ocst], false)));
-          Classes.set_typeclass_transparency ~locality [Tacred.EvalConstRef cst] false;
+            (HintsTransparencyEntry (HintsReferences [Evaluable.EvalConstRef ocst], false)));
+          Classes.set_typeclass_transparency ~locality [Evaluable.EvalConstRef cst] false;
           (match alias with
            | Some ((f, _), _, _) ->
               let cst' = fst (destConst !evd f) in
               Hints.(add_hints ~locality [info.base_id]
-                (HintsTransparencyEntry (HintsReferences [Tacred.EvalConstRef cst'], false)));
-              Global.set_strategy (ConstKey cst') Conv_oracle.Opaque
+                (HintsTransparencyEntry (HintsReferences [Evaluable.EvalConstRef cst'], false)));
+              Global.set_strategy (Evaluable.EvalConstRef cst') Conv_oracle.Opaque
            | None -> ());
-          Global.set_strategy (ConstKey cst) Conv_oracle.Opaque;
+          Global.set_strategy (Evaluable.EvalConstRef cst) Conv_oracle.Opaque;
           if with_ind then (declare_ind (); pm) else pm)
         else pm
       in

src/principles_proofs.ml

@@ -277,9 +277,9 @@ let hyps_after sigma env pos args =
 
 let simpl_of csts =
   let opacify () = List.iter (fun (cst,_) ->
-    Global.set_strategy (ConstKey cst) Conv_oracle.Opaque) csts
+    Global.set_strategy (Evaluable.EvalConstRef cst) Conv_oracle.Opaque) csts
   and transp () = List.iter (fun (cst, level) ->
-    Global.set_strategy (ConstKey cst) level) csts
+    Global.set_strategy (Evaluable.EvalConstRef cst) level) csts
   in opacify, transp
 
 let gather_subst env sigma ty args len =
@@ -912,8 +912,8 @@ let solve_rec_eq simpltac subst =
               is_global env sigma (GlobRef.ConstRef f_cst) xf && is_global env sigma (GlobRef.ConstRef funf_cst) yf) subst
         in
         let unfolds = unfold_in_concl
-            [((Locus.OnlyOccurrences [1]), Tacred.EvalConstRef f_cst); 
-              ((Locus.OnlyOccurrences [1]), Tacred.EvalConstRef funf_cst)]
+            [((Locus.OnlyOccurrences [1]), Evaluable.EvalConstRef f_cst); 
+              ((Locus.OnlyOccurrences [1]), Evaluable.EvalConstRef funf_cst)]
         in tclTHENLIST [unfolds; simpltac; pi_tac ()]
       with Not_found -> tclORELSE reflexivity (congruence_tac 10 []))
   | _ -> reflexivity
@@ -1130,13 +1130,13 @@ let prove_unfolding_lemma_aux info where_map my_simpl subst p unfp =
     let unfolds =
       tclTHENLIST
         [unfold_in_concl
-                  [Locus.OnlyOccurrences [1], Tacred.EvalConstRef f_cst;
-                  (Locus.OnlyOccurrences [1], Tacred.EvalConstRef funf_cst)];
+                  [Locus.OnlyOccurrences [1], Evaluable.EvalConstRef f_cst;
+                  (Locus.OnlyOccurrences [1], Evaluable.EvalConstRef funf_cst)];
           my_simpl]
     in
     let set_opaque () =
-      Global.set_strategy (ConstKey f_cst) Conv_oracle.Opaque;
-      Global.set_strategy (ConstKey funf_cst) Conv_oracle.Opaque;
+      Global.set_strategy (Evaluable.EvalConstRef f_cst) Conv_oracle.Opaque;
+      Global.set_strategy (Evaluable.EvalConstRef funf_cst) Conv_oracle.Opaque;
     in
     let kind = get_program_reckind env sigma where_map p in
     let subst, fixtac, extgl = match kind with

src/splitting.ml

@@ -1229,7 +1229,7 @@ let simplify_evars evars t =
     | _ -> EConstr.map evars aux t
   in aux t
 
-let unfold_entry cst = Hints.HintsUnfoldEntry [Tacred.EvalConstRef cst]
+let unfold_entry cst = Hints.HintsUnfoldEntry [Evaluable.EvalConstRef cst]
 let add_hint local i cst =
   let locality = if local || Global.sections_are_opened () then Hints.Local else Hints.SuperGlobal in
   Hints.add_hints ~locality [Id.to_string i] (unfold_entry cst)

src/subterm.ml

@@ -239,7 +239,7 @@ let derive_subterm ~pm env sigma ~poly (ind, u as indu) =
         (* Impargs.declare_manual_implicits false (ConstRef cst) ~enriching:false *)
         (* 	(list_map_i (fun i _ -> ExplByPos (i, None), (true, true, true)) 1 parambinders); *)
         Hints.add_hints ~locality [subterm_relation_base]
-                        (Hints.HintsUnfoldEntry [Tacred.EvalConstRef kn]);
+                        (Hints.HintsUnfoldEntry [Evaluable.EvalConstRef kn]);
         mkApp (cst, extended_rel_vect 0 parambinders)
       in
       let env' = push_rel_context pars env in