ported to new types in grafite*/

diff --git a/helm/ocaml/grafite2/grafiteEngine.ml b/helm/ocaml/grafite2/grafiteEngine.ml
index d4a16d2d6ce75370813e164875d4e81158e28bbf..1fa272b22987dbf123a751e422705d0eded4fe26 100644 (file)
--- a/helm/ocaml/grafite2/grafiteEngine.ml
+++ b/helm/ocaml/grafite2/grafiteEngine.ml
@@ -327,8 +327,8 @@ type eval_ast =
 
   disambiguate_command:
    (GrafiteTypes.status ->
-    ('term, 'obj) GrafiteAst.command ->
-    GrafiteTypes.status * (Cic.term, Cic.obj) GrafiteAst.command) ->
+    'obj GrafiteAst.command ->
+    GrafiteTypes.status * Cic.obj GrafiteAst.command) ->
 
   ?do_heavy_checks:bool ->
   ?clean_baseuri:bool ->
@@ -342,9 +342,9 @@ type 'a eval_command =
   baseuri_of_script:(string -> string) ->
   disambiguate_command:
    (GrafiteTypes.status ->
-    ('term,'obj) GrafiteAst.command ->
-    GrafiteTypes.status * (Cic.term, Cic.obj) GrafiteAst.command) ->
-  options -> GrafiteTypes.status -> ('term,'obj) GrafiteAst.command ->
+    'obj GrafiteAst.command ->
+    GrafiteTypes.status * Cic.obj GrafiteAst.command) ->
+  options -> GrafiteTypes.status -> 'obj GrafiteAst.command ->
    GrafiteTypes.status
  }
 
@@ -360,8 +360,8 @@ type 'a eval_executable =
 
   disambiguate_command:
    (GrafiteTypes.status ->
-    ('term, 'obj) GrafiteAst.command ->
-    GrafiteTypes.status * (Cic.term, Cic.obj) GrafiteAst.command) ->
+    'obj GrafiteAst.command ->
+    GrafiteTypes.status * Cic.obj GrafiteAst.command) ->
 
   options ->
   GrafiteTypes.status ->
@@ -371,11 +371,9 @@ type 'a eval_executable =
 type 'a eval_from_moo = { efm_go: GrafiteTypes.status ref -> string -> unit }
       
 let coercion_moo_statement_of uri =
-  GrafiteAst.Coercion 
-    (DisambiguateTypes.dummy_floc, CicUtil.term_of_uri uri, false)
+  GrafiteAst.Coercion (DisambiguateTypes.dummy_floc, uri, false)
 
-let eval_coercion status ~add_composites coercion =
- let uri = CicUtil.uri_of_term coercion in
+let eval_coercion status ~add_composites uri =
  let basedir = Helm_registry.get "matita.basedir" in
  let compounds = LibrarySync.add_coercion ~add_composites ~basedir uri in
  let moo_content = coercion_moo_statement_of uri in
@@ -593,8 +591,8 @@ let rec eval_command = {ec_go = fun ~baseuri_of_script ~disambiguate_command opt
       let status, _lemmas = add_obj uri obj status in
        (* should we assert lemmas = [] ? *)
        {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}
-  | GrafiteAst.Coercion (loc, coercion, add_composites) ->
-     eval_coercion status ~add_composites coercion
+  | GrafiteAst.Coercion (loc, uri, add_composites) ->
+     eval_coercion status ~add_composites uri
   | GrafiteAst.Alias (loc, spec) -> 
      let diff =
       (*CSC: Warning: this code should be factorized with the corresponding

diff --git a/helm/ocaml/grafite2/grafiteEngine.mli b/helm/ocaml/grafite2/grafiteEngine.mli
index e317060b580e2c84a544dbbcd88c0e298526d393..ccdc306c25789aafd7e32e14a4da1312960e6c11 100644 (file)
--- a/helm/ocaml/grafite2/grafiteEngine.mli
+++ b/helm/ocaml/grafite2/grafiteEngine.mli
@@ -38,8 +38,8 @@ val eval_ast :
 
   disambiguate_command:
    (GrafiteTypes.status ->
-    ('term, 'obj) GrafiteAst.command ->
-    GrafiteTypes.status * (Cic.term, Cic.obj) GrafiteAst.command) ->
+    'obj GrafiteAst.command ->
+    GrafiteTypes.status * Cic.obj GrafiteAst.command) ->
 
   ?do_heavy_checks:bool ->
   ?clean_baseuri:bool ->