| NotationPt.Sort `Prop -> NCic.Sort NCic.Prop
| NotationPt.Sort `Set -> NCic.Sort (NCic.Type
[`Type,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
- | NotationPt.Sort (`Type _u) -> NCic.Sort (NCic.Type
- [`Type,NUri.uri_of_string "cic:/matita/pts/Type0.univ"])
| NotationPt.Sort (`NType s) -> NCic.Sort (NCic.Type
[`Type,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
| NotationPt.Sort (`NCProp s) -> NCic.Sort (NCic.Type
[`CProp,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
- | NotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type
- [`CProp,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
| NotationPt.Symbol (symbol, instance) ->
Disambiguate.resolve ~env ~mk_choice
(Symbol (symbol, instance)) (`Args [])
~uri:None ~is_path:true ~localization_tbl) ~context:[] path
;;
-let new_flavour_of_flavour = function
- | `Definition -> `Definition
- | `MutualDefinition -> `Definition
- | `Fact -> `Fact
- | `Lemma -> `Lemma
- | `Remark -> `Example
- | `Theorem -> `Theorem
- | `Variant -> `Corollary
- | `Axiom -> `Fact
-;;
-
let ncic_name_of_ident = function
| Ast.Ident (name, None) -> name
| _ -> assert false
uri, height, [], [],
(match bo,flavour with
| None,`Axiom ->
- let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
+ let attrs = `Provided, flavour, pragma in
NCic.Constant ([],name,None,ty',attrs)
| Some _,`Axiom -> assert false
| None,_ ->
- let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
+ let attrs = `Provided, flavour, pragma in
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
- let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
+ let attrs = `Provided, flavour, pragma in
NCic.Fixpoint (inductive,inductiveFuns,attrs)
| bo ->
let bo =
interpretate_term
~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo
in
- let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
+ let attrs = `Provided, flavour, pragma in
NCic.Constant ([],name,Some bo,ty',attrs)))
| NotationPt.Inductive (params,tyl) ->
let context,params =