From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 12 Dec 2005 16:01:29 +0000 (+0000)
Subject: ported to new types in grafite*/
X-Git-Tag: make_still_working~8013
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d6a93ae23730073aa31e50537f0708a105ba873a;p=helm.git

ported to new types in grafite*/
---

diff --git a/helm/ocaml/grafite2/grafiteEngine.ml b/helm/ocaml/grafite2/grafiteEngine.ml
index d4a16d2d6..1fa272b22 100644
--- 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 e317060b5..ccdc306c2 100644
--- 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 ->