Adapt to rocq-prover/rocq#21669 (evaluable_of_global_reference no env arg)

Author: SkySkimmer

template-rocq/src/plugin_core.ml

@@ -21,10 +21,10 @@ let rs_lazy = Genredexpr.Cbv Redops.all_flags
 let rs_unfold (env : Environ.env) (gr : global_reference) =
   try
     Genredexpr.Unfold [Locus.AllOccurrences,
-                       Tacred.evaluable_of_global_reference env gr]
+                       Tacred.evaluable_of_global_reference gr]
   with
-  | _ -> CErrors.user_err
-           Pp.(str "Constant not found or not a constant: " ++ Printer.pr_global gr)
+  | Tacred.NotEvaluableRef _ -> CErrors.user_err
+           Pp.(str "Not a constant: " ++ Printer.pr_global gr ++ str ".")
 
 (* Rocq state related to vernaculars, needed to declare constants,
    could be a good idea to add the evar_map / env here as a record *)

template-rocq/src/run_template_monad.ml

@@ -30,7 +30,7 @@ let unquote_reduction_strategy env evm trm (* of type reductionStrategy *) : Red
     | name (* to unfold *) :: _ ->
        let name = reduce_all env evm name in
        let name = unquote_kn name in
-       Unfold [Locus.AllOccurrences, Tacred.evaluable_of_global_reference env (GlobRef.ConstRef (Constant.make1 name))]
+       Unfold [Locus.AllOccurrences, Tacred.evaluable_of_global_reference (GlobRef.ConstRef (Constant.make1 name))]
     | _ -> bad_term_verb trm "unquote_reduction_strategy"
   else not_supported_verb trm "unquote_reduction_strategy"