diff options
author | 2008-07-25 15:12:53 +0200 | |
---|---|---|
committer | 2008-07-25 15:12:53 +0200 | |
commit | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch) | |
tree | dabcac548e299fee1da464c93b3dba98484f45b1 /pretyping/reductionops.mli | |
parent | 2281410e38ef99d025ea77194585a9bc019fdaa9 (diff) |
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
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 |