diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-21 11:51:33 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-21 11:51:33 +0000 |
| commit | 0dece739c580b39d77708bb8117442e7e1cd560b (patch) | |
| tree | 3db834fd12224590c4feddd213a41a0edd7c4986 /parsing/pptactic.ml | |
| parent | 094b40758cb4278b33a87e5633cf4ac716f348b4 (diff) | |
Légère amélioration des messages d'erreur des with-bindings et des Rewrite
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3474 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/pptactic.ml')
| -rw-r--r-- | parsing/pptactic.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 6c45c9e70..c44881614 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -75,8 +75,8 @@ let pr_quantified_hypothesis = function let pr_quantified_hypothesis_arg h = spc () ++ pr_quantified_hypothesis h let pr_binding prc = function - | NamedHyp id, c -> hov 1 (pr_id id ++ str ":=" ++ cut () ++ prc c) - | AnonHyp n, c -> hov 1 (int n ++ str ":=" ++ cut () ++ prc c) + | loc, NamedHyp id, c -> hov 1 (pr_id id ++ str ":=" ++ cut () ++ prc c) + | loc, AnonHyp n, c -> hov 1 (int n ++ str ":=" ++ cut () ++ prc c) let pr_bindings prc = function | ImplicitBindings l -> |