diff options
| author | herbelin | 2006-04-26 22:23:37 +0000 |
|---|---|---|
| committer | herbelin | 2006-04-26 22:23:37 +0000 |
| commit | 519804c3de605b6da3c5973cf2061a01d1102270 (patch) | |
| tree | b4510f3e1a4f1c1158995ba2c85d6181434dc067 /tactics | |
| parent | 328be738c63b10638c8826922dd8f28c59b35fe9 (diff) | |
Diverses corrections de l'afficheur et du traducteur pour s'assurer de
la réversibilité de la traduction (correction enregistrement des
retours chariot dans le lexeur, correction affichage espace superflu
en tête des VERNAC EXTEND, correction affichage morphism_signature
dans extraargs.ml4, correction affichage clear dans pptactic.ml)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8739 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/extraargs.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 6017115c46..665a7bd752 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -34,7 +34,8 @@ ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient END (* For Setoid rewrite *) -let pr_morphism_signature _ _ _ = Setoid_replace.pr_morphism_signature +let pr_morphism_signature _ _ _ s = + spc () ++ Setoid_replace.pr_morphism_signature s ARGUMENT EXTEND morphism_signature TYPED AS morphism_signature |