Merge pull request #582 from rlepigre/br/evaluable_refactoring

Adapt to coq/coq#18546.
mattam82 · Apr 3, 2024 · 0f75fa9 · 0f75fa9
2 parents 962c005 + a2273ac
commit 0f75fa9
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 11 deletions.
diff --git a/src/equations.ml b/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 (Evaluable.EvalConstRef funf_cst) Conv_oracle.transparent;
+    Global.set_strategy (Conv_oracle.EvalConstRef funf_cst) Conv_oracle.transparent;
     let () = (* Declare the subproofs of unfolding for where as rewrite rules *)
       let decl _ (_, id, _) =
         let gr =

diff --git a/src/noconf_hom.ml b/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 (Evaluable.EvalConstRef program_cst) Conv_oracle.transparent;
+    Global.set_strategy (Conv_oracle.EvalConstRef program_cst) Conv_oracle.transparent;
     let env = Global.env () in
     let sigma = Evd.from_env env in
     let sigma, indu = Evd.fresh_global

diff --git a/src/principles.ml b/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 (Evaluable.EvalConstRef cst) Conv_oracle.Opaque
+  Global.set_strategy (Conv_oracle.EvalConstRef cst) Conv_oracle.Opaque
 
 let subst_opacity (subst, cst) =
   let gr' = Mod_subst.subst_constant subst cst in
@@ -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 (Evaluable.EvalConstRef (fst (destConst evd f))) Conv_oracle.transparent;
+      (Global.set_strategy (Conv_oracle.EvalConstRef (fst (destConst evd f))) Conv_oracle.transparent;
        match alias with
        | None -> ()
-       | Some ((f, _), _, _) -> Global.set_strategy (Evaluable.EvalConstRef (fst (destConst evd f))) Conv_oracle.transparent)
+       | Some ((f, _), _, _) -> Global.set_strategy (Conv_oracle.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)));
@@ -1776,9 +1776,9 @@ let build_equations ~pm with_ind env evd ?(alias:alias option) rec_info progs =
               let cst' = fst (destConst !evd f) in
               Hints.(add_hints ~locality [info.base_id]
                 (HintsTransparencyEntry (HintsReferences [Evaluable.EvalConstRef cst'], false)));
-              Global.set_strategy (Evaluable.EvalConstRef cst') Conv_oracle.Opaque
+              Global.set_strategy (Conv_oracle.EvalConstRef cst') Conv_oracle.Opaque
            | None -> ());
-          Global.set_strategy (Evaluable.EvalConstRef cst) Conv_oracle.Opaque;
+          Global.set_strategy (Conv_oracle.EvalConstRef cst) Conv_oracle.Opaque;
           if with_ind then (declare_ind (); pm) else pm)
         else pm
       in

diff --git a/src/principles_proofs.ml b/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 (Evaluable.EvalConstRef cst) Conv_oracle.Opaque) csts
+    Global.set_strategy (Conv_oracle.EvalConstRef cst) Conv_oracle.Opaque) csts
   and transp () = List.iter (fun (cst, level) ->
-    Global.set_strategy (Evaluable.EvalConstRef cst) level) csts
+    Global.set_strategy (Conv_oracle.EvalConstRef cst) level) csts
   in opacify, transp
 
 let gather_subst env sigma ty args len =
@@ -1135,8 +1135,8 @@ let prove_unfolding_lemma_aux info where_map my_simpl subst p unfp =
           my_simpl]
     in
     let set_opaque () =
-      Global.set_strategy (Evaluable.EvalConstRef f_cst) Conv_oracle.Opaque;
-      Global.set_strategy (Evaluable.EvalConstRef funf_cst) Conv_oracle.Opaque;
+      Global.set_strategy (Conv_oracle.EvalConstRef f_cst) Conv_oracle.Opaque;
+      Global.set_strategy (Conv_oracle.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