let refine_obj status metasenv subst _context _uri ~use_coercions obj _ _ugraph
~localization_tbl
=
+ (*prerr_endline ((sprintf "TEST_INTERPRETATION: %s" (status#ppobj obj)));*)
assert (metasenv=[]);
assert (subst=[]);
let localise t =
NCicUntrusted.NCicHash.add localization_tbl res loc;
res
| NotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
- | NotationPt.Appl (NotationPt.Appl inner :: args) ->
- aux ~localize loc context (NotationPt.Appl (inner @ args))
| NotationPt.Appl
- (NotationPt.AttributedTerm (att,(NotationPt.Appl inner))::args)->
+ (NotationPt.AttributedTerm (att, inner)::args)->
aux ~localize loc context
- (NotationPt.AttributedTerm (att,NotationPt.Appl (inner @ args)))
+ (NotationPt.AttributedTerm (att,NotationPt.Appl (inner :: args)))
+ | NotationPt.Appl (NotationPt.Appl inner :: args) ->
+ aux ~localize loc context (NotationPt.Appl (inner @ args))
| NotationPt.Appl (NotationPt.Symbol (symb, i) :: args) ->
let cic_args = List.map (aux ~localize loc context) args in
Disambiguate.resolve ~mk_choice ~env (Symbol (symb, i)) (`Args cic_args)
raise (DisambiguateTypes.Invalid_choice
(lazy (loc, "Syntax error: the left hand side of a "^
"branch pattern must be \"_\"")))
- ) branches
+ ) branches in
+ let indtype_ref =
+ NReference.reference_of_string "cic:/fake_indty.ind(0,0,0)"
in
- (*
- NCic.MutCase (ref, cic_outtype, cic_term,
- (List.map do_branch branches))
- *) ignore branches; assert false (* patterns not implemented yet *)
+ NCic.Match (indtype_ref, cic_outtype, cic_term,
+ (List.map do_branch branches))
else
let indtype_ref =
match indty_ident with