let mk_case_pattern =
function
Ast.Pattern (head, href, vars) ->
- hbox true false (ident_w_href href head :: List.map aux_var vars)
+ hvbox true false (ident_w_href href head :: List.map aux_var vars)
| Ast.Wildcard -> builtin_symbol "_"
in
let patterns' =
assert (CicNotationEnv.well_typed ty value); (* INVARIANT *)
(* following assertion should be a conditional that makes this
* instantiation fail *)
- assert (CicNotationEnv.well_typed expected_ty value);
+ if not (CicNotationEnv.well_typed expected_ty value) then
+ begin
+ prerr_endline ("The variable " ^ name ^ " is used with the wrong type in the notation declaration");
+ assert false
+ end;
let value = CicNotationEnv.term_of_value value in
let value =
match expected_ty with
and subst_magic pos env = function
| Ast.List0 (p, sep_opt)
| Ast.List1 (p, sep_opt) ->
+ prerr_endline "1";
let rec_decls = CicNotationEnv.declarations_of_term p in
+ prerr_endline "2";
let rec_values =
List.map (fun (n, _) -> CicNotationEnv.lookup_list env n) rec_decls
in
+ prerr_endline "3";
let values = CicNotationUtil.ncombine rec_values in
+ prerr_endline "4";
let sep =
match sep_opt with
| None -> []
| Some l -> [ Ast.Literal l; break; space ]
in
+ prerr_endline "5";
let rec instantiate_list acc = function
| [] -> List.rev acc
| value_set :: [] ->