diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-24 09:15:57 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-24 09:15:57 +0000 |
| commit | 5fb9b0b82547eac276b5fb5d64a63396b557e3bc (patch) | |
| tree | 338e057f11321a00283aa68beece4173642b3b11 /kernel/closure.mli | |
| parent | ad7bec4eacfc3255f7270feab55eca407ac8766c (diff) | |
Bug réduction suite modifs let-in
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@750 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/closure.mli')
| -rw-r--r-- | kernel/closure.mli | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/kernel/closure.mli b/kernel/closure.mli index e2345fdf5..183afe253 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -137,7 +137,7 @@ and frterm = | FRel of int | FAtom of constr | FCast of freeze * freeze - | FFlex of frreference * freeze array + | FFlex of frreference | FInd of inductive_path * freeze array | FConstruct of constructor_path * freeze array | FApp of freeze * freeze array @@ -153,8 +153,8 @@ and frterm = | FFROZEN of constr * freeze subs and frreference = - | FConst of section_path - | FEvar of existential_key + | FConst of constant + | FEvar of (existential * freeze subs) | FVar of identifier | FFarRel of int @@ -213,8 +213,7 @@ val whd_val : 'a clos_infos -> fconstr -> constr val fhnf: 'a clos_infos -> fconstr -> int * fconstr * fconstr array val fhnf_apply : 'a clos_infos -> int -> fconstr -> fconstr array -> int * fconstr * fconstr array -val search_frozen_value : - 'a clos_infos -> frreference -> fconstr array -> fconstr option +val search_frozen_value : 'a clos_infos -> frreference -> fconstr option (* recursive functions... *) val unfreeze : 'a clos_infos -> fconstr -> fconstr |