diff options
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 1e9b3b5b..d48055cf 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: reductionops.mli 9106 2006-09-01 11:18:17Z herbelin $ i*) +(*i $Id: reductionops.mli 11010 2008-05-28 15:25:19Z barras $ i*) (*i*) open Names @@ -181,7 +181,8 @@ val is_arity : env -> evar_map -> constr -> bool val whd_programs : reduction_function -(* [reduce_fix] contracts a fix redex if it is actually reducible *) +(* [reduce_fix redfun fix stk] contracts [fix stk] if it is actually + reducible; the structural argument is reduced by [redfun] *) type fix_reduction_result = NotReducible | Reduced of state @@ -189,6 +190,9 @@ val fix_recarg : fixpoint -> constr stack -> (int * constr) option val reduce_fix : local_state_reduction_function -> fixpoint -> constr stack -> fix_reduction_result +(*s Querying the kernel conversion oracle: opaque/transparent constants *) +val is_transparent : 'a tableKey -> bool + (*s Conversion Functions (uses closures, lazy strategy) *) type conversion_test = constraints -> constraints @@ -197,12 +201,15 @@ val pb_is_equal : conv_pb -> bool val pb_equal : conv_pb -> conv_pb val sort_cmp : conv_pb -> sorts -> sorts -> conversion_test -val base_sort_cmp : conv_pb -> sorts -> sorts -> bool val is_conv : env -> evar_map -> constr -> constr -> bool val is_conv_leq : env -> evar_map -> constr -> constr -> bool val is_fconv : conv_pb -> env -> evar_map -> constr -> constr -> bool +val is_trans_conv : transparent_state -> env -> evar_map -> constr -> constr -> bool +val is_trans_conv_leq : transparent_state -> env -> evar_map -> constr -> constr -> bool +val is_trans_fconv : conv_pb -> transparent_state -> env -> evar_map -> constr -> constr -> bool + (*s Special-Purpose Reduction Functions *) val whd_meta : (metavariable * constr) list -> constr -> constr @@ -211,8 +218,9 @@ val instance : (metavariable * constr) list -> constr -> constr (*s Heuristic for Conversion with Evar *) -val apprec : state_reduction_function +val whd_betaiota_deltazeta_for_iota_state : state_reduction_function (*s Meta-related reduction functions *) val meta_instance : evar_defs -> constr freelisted -> constr val nf_meta : evar_defs -> constr -> constr +val meta_reducible_instance : evar_defs -> constr freelisted -> constr |