Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)
(** Delta implies all consts (both global (= by [kernel_name]) and local (= by [Rel] or [Var])), all evars, and letin's. Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of a LetIn expression is Letin reduction *)
(** Set of reduction kinds. *)type reds
(** Reduction kind. *)type red_kind
val fBETA : red_kindval fDELTA : red_kindval fMATCH : red_kindval fFIX : red_kindval fCOFIX : red_kindval fZETA : red_kindval fCONST : Names.Constant.t -> red_kindval fPROJ : Names.Projection.Repr.t -> red_kindval fVAR : Names.Id.t -> red_kind
(** No reduction at all *)val no_red : reds
(** Adds a reduction kind to a set *)val red_add : reds -> red_kind -> reds
(** Removes a reduction kind from a set *)val red_sub : reds -> red_kind -> reds
(** Adds a list of reduction kind to a set *)val red_add_list : reds -> red_kind list -> reds
(** Removes a list of reduction kind from a set *)val red_sub_list : reds -> red_kind list -> reds
(** Adds a reduction kind to a set *)val red_add_transparent : reds -> TransparentState.t -> reds
(** Retrieve the transparent state of the reduction flags *)val red_transparent : reds -> TransparentState.t
(** Build a reduction set from scratch = iter [red_add] on [no_red] *)val mkflags : red_kind list -> reds
(** Tests if a reduction kind is set *)val red_set : reds -> red_kind -> bool
(** This tests if the projection is in unfolded state already or is unfodable due to delta. *)val red_projection : reds -> Names.Projection.t -> bool
(* These flags do not contain eta *)val all : redsval allnolet : redsval beta : redsval betadeltazeta : redsval betaiota : redsval betaiotazeta : redsval betazeta : redsval delta : redsval zeta : redsval nored : reds