diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-01 13:50:11 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-01 13:50:11 +0000 |
| commit | f62385a60b4d4f20a95891b6044c7bc9135b5915 (patch) | |
| tree | 8a76f624d288063a39102abc136da3e6e74d3b6d /kernel | |
| parent | 2b0ec396211db0487cb836729a3d91bf94de5baf (diff) | |
Code comateux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@628 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/reduction.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index ad1ac931e..84b5b7a07 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -103,6 +103,7 @@ let rec whd_state (x, stack as s) = | _ -> s let whd_stack x = appterm_of_stack (whd_state (x, empty_stack)) +let whd_castapp_stack = whd_stack let stack_reduction_of_reduction red_fun env sigma s = let t = red_fun env sigma (app_stack s) in @@ -1186,7 +1187,7 @@ let rec whd_ise1 sigma c = whd_ise1 sigma (existential_value sigma (ev,args)) | IsCast (c,_) -> whd_ise1 sigma c (* A quoi servait cette ligne ??? - | DOP0(Sort(Type _)) -> DOP0(Sort(Type dummy_univ)) + | IsSort (Type _) -> mkSort (Type dummy_univ) *) | _ -> c |