diff options
| author | herbelin | 2004-08-23 17:37:19 +0000 |
|---|---|---|
| committer | herbelin | 2004-08-23 17:37:19 +0000 |
| commit | 22b4f87057db8866ff224bbae3c5de21a6f4c3e1 (patch) | |
| tree | 986296d5afcd2f1d0f0173ba698adb9e1a9d9e6d | |
| parent | 7bb761dac1079ab82b10eeb407883c0d3e2f7aed (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.ml | 2 | ||||
| -rw-r--r-- | parsing/termast.ml | 3 |
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 |
