tl = OPT [ "with";
types = LIST1 [
name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
- OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
+ OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
(name, true, typ, constructors) ] SEP "with" -> types
] ->
let params =
ind_types
in
return_command loc (TacticAst.Inductive (params, ind_types))
+ | [ IDENT "coercion" | IDENT "Coercion" ] ; name = IDENT ->
+ return_command loc (TacticAst.Coercion (CicAst.Ident (name,Some [])))
+ | [ IDENT "coercion" | IDENT "Coercion" ] ; name = URI ->
+ return_command loc (TacticAst.Coercion (CicAst.Uri (name,Some [])))
| [ IDENT "goal" | IDENT "Goal" ]; typ = term;
body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
return_command loc (TacticAst.Theorem (`Goal, None, typ, body))
?enable_button_for_non_vars:bool ->
title:string -> msg:string -> id:string -> string list -> string list
- val interactive_interpretation_choice :
+ val interactive_interpretation_choice :
(string * string) list list -> int list
(** @param title gtk window title for user prompting
(Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent) in
let xmlpres = mpres_document pres_sequent in
Xml2Gdome.document_of_xml Misc.domImpl xmlpres,
- (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
+ (asequent,
+ (ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts))
;;
let mml_of_cic_object uri obj =
let pres = Content2pres.content2pres ~ids_to_inner_sorts content in
let xmlpres = mpres_document pres in
let mathml = Xml2Gdome.document_of_xml Misc.domImpl xmlpres in
- (mathml,
- (ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses))
+ (mathml,(annobj,
+ (ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses,
+ ids_to_inner_sorts,ids_to_inner_types)))
Cic.metasenv -> (* metasenv *)
Cic.conjecture -> (* sequent *)
Gdome.document * (* Math ML *)
+ (Cic.annconjecture * (* annsequent *)
((Cic.id, Cic.term) Hashtbl.t * (* id -> term *)
(Cic.id, Cic.id option) Hashtbl.t * (* id -> father id *)
- (Cic.id, Cic.hypothesis) Hashtbl.t) (* id -> hypothesis *)
+ (Cic.id, Cic.hypothesis) Hashtbl.t * (* id -> hypothesis *)
+ (Cic.id, string) Hashtbl.t)) (* ids_to_inner_sorts *)
val mml_of_cic_object :
UriManager.uri -> (* object uri *)
Cic.obj -> (* uri *)
Gdome.document * (* Math ML *)
+ (Cic.annobj * (* annobj *)
((Cic.id, Cic.term) Hashtbl.t * (* id -> term *)
(Cic.id, Cic.id option) Hashtbl.t * (* id -> father id *)
(Cic.id, Cic.conjecture) Hashtbl.t * (* id -> conjecture *)
- (Cic.id, Cic.hypothesis) Hashtbl.t) (* id -> hypothesis *)
+ (Cic.id, Cic.hypothesis) Hashtbl.t * (* id -> hypothesis *)
+ (Cic.id, string) Hashtbl.t * (* ids_to_inner_sorts *)
+ (Cic.id, Cic2acic.anntypes) Hashtbl.t))(* ids_to_inner_types *)
* - body is present when its given along with the command, otherwise it
* will be given in proof editing mode using the tactical language
*)
+ | Coercion of 'term
| Redo of int option
| Undo of int option
then
begin
prerr_endline "TROVATA coercion";
- Some (CicUtil.term_of_uri "cic://Coq/Reals/Raxioms/INR.con")
+ Some (CicUtil.term_of_uri "cic:/Coq/Reals/Raxioms/INR.con")
end
else
begin