diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-12 16:08:04 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-12 16:08:04 +0000 |
| commit | 63ffd17f771d0f4c8c7f9b1ada9faa04253f05aa (patch) | |
| tree | ff43de2111efb4a9b9db28e137130b4d7854ec69 /tactics/eauto.ml4 | |
| parent | 1ea4a8d26516af14670cc677a5a0fce04b90caf7 (diff) | |
Add the ability to specify what to do with free variables in instance
declarations. By default, print the list of implicitely generalized
variables. Implement new commands Add Parametric Relation/Morphism for...
parametric relations and morphisms. Now the Add * commands are strict
about free vars and will fail if there remain some. Parametric just allows to
give a variable context. Also, correct a bug in generalization of
implicits that ordered the variables in the wrong order.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10782 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/eauto.ml4')
0 files changed, 0 insertions, 0 deletions