diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-08-28 09:15:53 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-08-28 09:15:53 +0000 |
| commit | afebe632272441db15ec0958825112e4558f7a85 (patch) | |
| tree | 8139aecf169bad99777cf55bde73b823987b9d00 /pretyping/reductionops.mli | |
| parent | 6f7801f1a40e6f2ad593eb9cdad01e118b10018f (diff) | |
Ajout whd_eta + export append_stack_list + petit nettoyage (dont maj de
certains commentaires historiques, traçables jusqu'à la version 4.1,
mais devenus hors à propos suite aux nombreuses modifications du code).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9087 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 7e27765e4..0ac1fe118 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -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 @@ -206,11 +208,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 *) |