aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorherbelin2004-08-23 17:37:19 +0000
committerherbelin2004-08-23 17:37:19 +0000
commit22b4f87057db8866ff224bbae3c5de21a6f4c3e1 (patch)
tree986296d5afcd2f1d0f0173ba698adb9e1a9d9e6d
parent7bb761dac1079ab82b10eeb407883c0d3e2f7aed (diff)
Précisions message d'erreur
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6026 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--parsing/ppconstr.ml2
-rw-r--r--parsing/termast.ml3
2 files changed, 2 insertions, 3 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index aa9482a2f2..7c573e07cc 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -293,7 +293,7 @@ let rec pr inherited a =
hov 0 (str "then" ++ brk (1,1) ++ pr ltop b1) ++ spc () ++
hov 0 (str "else" ++ brk (1,1) ++ pr ltop b2))), lif
| CLetTuple _ | CIf _ ->
- error "Let tuple not supported in v7"
+ anomaly "Let tuple and If not supported in v7"
| COrderedCase (_,(MatchStyle|RegularStyle as style),po,c,bl) ->
hov 0 (
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 689441bac0..021025f74a 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -261,7 +261,6 @@ let rec ast_of_raw = function
let nvar' = function Anonymous -> nvar wildcard | Name id -> nvar id in
let rec f l = function
| RLambda (_,na,RHole _,c) -> f (nvar' na :: l) c
- | RLetIn (_,na,RHole _,c) -> f (nvar' na :: l) c
| c -> List.rev l, ast_of_raw c in
let l,c = f [] bv in
let eqn = ope ("EQN", [c;ope ("PATTCONSTRUCT",(nvar wildcard)::l)]) in
@@ -280,7 +279,7 @@ let rec ast_of_raw = function
::(Array.to_list (Array.map ast_of_raw bv)))
| RLetTuple _ | RIf _ ->
- error "Let tuple not supported in v7"
+ anomaly "Let tuple and If not supported in v7"
| RRec (_,fk,idv,blv,tyv,bv) ->
let alfi = Array.map ast_of_ident idv in