diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-23 08:25:31 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-23 08:25:31 +0000 |
| commit | 8fc99285ff74272185c53859b1ba21279deb624b (patch) | |
| tree | 54fd783e6da4a99f2e65876919c7d22ec3978e75 | |
| parent | 4dc2b671aad3fd491c0587dcf49aa08b6c55a409 (diff) | |
Simplifications/questions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@737 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | kernel/reduction.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 539426bc3..d27935187 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -889,8 +889,6 @@ and eqappr cv_pb infos appr1 appr2 = let fconv cv_pb env sigma t1 t2 = - let t1 = local_strong strip_outer_cast t1 - and t2 = local_strong strip_outer_cast t2 in if eq_constr t1 t2 then Constraint.empty else @@ -1154,7 +1152,7 @@ let rec whd_ise sigma c = whd_ise sigma (existential_value sigma (ev,args)) else raise (Uninstantiated_evar ev) | IsCast (c,_) -> whd_ise sigma c - | IsSort (Type _) -> mkSort (Type dummy_univ) +(* | IsSort (Type _) -> mkSort (Type dummy_univ)*) | _ -> c |