diff options
| author | herbelin | 2003-04-27 07:44:00 +0000 |
|---|---|---|
| committer | herbelin | 2003-04-27 07:44:00 +0000 |
| commit | 8412d45181edd1d0627df454fa370d858d3fd623 (patch) | |
| tree | a3e553afd424992d6935712b0d41b389ae777726 | |
| parent | b1901a4f1278465179718d614b3d26b19eefcd75 (diff) | |
Reparation affichage LetTac
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3958 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/pptactic.ml | 8 | ||||
| -rw-r--r-- | translate/pptacticnew.ml | 8 |
2 files changed, 8 insertions, 8 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 1147e84fd4..8560726fb2 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -153,14 +153,14 @@ let pr_clause pr_id = function | [] -> mt () | l -> spc () ++ hov 0 (str "in" ++ prlist (pr_hyp_location pr_id) l) -let pr_clause_pattern pr_id = function (* To check *) +let pr_clause_pattern pr_id = function | (None, []) -> mt () | (glopt,l) -> - str "in" ++ + str " in" ++ prlist - (fun (id,nl) -> spc () ++ prlist_with_sep spc int nl + (fun (id,nl) -> prlist (pr_arg int) nl ++ spc () ++ pr_id id) l ++ - pr_opt (prlist_with_sep spc int) glopt + pr_opt (fun nl -> prlist_with_sep spc int nl ++ str " Goal") glopt let pr_subterms pr occl = hov 0 (pr_occurrences pr occl ++ spc () ++ str "with") diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml index 0cc3234c27..44224227d1 100644 --- a/translate/pptacticnew.ml +++ b/translate/pptacticnew.ml @@ -85,14 +85,14 @@ let pr_clause pr_id = function | [] -> mt () | l -> spc () ++ hov 0 (str "in" ++ prlist (pr_hyp_location pr_id) l) -let pr_clause_pattern pr_id = function (* To check *) +let pr_clause_pattern pr_id = function | (None, []) -> mt () | (glopt,l) -> - str "in" ++ + str " in" ++ prlist - (fun (id,nl) -> spc () ++ prlist_with_sep spc int nl + (fun (id,nl) -> prlist (pr_arg int) nl ++ spc () ++ pr_id id) l ++ - pr_opt (prlist_with_sep spc int) glopt + pr_opt (fun nl -> prlist_with_sep spc int nl ++ str " Goal") glopt let pr_induction_arg prc = function | ElimOnConstr c -> prc c |