let variable_closure k =
(fun matched_terms terms ->
- prerr_endline "variable_closure";
match terms with
| hd :: tl -> k (hd :: matched_terms) tl
| _ -> assert false)
let constructor_closure ks k =
(fun matched_terms terms ->
- prerr_endline "constructor_closure";
match terms with
| t :: tl ->
(try
| Pt.Variable _ -> Variable
| Pt.Magic _
| Pt.Layout _
- | Pt.Literal _ as t ->
- prerr_endline (CicNotationPp.pp_term t);
- assert false
+ | Pt.Literal _ as t -> assert false
| _ -> Constructor
let tag_of_pattern = CicNotationTag.get_tag
let tag_of_term = CicNotationTag.get_tag
candidates
in
let match_cb rows =
- prerr_endline (sprintf "match_cb on %d row(s)" (List.length rows));
let candidates =
List.map
(fun (pl, pid) ->
let compiler rows =
let match_cb rows =
- prerr_endline (sprintf "match_cb on %d row(s)" (List.length rows));
let pl, pid = try List.hd rows with Not_found -> assert false in
(fun matched_terms ->
let env =