summaryrefslogtreecommitdiff
path: root/interp/topconstr.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2008-08-08 13:18:42 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2008-08-08 13:18:42 +0200
commit870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch)
tree0c647056de1832cf1dba5ba58758b9121418e4be /interp/topconstr.ml
parenta0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff)
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'interp/topconstr.ml')
-rw-r--r--interp/topconstr.ml32
1 files changed, 16 insertions, 16 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index b858eecb..a51b6bb0 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: topconstr.ml 11024 2008-05-30 12:41:39Z msozeau $ *)
+(* $Id: topconstr.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
(*i*)
open Pp
@@ -150,7 +150,7 @@ let compare_rawconstr f t1 t2 = match t1,t2 with
| RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _),_
| _,(RLetIn _ | RCases _ | RRec _ | RDynamic _
| RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _)
- -> error "Unsupported construction in recursive notations"
+ -> error "Unsupported construction in recursive notations."
| (RRef _ | RVar _ | RApp _ | RLambda _ | RProd _ | RHole _ | RSort _), _
-> false
@@ -168,13 +168,13 @@ let discriminate_patterns foundvars nl l1 l2 =
| _ -> compare_rawconstr (aux (n+1)) c1 c2 in
let l = list_map2_i aux 0 l1 l2 in
if not (List.for_all ((=) true) l) then
- error "Both ends of the recursive pattern differ";
+ error "Both ends of the recursive pattern differ.";
match !diff with
- | None -> error "Both ends of the recursive pattern are the same"
+ | None -> error "Both ends of the recursive pattern are the same."
| Some (x,y,_ as discr) ->
List.iter (fun id ->
if List.mem id !foundvars
- then error "Variables used in the recursive part of a pattern are not allowed to occur outside of the recursive part";
+ then errorlabstrm "" (strbrk "Variables used in the recursive part of a pattern are not allowed to occur outside of the recursive part.");
foundvars := id::!foundvars) [x;y];
discr
@@ -212,7 +212,7 @@ let aconstr_and_vars_of_rawconstr a =
Array.iter (fun id -> found := id::!found) idl;
let dll = Array.map (List.map (fun (na,bk,oc,b) ->
if bk <> Explicit then
- error "Binders marked as implicit not allowed in notations";
+ error "Binders marked as implicit not allowed in notations.";
add_name found na; (na,Option.map aux oc,aux b))) dll in
ARec (fk,idl,dll,Array.map aux tl,Array.map aux bl)
| RCast (_,c,k) -> ACast (aux c,
@@ -223,17 +223,17 @@ let aconstr_and_vars_of_rawconstr a =
| RRef (_,r) -> ARef r
| RPatVar (_,(_,n)) -> APatVar n
| RDynamic _ | REvar _ ->
- error "Existential variables not allowed in notations"
+ error "Existential variables not allowed in notations."
(* Recognizing recursive notations *)
and terminator_of_pat f1 ll1 lr1 = function
| RApp (loc,f2,l2) ->
- if not (eq_rawconstr f1 f2) then error
- "Cannot recognize the same head to both ends of the recursive pattern";
+ if not (eq_rawconstr f1 f2) then errorlabstrm ""
+ (strbrk "Cannot recognize the same head to both ends of the recursive pattern.");
let nl = List.length ll1 in
let nr = List.length lr1 in
if List.length l2 <> nl + nr + 1 then
- error "Both ends of the recursive pattern have different lengths";
+ error "Both ends of the recursive pattern have different lengths.";
let ll2,l2' = list_chop nl l2 in
let t = List.hd l2' and lr2 = List.tl l2' in
let x,y,order = discriminate_patterns found nl (ll1@lr1) (ll2@lr2) in
@@ -241,8 +241,8 @@ let aconstr_and_vars_of_rawconstr a =
if order then RApp (loc,f2,ll2@RVar (loc,ldots_var)::lr2)
else RApp (loc,f1,ll1@RVar (loc,ldots_var)::lr1) in
(if order then y else x),(if order then x else y), aux iter, aux t, order
- | _ -> error "One end of the recursive pattern is not an application"
-
+ | _ -> error "One end of the recursive pattern is not an application."
+
and make_aconstr_list f args =
let rec find_patterns acc = function
| RApp(_,RVar (_,a),[c]) :: l when a = ldots_var ->
@@ -250,7 +250,7 @@ let aconstr_and_vars_of_rawconstr a =
let x,y,iter,term,lassoc = terminator_of_pat f (List.rev acc) l c in
AList (x,y,iter,term,lassoc)
| a::l -> find_patterns (a::acc) l
- | [] -> error "Ill-formed recursive notation"
+ | [] -> error "Ill-formed recursive notation."
in find_patterns [] args
in
@@ -262,7 +262,7 @@ let aconstr_of_rawconstr vars a =
let a,foundvars = aconstr_and_vars_of_rawconstr a in
let check_type x =
if not (List.mem x foundvars) then
- error ((string_of_id x)^" is unbound in the right-hand-side") in
+ error ((string_of_id x)^" is unbound in the right-hand-side.") in
List.iter check_type vars;
a
@@ -590,7 +590,7 @@ type notation = string
type explicitation = ExplByPos of int * identifier option | ExplByName of identifier
-type binder_kind = Default of binding_kind | TypeClass of binding_kind
+type binder_kind = Default of binding_kind | TypeClass of binding_kind * binding_kind
type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
@@ -853,7 +853,7 @@ let coerce_to_id = function
| CRef (Ident (loc,id)) -> (loc,id)
| a -> user_err_loc
(constr_loc a,"coerce_to_id",
- str "This expression should be a simple identifier")
+ str "This expression should be a simple identifier.")
(* Used in correctness and interface *)