diff options
| author | sacerdot | 2004-09-13 19:50:25 +0000 |
|---|---|---|
| committer | sacerdot | 2004-09-13 19:50:25 +0000 |
| commit | 6b1a9a221bf4ab70671da11c100a8281bde02b20 (patch) | |
| tree | 5e9b6a7d2a0e838bd36c98089d52f12e240bc8c0 /pretyping/pretype_errors.ml | |
| parent | 87ddee89d52f3c8e0bd10f09e45396e2fec62550 (diff) | |
* The ML tactic is now also aware of rewriting directions.
* Code clean-up.
* Preparation for the last implementation phase.
The last implementation phase will consist in the algorithm that, performing
backtracking, chooses the right combination of morphisms in the syntactic
representation of the goal.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6103 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/pretype_errors.ml')
0 files changed, 0 insertions, 0 deletions