Rename soft_evaluable_of_global_reference -> evaluable_of_global_reference

Author: SkySkimmer

dev/ci/user-overlays/21669-SkySkimmer-eval-ref.sh

@@ -0,0 +1,3 @@
+overlay metarocq https://github.com/SkySkimmer/metarocq eval-ref 21669
+
+overlay rewriter https://github.com/SkySkimmer/rewriter eval-ref 21669

plugins/ltac/tacintern.ml

@@ -305,7 +305,7 @@ let evalref_of_globref ?loc r =
     in
     if not is_proof_variable then Dumpglob.add_glob ?loc r
   in
-  Tacred.soft_evaluable_of_global_reference ?loc r
+  Tacred.evaluable_of_global_reference ?loc r
 
 let intern_smart_global ist = function
   | {v=AN r} -> intern_global_reference ist r

pretyping/tacred.ml

@@ -84,7 +84,7 @@ let value_of_evaluable_ref env sigma evref u =
   | Evaluable.EvalProjectionRef _ ->
     assert false (* TODO *)
 
-let soft_evaluable_of_global_reference ?loc = function
+let evaluable_of_global_reference ?loc = function
   | GlobRef.ConstRef cst ->
     begin
       match Structures.PrimitiveProjections.find_opt cst with
@@ -94,6 +94,8 @@ let soft_evaluable_of_global_reference ?loc = function
   | GlobRef.VarRef id -> Evaluable.EvalVarRef id
   | r -> error_not_evaluable ?loc r
 
+let soft_evaluable_of_global_reference = evaluable_of_global_reference
+
 let global_of_evaluable_reference = function
   | Evaluable.EvalConstRef cst -> GlobRef.ConstRef cst
   | Evaluable.EvalVarRef id -> GlobRef.VarRef id

pretyping/tacred.mli

@@ -42,10 +42,14 @@ val is_evaluable : Environ.env -> Evd.evar_map -> Evaluable.t -> bool
 exception NotEvaluableRef of GlobRef.t
 val error_not_evaluable : ?loc:Loc.t -> GlobRef.t -> 'a
 
-val soft_evaluable_of_global_reference :
+val evaluable_of_global_reference :
   ?loc:Loc.t -> GlobRef.t -> Evaluable.t
 (** Succeeds for any constant or variable even if marked opaque or otherwise not evaluable. *)
 
+val soft_evaluable_of_global_reference :
+  ?loc:Loc.t -> GlobRef.t -> Evaluable.t
+[@@deprecated "(9.3) Use evaluable_of_global_reference."]
+
 val global_of_evaluable_reference :
   Evaluable.t -> GlobRef.t
 

tactics/redexpr.ml

@@ -478,7 +478,7 @@ module Intern = struct
       in
       if not is_proof_variable then Dumpglob.add_glob ?loc r
     in
-    Tacred.soft_evaluable_of_global_reference ?loc r
+    Tacred.evaluable_of_global_reference ?loc r
 
   type ('constr,'ref,'pat) intern_env = {
     strict_check : bool;

vernac/classes.ml

@@ -40,7 +40,7 @@ let set_typeclass_transparency ?typeclasses_db ~locality c b =
 
 let set_typeclass_transparency_com ~locality refs b =
   let refs = List.map
-      (fun x -> Tacred.soft_evaluable_of_global_reference
+      (fun x -> Tacred.evaluable_of_global_reference
           (Smartlocate.global_with_alias x))
       refs
   in

vernac/comHints.ml

@@ -64,11 +64,6 @@ let project_hint ~poly pri l2r r =
   let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
   (info, true, GlobRef.ConstRef c)
 
-(* Only error when we have to (axioms may be instantiated if from functors)
-   XXX maybe error if not from a functor argument?
- *)
-let soft_evaluable = Tacred.soft_evaluable_of_global_reference
-
 (* Slightly more lenient global hint syntax for backwards compatibility *)
 let rectify_hint_constr h = match h with
 | Vernacexpr.HintsReference qid -> Some qid
@@ -86,7 +81,7 @@ let interp_hints ~poly h =
     Dumpglob.add_glob ?loc:r.CAst.loc gr;
     gr
   in
-  let fr r = soft_evaluable ?loc:r.CAst.loc (fref r) in
+  let fr r = Tacred.evaluable_of_global_reference ?loc:r.CAst.loc (fref r) in
   let fi c =
     match rectify_hint_constr c with
     | Some c ->