diff options
| author | notin | 2007-04-26 14:42:38 +0000 |
|---|---|---|
| committer | notin | 2007-04-26 14:42:38 +0000 |
| commit | c900915e6e7100c9b6802d2e5641e67fa3f7ecb0 (patch) | |
| tree | b199615fb26b670de06543fb560f844f8604ce19 /dev | |
| parent | ea1eaa9b152b73652f417e02bd469e5b289cec47 (diff) | |
Petite modif dans instantiate_pf_com: ajout de test pour l'indice 0, et uniformisation des messages d'erreur wrt instantiate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9798 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions