From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 pretyping/reductionops.mli | 27 +++++++++++++++------------
 1 file changed, 15 insertions(+), 12 deletions(-)

(limited to 'pretyping/reductionops.mli')

diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index b8ac085a..c0ff6723 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -25,10 +25,10 @@ module ReductionBehaviour : sig
 
 (** [set is_local ref (recargs, nargs, flags)] *)
   val set :
-    bool -> Globnames.global_reference -> (int list * int * flag list) -> unit
+    bool -> GlobRef.t -> (int list * int * flag list) -> unit
   val get :
-    Globnames.global_reference -> (int list * int * flag list) option
-  val print : Globnames.global_reference -> Pp.t
+    GlobRef.t -> (int list * int * flag list) option
+  val print : GlobRef.t -> Pp.t
 end
 
 (** {6 Support for reduction effects } *)
@@ -41,10 +41,10 @@ val declare_reduction_effect : effect_name ->
   (Environ.env -> Evd.evar_map -> Constr.constr -> unit) -> unit
 
 (* [set_reduction_effect cst name] declares effect [name] to be called when [cst] is found *)
-val set_reduction_effect : Globnames.global_reference -> effect_name -> unit
+val set_reduction_effect : Constant.t -> effect_name -> unit
 
 (* [effect_hook env sigma key term] apply effect associated to [key] on [term] *)
-val reduction_effect_hook : Environ.env -> Evd.evar_map -> Constr.constr ->
+val reduction_effect_hook : Environ.env -> Evd.evar_map -> Constant.t ->
   Constr.constr Lazy.t -> unit
 
 (** {6 Machinery about a stack of unfolded constant }
@@ -60,7 +60,7 @@ module Cst_stack : sig
   val best_cst : t -> (constr * constr list) option
   val best_replace : Evd.evar_map -> constr -> t -> constr -> constr
   val reference : Evd.evar_map -> t -> Constant.t option
-  val pr : t -> Pp.t
+  val pr : env -> Evd.evar_map -> t -> Pp.t
 end
 
 module Stack : sig
@@ -75,7 +75,7 @@ module Stack : sig
   type 'a member =
   | App of 'a app_node
   | Case of case_info * 'a * 'a array * Cst_stack.t
-  | Proj of int * int * Projection.t * Cst_stack.t
+  | Proj of Projection.t * Cst_stack.t
   | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
   | Cst of cst_member * int (** current foccussed arg *) * int list (** remaining args *)
     * 'a t * Cst_stack.t
@@ -140,10 +140,13 @@ type contextual_state_reduction_function =
 type state_reduction_function = contextual_state_reduction_function
 type local_state_reduction_function = evar_map -> state -> state
 
-val pr_state : state -> Pp.t
+val pr_state : env -> evar_map -> state -> Pp.t
 
 (** {6 Reduction Function Operators } *)
 
+val strong_with_flags :
+  (CClosure.RedFlags.reds -> reduction_function) ->
+  (CClosure.RedFlags.reds -> reduction_function)
 val strong : reduction_function -> reduction_function
 val local_strong : local_reduction_function -> local_reduction_function
 val strong_prodspine : local_reduction_function -> local_reduction_function
@@ -277,13 +280,13 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env ->  evar_map -> con
     otherwise returns false in that case.
  *)
 val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> 
-  env -> evar_map -> constr -> constr -> evar_map * bool
+  env -> evar_map -> constr -> constr -> evar_map option
 
 (** Conversion with inference of universe constraints *)
 val set_vm_infer_conv : (?pb:conv_pb -> env -> evar_map -> constr -> constr ->
-  evar_map * bool) -> unit
+  evar_map option) -> unit
 val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr ->
-  evar_map * bool
+  evar_map option
 
 
 (** [infer_conv_gen] behaves like [infer_conv] but is parametrized by a
@@ -291,7 +294,7 @@ conversion function. Used to pretype vm and native casts. *)
 val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> transparent_state ->
     (Constr.constr, evar_map) Reduction.generic_conversion_function) ->
   ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> env ->
-  evar_map -> constr -> constr -> evar_map * bool
+  evar_map -> constr -> constr -> evar_map option
 
 (** {6 Special-Purpose Reduction Functions } *)
 
-- 
cgit v1.2.3