status#ppterm ~metasenv ~subst ~context term)) ;
Disambiguate.Uncertain loc_msg
| NCicRefiner.RefineFailure loc_msg ->
status#ppterm ~metasenv ~subst ~context term)) ;
Disambiguate.Uncertain loc_msg
| NCicRefiner.RefineFailure loc_msg ->
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
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
| NotationPt.Appl terms ->
NCic.Appl (List.map (aux ~localize loc context) terms)
| NotationPt.Binder (binder_kind, (var, typ), body) ->
| NotationPt.Appl terms ->
NCic.Appl (List.map (aux ~localize loc context) terms)
| NotationPt.Binder (binder_kind, (var, typ), body) ->
(`Args [ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ]))
| NotationPt.Case (term, indty_ident, outtype, branches) ->
let cic_term = aux ~localize loc context term in
(`Args [ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ]))
| NotationPt.Case (term, indty_ident, outtype, branches) ->
let cic_term = aux ~localize loc context term in
match indty_ident with
| Some (indty_ident, _) ->
(match Disambiguate.resolve ~env ~mk_choice
match indty_ident with
| Some (indty_ident, _) ->
(match Disambiguate.resolve ~env ~mk_choice
| NCic.Const (NReference.Ref (_,NReference.Ind _) as r) -> r
| NCic.Implicit _ ->
raise (Disambiguate.Try_again
| NCic.Const (NReference.Ref (_,NReference.Ind _) as r) -> r
| NCic.Implicit _ ->
raise (Disambiguate.Try_again
function
(Ast.Pattern (head, _, _), _) :: _ -> head
| (Ast.Wildcard, _) :: tl -> fst_constructor tl
function
(Ast.Pattern (head, _, _), _) :: _ -> head
| (Ast.Wildcard, _) :: tl -> fst_constructor tl
"of the term to be matched cannot be determined "^
"because it is an inductive type without constructors "^
"or because all patterns use wildcards")))
"of the term to be matched cannot be determined "^
"because it is an inductive type without constructors "^
"or because all patterns use wildcards")))
| NCic.Const (NReference.Ref (_,NReference.Con _) as r) ->
let b,_,_,_,_= NCicEnvironment.get_checked_indtys status r in
NReference.mk_indty b r
| NCic.Const (NReference.Ref (_,NReference.Con _) as r) ->
let b,_,_,_,_= NCicEnvironment.get_checked_indtys status r in
NReference.mk_indty b r
| NotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)
| NotationPt.UserInput -> NCic.Implicit `Hole
| NotationPt.Num (num, i) ->
| NotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)
| NotationPt.UserInput -> NCic.Implicit `Hole
| NotationPt.Num (num, i) ->
[`CProp,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
| NotationPt.Symbol (symbol, instance) ->
Disambiguate.resolve ~env ~mk_choice
[`CProp,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
| NotationPt.Symbol (symbol, instance) ->
Disambiguate.resolve ~env ~mk_choice
interpretate_term_option ~mk_choice ~localization_tbl ~obj_context in
let uri = match uri with | None -> assert false | Some u -> u in
match obj with
interpretate_term_option ~mk_choice ~localization_tbl ~obj_context in
let uri = match uri with | None -> assert false | Some u -> u in
match obj with
- | NotationPt.Theorem (flavour, name, ty, bo, pragma) ->
+ | NotationPt.Theorem (name, ty, bo, attrs) ->
+ let _, flavour, _ = attrs in
NCic.Constant ([],name,None,ty',attrs)
| Some _,`Axiom -> assert false
| None,_ ->
NCic.Constant ([],name,None,ty',attrs)
| Some _,`Axiom -> assert false
| None,_ ->
NCic.Constant ([],name,Some (NCic.Implicit `Term),ty',attrs)
| Some bo,_ ->
(match bo with
NCic.Constant ([],name,Some (NCic.Implicit `Term),ty',attrs)
| Some bo,_ ->
(match bo with
([],ncic_name_of_ident name, decr_idx, cic_type, cic_body))
defs
in
([],ncic_name_of_ident name, decr_idx, cic_type, cic_body))
defs
in
NCic.Fixpoint (inductive,inductiveFuns,attrs)
| bo ->
let bo =
interpretate_term status
~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo
in
NCic.Fixpoint (inductive,inductiveFuns,attrs)
| bo ->
let bo =
interpretate_term status
~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo
in
NCic.Constant ([],name,Some bo,ty',attrs)))
| NotationPt.Inductive (params,tyl) ->
let context,params =
NCic.Constant ([],name,Some bo,ty',attrs)))
| NotationPt.Inductive (params,tyl) ->
let context,params =
in
List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
;;
in
List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
;;