This commit patches the environment and the library so that their status is

[helm.git] / matitaB / components / grafite_engine / nCicCoercDeclaration.ml

diff --git a/matitaB/components/grafite_engine/nCicCoercDeclaration.ml b/matitaB/components/grafite_engine/nCicCoercDeclaration.ml
index 2693d608b37307140d80fa6b2b063f3447cbbd4e..cf3c127b95371d9536bb0d7a3a3c9e5e7d265c5e 100644 (file)
--- a/matitaB/components/grafite_engine/nCicCoercDeclaration.ml
+++ b/matitaB/components/grafite_engine/nCicCoercDeclaration.ml
@@ -134,7 +134,7 @@ let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
          if name <> id then aux (cpos+1) ((name,NCic.Decl ty)::ctx) bo
          else
            (try 
-            let newast,metasenv,subst,status,src =
+            let metasenv,subst,status,src =
               GrafiteDisambiguate.disambiguate_nterm 
                 status None ctx [] [] ("",0,src) in
             let src = NCicUntrusted.apply_subst status subst [] src in
@@ -152,7 +152,7 @@ let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
       aux 0 [] ty
   in
   let status, tgt, arity = 
-    let newast, metasenv,subst,status,tgt =
+    let metasenv,subst,status,tgt =
       GrafiteDisambiguate.disambiguate_nterm 
         status None [] [] [] ("",0,tgt) in
     let tgt = NCicUntrusted.apply_subst status subst [] tgt in
@@ -174,7 +174,7 @@ let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
 let fresh_uri status prefix suffix = 
   let mk x = NUri.uri_of_string (status#baseuri ^ "/" ^ prefix ^ x ^ suffix) in
   let rec diverge u i =
-    if NCicLibrary.aliases_of u = [] then u
+    if NCicLibrary.aliases_of status u = [] then u
     else diverge (mk ("__" ^ string_of_int i)) (i+1)
   in
    diverge (mk "") 0
@@ -295,7 +295,9 @@ let record_ncoercion =
   ~refresh_uri_in_reference ~alias_only status
  =
   if not alias_only then
-   List.fold_right (aux ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))) l status
+   List.fold_right 
+    (aux ~refresh_uri_in_term:(refresh_uri_in_term
+     (status:>NCicEnvironment.status))) l status
   else
    status
  in
@@ -319,11 +321,11 @@ let basic_eval_and_record_ncoercion_from_t_cpos_arity
 ;;
 
 let eval_ncoercion (status: #GrafiteTypes.status) name t ty (id,src) tgt = 
- let newast_ty,metasenv,subst,status,ty =
+ let metasenv,subst,status,ty =
   GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,ty) in
  assert (metasenv=[]);
  let ty = NCicUntrusted.apply_subst status subst [] ty in
- let newast_t,metasenv,subst,status,t =
+ let metasenv,subst,status,t =
   GrafiteDisambiguate.disambiguate_nterm status (Some ty) [] [] [] ("",0,t) in
  assert (metasenv=[]);
  let t = NCicUntrusted.apply_subst status subst [] t in