- Changed ApplyTransformation API to return both the mathml and acic,

  plus all the related tables
- Added the "Coercion" keyword to CicTextualParser2

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 00b4c4418cf7847d82b8dcee13dfb1c6b00e97d3..478e97d390531fe2df2e77f29570a0e0c17455cb 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -392,7 +392,7 @@ EXTEND
     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 =
@@ -427,6 +427,10 @@ EXTEND
             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))

diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli
index c210849669320aaaa57e6e2cfc5e0cb2e119fe96..6146a082ddc9548db5bea3f89271862b77fad5e8 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli
@@ -47,7 +47,7 @@ module type Callbacks =
       ?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

diff --git a/helm/ocaml/cic_transformations/applyTransformation.ml b/helm/ocaml/cic_transformations/applyTransformation.ml
index 784ab89d7b3ae966ac33ccb7c25d4d1d890404cd..4d1a65069a380f4f223a3e88b2a2ebbf07b62a4b 100644 (file)
--- a/helm/ocaml/cic_transformations/applyTransformation.ml
+++ b/helm/ocaml/cic_transformations/applyTransformation.ml
@@ -46,7 +46,8 @@ let mml_of_cic_sequent metasenv sequent =
     (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 =
@@ -61,6 +62,7 @@ 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)))
 

diff --git a/helm/ocaml/cic_transformations/applyTransformation.mli b/helm/ocaml/cic_transformations/applyTransformation.mli
index 1b646aa6e9a4d3cb02522c1ec524f3fd040b42f2..f7d3d2da2c09cfa15b1e865e8ee44eba02d9bbde 100644 (file)
--- a/helm/ocaml/cic_transformations/applyTransformation.mli
+++ b/helm/ocaml/cic_transformations/applyTransformation.mli
@@ -37,16 +37,21 @@ val mml_of_cic_sequent :
  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 *)
 

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index 8c678de93ba9d9fe6d0d91e2ac1d362efe03437d..1b4e906e0ed508a8099a9616516470ef952caafe 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -111,6 +111,7 @@ type 'term command =
        * - 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
 

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index fe70f250aa89999161824cf26d08639dc18739a7..d8b822d82cf6f6b39287025869e22bef114a7482 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -52,7 +52,7 @@ let look_for_coercion src tgt =
   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