diff options
author | 2004-02-18 18:32:33 +0000 | |
---|---|---|
committer | 2004-02-18 18:32:33 +0000 | |
commit | b5df1925bbc14f441247349b200aa3f5828e8427 (patch) | |
tree | c158ac5d3d3133f2fce8188f3d0b4a75bd0c5415 /translate | |
parent | 06900e469cd593c272f57c2af7d2e4f206a2f944 (diff) |
- fixed the Assert_failure error in kernel/modops
- fixed the problem with passing atomic tactics to ltacs
- restructured the distrib Makefile (can build a package from
the CVS working dir)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5358 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate')
-rw-r--r-- | translate/ppconstrnew.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index 8a2ce3765..9a86e3ffa 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -426,7 +426,8 @@ let pr_return_type pr po = pr_case_type pr po let pr_simple_return_type pr na po = (match na with - | Name id -> spc () ++ str "as " ++ pr_id id + | Some (Name id) -> + spc () ++ str "as " ++ pr_id id | _ -> mt ()) ++ pr_case_type pr po |