Having added a special Cast for remembering the use of conversion

tactic steps (r14407) increased the size of proof-terms, leading in
some cases (e.g. in Nijmegen/Algebra) to calls to simpl becoming
extremely costly on such terms built with tactics.

We try as a workaround to remove the newly introduced Cast after it
has been used by the type-checking algorithm.

We incidentally fixed eq_constr which was not fully transparent wrt
casts. We also removed useless code in judge_of_apply (has_revert).

Note: checker still to be updated to reflect a possible use of this
new kind of cast.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14448 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions