let mk_id id =
let id = if id = "_" then fresh_name () else id in
- NotationPt.Ident (id,None)
+ NotationPt.Ident (id,`Ambiguous)
;;
(*CSC: cut&paste from nCicReduction.split_prods, but does not check that
NCic.Inductive (true,leftno,[itl],_) ->
List.map (fun s-> mk_elim status uri leftno itl (ast_of_sort s) (`Elim s))
(NCic.Prop::
- List.map (fun s -> NCic.Type s) (NCicEnvironment.get_universes ()))
+ List.map (fun s -> NCic.Type s) (NCicEnvironment.get_universes status))
| _ -> []
;;
let rec pp rels =
function
NCic.Rel i -> List.nth rels (i - 1)
- | NCic.Const _ as t ->
- NotationPt.Ident
- (status#ppterm ~metasenv:[] ~subst:[] ~context:[] t,None)
+ | NCic.Const _ as t -> NotationPt.NCic t
| NCic.Sort s -> NotationPt.Sort (fst (ast_of_sort s))
| NCic.Meta _
| NCic.Implicit _ -> assert false
let arg = mk_id "xxx" in
let arg_ty = mk_appl (mk_id tyname :: List.rev names) in
let bvar = mk_id "yyy" in
- let underscore = NotationPt.Ident ("_",None),None in
+ let underscore = NotationPt.Ident ("_",`Ambiguous),None in
let bvars =
HExtlib.mk_list underscore i @ [bvar,None] @
HExtlib.mk_list underscore (argsno - i -1) in