diff options
| author | Enrico Tassi | 2019-05-10 18:01:33 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-05-10 18:01:33 +0200 |
| commit | 2f2658c5a318fb8a8c00caf4d1aca9fbc2d060d0 (patch) | |
| tree | 727bac3aa0301562ecdec323d0a2de6a7dcdf39c /pretyping/reductionops.mli | |
| parent | 482995d1741be47f6c296276aeb4322443c5b3f4 (diff) | |
| parent | 857082b492760c17bfbc2b2022862c7cd758261e (diff) | |
Merge PR #10058: Remove various circumvolutions from reduction behaviors
Ack-by: SkySkimmer
Reviewed-by: gares
Ack-by: maximedenes
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index b5d3ff7627..aa39921ea2 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -21,13 +21,12 @@ exception Elimconst (** Machinery to customize the behavior of the reduction *) module ReductionBehaviour : sig - type flag = [ `ReductionDontExposeCase | `ReductionNeverUnfold ] -(** [set is_local ref (recargs, nargs, flags)] *) - val set : - bool -> GlobRef.t -> (int list * int * flag list) -> unit - val get : - GlobRef.t -> (int list * int * flag list) option + type t = NeverUnfold | UnfoldWhen of when_flags | UnfoldWhenNoMatch of when_flags + and when_flags = { recargs : int list ; nargs : int option } + + val set : local:bool -> GlobRef.t -> t -> unit + val get : GlobRef.t -> t option val print : GlobRef.t -> Pp.t end |