Keeping track of locations of disambiguated ids and symbols.

[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..a26d5ec7c267b986449b9ae55646bbc9660c40ee 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
@@ -319,11 +319,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