X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FnCicCoercDeclaration.ml;h=3cf07626531c37902cff53640451885386211997;hb=b108ab28153129d6578d7d9c2ffdf19e6779d86f;hp=7fcd6a473f4595f70047f2bda5fce0b6867b68bf;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/grafite_engine/nCicCoercDeclaration.ml b/matita/components/grafite_engine/nCicCoercDeclaration.ml
index 7fcd6a473..3cf076265 100644
--- a/matita/components/grafite_engine/nCicCoercDeclaration.ml
+++ b/matita/components/grafite_engine/nCicCoercDeclaration.ml
@@ -311,7 +311,7 @@ let basic_eval_and_record_ncoercion_from_t_cpos_arity
   let status, uris =
    basic_eval_and_record_ncoercion (name,t,src,tgt,cpos,arity) status
   in
-   status,`New uris
+   status,uris
 ;;
 
 let eval_ncoercion status name t ty (id,src) tgt = 
@@ -330,6 +330,6 @@ let eval_ncoercion status name t ty (id,src) tgt =
  let status, uris =
   basic_eval_and_record_ncoercion (name,t,src,tgt,cpos,arity) status
  in
-  status,`New uris
+  status,uris
 ;;