raise (Try_again (lazy "The type of the term to be matched
is still unknown"))
| _ ->
raise (Try_again (lazy "The type of the term to be matched
is still unknown"))
| _ ->
- raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
+ raise (Invalid_choice (lazy (loc,"The type of the term to be matched is not (co)inductive!"))))
| None ->
let rec fst_constructor =
function
(Ast.Pattern (head, _, _), _) :: _ -> head
| (Ast.Wildcard, _) :: tl -> fst_constructor tl
| None ->
let rec fst_constructor =
function
(Ast.Pattern (head, _, _), _) :: _ -> head
| (Ast.Wildcard, _) :: tl -> fst_constructor tl
- | [] -> raise (Invalid_choice (Some loc, lazy "The type of the term to be matched cannot be determined because it is an inductive type without constructors or because all patterns use wildcards"))
+ | [] -> raise (Invalid_choice (lazy (loc,"The type of the term to be matched cannot be determined because it is an inductive type without constructors or because all patterns use wildcards")))
in
(match resolve env (Id (fst_constructor branches)) () with
List.assoc s ids_to_uris, aux ~localize loc context term
with Not_found ->
(try
List.assoc s ids_to_uris, aux ~localize loc context term
with Not_found ->
- raise (Invalid_choice (Some loc, lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on"))))
+ raise (Invalid_choice (lazy (loc, "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on")))))