diff options
| author | letouzey | 2010-06-17 18:51:23 +0000 |
|---|---|---|
| committer | letouzey | 2010-06-17 18:51:23 +0000 |
| commit | 405885980b4a7a7eeb8d26cd5a7ad0f132ac6388 (patch) | |
| tree | b7eac1082c65ff1c528adfb21656bf042c7c9eca /kernel/cbytecodes.ml | |
| parent | 195dc9ae3928a62e58977d8a2582660951d17b9c (diff) | |
fsetdec: clear dependent hypothesis before anything else (fix #2136).
Since the tactic fsetdec is doing lots of "clear" and also "subst"
on equalities, things may go wrong in case of dependencies amongst
hypothesis. For the moment, we clear all hypothesis that mention
other hypothesis of sort Prop.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13162 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions