diff options
| author | msozeau | 2008-02-10 14:10:38 +0000 |
|---|---|---|
| committer | msozeau | 2008-02-10 14:10:38 +0000 |
| commit | ee90aac584d123fa709d6629d99057b62bb343d0 (patch) | |
| tree | 242267d42f56a952af775f1eb04d94378d171836 /dev | |
| parent | 952d9ebd44fe6bd052c81c583e3a74752b53f932 (diff) | |
Backport Program Instance into Instance. Proper early error message if
trying to declare an instance with an already existing name. Add
possibility of not giving all the fields in Instance declarations, using
Refine.refine to generate the subgoals. No control over opacity in this
case though...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10548 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions