| Cic.Meta _ -> PT.Implicit
| Cic.Sort (Cic.Type u) -> PT.Sort (`Type u)
| Cic.Sort Cic.Set -> PT.Sort `Set
- | Cic.Sort Cic.CProp -> PT.Sort `CProp
+ | Cic.Sort (Cic.CProp u) -> PT.Sort (`CProp u)
| Cic.Sort Cic.Prop -> PT.Sort `Prop
| _ as t -> PT.Ident ("ERROR: "^CicPp.ppterm t, None)
in
cic2grafite cc menv proof_term
else
(* alternative using FG stuff *)
- let proof_term, how_many_lambdas =
- Auto.lambda_close ~prefix_name:"orrible_hack_"
- proof_term menv cc
- in
- let ty,_ =
- CicTypeChecker.type_of_aux'
- menv [] proof_term CicUniv.empty_ugraph
- in
- let obj =
- Cic.Constant ("",Some proof_term, ty, [], [`Flavour `Lemma])
- in
- Pcre.qreplace ~templ:"?" ~pat:"orrible_hack_[0-9]+"
- (strip_comments
- (ApplyTransformation.txt_of_cic_object
- ~map_unicode_to_tex:(Helm_registry.get_bool
- "matita.paste_unicode_as_tex")
- ~skip_thm_and_qed:true
- ~skip_initial_lambdas:how_many_lambdas
- 80 (GrafiteAst.Procedural None) "" obj))
+ let map_unicode_to_tex =
+ Helm_registry.get_bool "matita.paste_unicode_as_tex"
+ in
+ ApplyTransformation.procedural_txt_of_cic_term
+ ~map_unicode_to_tex 78 cc proof_term
in
let text = comment parsed_text ^ "\n" ^ proof_script ^ trailer in
[],text,parsed_text_length
ProofEngineTypes.Fail _ as exn ->
raise exn
(* [], comment parsed_text ^ "\nfail.\n", parsed_text_length *))
- | TA.Inline (_,style,suri,prefix) ->
+ | TA.Inline (_,style,suri,prefix,flavour) ->
let str =
ApplyTransformation.txt_of_inline_macro
~map_unicode_to_tex:(Helm_registry.get_bool
"matita.paste_unicode_as_tex")
- style suri prefix
+ style ?flavour prefix suri
in
[], str, String.length parsed_text
let _,parsed_text_length = MatitaGtkMisc.utf8_parsed_text s loc in
(* CSC: why +1 in the following lines ???? *)
let parsed_text_length = parsed_text_length + 1 in
-prerr_endline ("## " ^ string_of_int parsed_text_length);
let remain_len = String.length s - parsed_text_length in
let next = String.sub s parsed_text_length remain_len in
is_there_only_comments lexicon_status next