diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
| commit | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
| tree | 591e9e512063e34099782e2518573f15ffeac003 /pretyping/reductionops.mli | |
| parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) | |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 78afd22b..1e9b3b5b 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 8812 2006-05-13 11:46:02Z herbelin $ i*) +(*i $Id: reductionops.mli 9106 2006-09-01 11:18:17Z herbelin $ i*) (*i*) open Names @@ -37,6 +37,7 @@ and 'a stack = 'a stack_member list val empty_stack : 'a stack val append_stack : 'a array -> 'a stack -> 'a stack +val append_stack_list : 'a list -> 'a stack -> 'a stack val decomp_stack : 'a stack -> ('a * 'a stack) option val list_of_stack : 'a stack -> 'a list @@ -140,6 +141,7 @@ val whd_betadeltaiotaeta_stack : stack_reduction_function val whd_betadeltaiotaeta_state : state_reduction_function val whd_betadeltaiotaeta : reduction_function +val whd_eta : constr -> constr @@ -162,6 +164,7 @@ val decomp_n_prod : val splay_prod_assum : env -> evar_map -> constr -> Sign.rel_context * constr val decomp_sort : env -> evar_map -> types -> sorts +val is_sort : env -> evar_map -> types -> bool type 'a miota_args = { mP : constr; (* the result type *) @@ -206,11 +209,8 @@ val whd_meta : (metavariable * constr) list -> constr -> constr val plain_instance : (metavariable * constr) list -> constr -> constr val instance : (metavariable * constr) list -> constr -> constr -(*s Obsolete Reduction Functions *) +(*s Heuristic for Conversion with Evar *) -(*i -val hnf : env -> 'a evar_map -> constr -> constr * constr list -i*) val apprec : state_reduction_function (*s Meta-related reduction functions *) |