diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-03-23 15:04:09 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-03-23 15:04:09 +0000 |
| commit | fae106f740d3d71555933cf416eec905c58f417e (patch) | |
| tree | 12cfd6fa08b20e9f076c113a1a668388c5cf5527 /kernel/reduction.mli | |
| parent | fab1cc89b9ff65938cff3b4e41e51ad3b0bc68db (diff) | |
amelioration de la consommation memoire de la conversion en eta-expansant
les definitions.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1483 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 19 |
1 files changed, 5 insertions, 14 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 20435a1fc..a47b19242 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -151,31 +151,23 @@ val reduce_fix : local_state_reduction_function -> fixpoint (*s Conversion Functions (uses closures, lazy strategy) *) +type conversion_test = constraints -> constraints + +exception NotConvertible + type conv_pb = | CONV - | CONV_LEQ + | CUMUL val pb_is_equal : conv_pb -> bool val pb_equal : conv_pb -> conv_pb -type conversion_test = constraints -> constraints - -exception NotConvertible - val sort_cmp : conv_pb -> sorts -> sorts -> conversion_test val base_sort_cmp : conv_pb -> sorts -> sorts -> bool -val bool_and_convert : bool -> conversion_test -> conversion_test -val convert_and : conversion_test -> conversion_test -> conversion_test -val convert_or : conversion_test -> conversion_test -> conversion_test -val convert_forall2 : - ('a -> 'b -> conversion_test) -> 'a array -> 'b array -> conversion_test - type 'a conversion_function = env -> 'a evar_map -> constr -> constr -> constraints -val fconv : conv_pb -> 'a conversion_function - (* [fconv] has 2 instances: [conv = fconv CONV] i.e. conversion test, and [conv_leq = fconv CONV_LEQ] i.e. cumulativity test. *) @@ -194,7 +186,6 @@ val is_conv : env -> 'a evar_map -> constr -> constr -> bool val is_conv_leq : env -> 'a evar_map -> constr -> constr -> bool val is_fconv : conv_pb -> env -> 'a evar_map -> constr -> constr -> bool - (*s Special-Purpose Reduction Functions *) val whd_meta : (int * constr) list -> constr -> constr |