aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/termast.ml
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>1999-12-09 09:59:27 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>1999-12-09 09:59:27 +0000
commitf09ca438e24bc4016b4e778dd8fd4de4641b7636 (patch)
tree4b108c844f99fb9bba496fa50d56445f5a8fd6ff /parsing/termast.ml
parentc4dccc430e10b784e65b5bf3330c55d658d2883d (diff)
Discharge (encore bugge)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@223 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/termast.ml')
-rw-r--r--parsing/termast.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/termast.ml b/parsing/termast.ml
index cdaa2a268..0ddee900f 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -27,7 +27,7 @@ let ids_of_ctxt cl =
| Rel n ->
warning "ids_of_ctxt: rel";
id_of_string ("REL "^(string_of_int n))
- | _-> anomaly"ids_of_ctxt")
+ | _-> anomaly "ids_of_ctxt")
(Array.to_list cl)
let ast_of_ident id = nvar (string_of_id id)