diff options
| author | herbelin | 2000-03-21 00:05:25 +0000 |
|---|---|---|
| committer | herbelin | 2000-03-21 00:05:25 +0000 |
| commit | 90be03bb4be9e7699209e380297d1ac49f4a6c19 (patch) | |
| tree | 5db75002d761145b38f1eace6160c130b4fcec19 /kernel/reduction.mli | |
| parent | 47b64cb48e83b16103dd8505490fb3dba60aa6ff (diff) | |
Plus besoin de env dans reduce_mind_case; make_arity et make_constructor sortent de inductive_summary et se renomment en get_arity et get_constructors
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@339 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index b953907db8..583a7cf1ff 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -90,8 +90,9 @@ val hnf_lam_appvect : env -> 'a evar_map -> string -> constr -> constr array -> constr val hnf_lam_applist : env -> 'a evar_map -> string -> constr -> constr list -> constr -val splay_prod : - env -> 'a evar_map -> constr -> (name * constr) list * constr +val splay_prod : env -> 'a evar_map -> constr -> (name * constr) list * constr +val splay_arity : env -> 'a evar_map -> constr -> (name * constr) list * sorts +val sort_of_arity : env -> constr -> sorts val decomp_prod : env -> 'a evar_map -> constr -> int * constr val decomp_n_prod : env -> 'a evar_map -> int -> constr -> ((name * constr) list) * constr @@ -104,7 +105,7 @@ type 'a miota_args = { mlf : 'a array } (* the branch code vector *) val reducible_mind_case : constr -> bool -val reduce_mind_case : env -> constr miota_args -> constr +val reduce_mind_case : constr miota_args -> constr val is_arity : env -> 'a evar_map -> constr -> bool val is_info_arity : env -> 'a evar_map -> constr -> bool @@ -179,7 +180,7 @@ val is_fconv : conv_pb -> env -> 'a evar_map -> constr -> constr -> bool val whd_meta : (int * constr) list -> constr -> constr val plain_instance : (int * constr) list -> constr -> constr -val instance : (int * constr) list -> 'a reduction_function +val instance : (int * constr) list -> constr -> constr (* [whd_ise] raise [Uninstantiated_evar] if an evar remains uninstantiated; *) (* *[whd_ise1]* is synonymous of *[whd_evar empty_env]* and *[nf_ise1]* of *) @@ -211,6 +212,11 @@ val find_mcoinductype : env -> 'a evar_map -> constr -> inductive * constr list (* [try_mutind_of env sigma t] raises [Induc] if [t] is not an inductive type*) (* The resulting summary is relative to the current env *) -val try_mutind_of : env -> 'a evar_map -> constr -> Inductive.inductive_summary +open Inductive +val try_mutind_of : env -> 'a evar_map -> constr -> inductive_summary +val get_constructors : env -> 'a evar_map -> inductive_summary + -> constructor_summary array +val get_arity : env -> 'a evar_map -> inductive_summary -> + (name * constr) list * sorts |