X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=f286cf6b8160fac4bc34dba41eeaf018742b5b11;hb=8aa44cb352041dd314011996b4b1a1ff8990a000;hp=2f37a4e92f5c1fcc0ba6a84c2ebfed95a0725a92;hpb=41c4bfe9415b1b40278878dd767b734c61a47a69;p=helm.git

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 2f37a4e92..f286cf6b8 100644
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -485,9 +485,10 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
       GrafiteTypes.Serializer.require
        ~alias_only ~baseuri ~fname:fullpath status
   | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
-  | GrafiteAst.NCoercion (loc, name, t, ty, source, target) ->
+  | GrafiteAst.NCoercion (loc, name, compose, t, ty, source, target) ->
      let status, composites =
-      NCicCoercDeclaration.eval_ncoercion status name t ty source target in
+      NCicCoercDeclaration.eval_ncoercion status name compose t ty source
+       target in
      let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
      let aliases = GrafiteDisambiguate.aliases_for_objs status composites in
       eval_alias status (mode,aliases)
@@ -622,7 +623,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                  let status, nuris = 
                    NCicCoercDeclaration.
                      basic_eval_and_record_ncoercion_from_t_cpos_arity 
-                      status (name,t,cpos,arity) in
+                      status (name,true,t,cpos,arity) in
                  let aliases = GrafiteDisambiguate.aliases_for_objs status nuris in
                   eval_alias status (mode,aliases)
                with MultiPassDisambiguator.DisambiguationError _->