Most warnings turned into errors and avoided

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

diff --git a/matita/components/grafite_engine/nCicCoercDeclaration.ml b/matita/components/grafite_engine/nCicCoercDeclaration.ml
index 1c6c63ebc2feac4dd6e308d2b65778ad96503718..a2ed8044a187a9236f365f18794a9f73ee65c02b 100644 (file)
--- a/matita/components/grafite_engine/nCicCoercDeclaration.ml
+++ b/matita/components/grafite_engine/nCicCoercDeclaration.ml
@@ -133,7 +133,7 @@ let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
            (try 
             let metasenv,subst,status,src =
               GrafiteDisambiguate.disambiguate_nterm 
-                status None ctx [] [] ("",0,src) in
+                status `XTSort ctx [] [] ("",0,src) in
             let src = NCicUntrusted.apply_subst status subst [] src in
             (* CHECK that the declared pattern matches the abstraction *)
             let _ = NCicUnification.unify status metasenv subst ctx ty src in
@@ -152,9 +152,9 @@ disambiguation error")))
       aux 0 [] ty
   in
   let status, tgt, arity = 
-    let metasenv,subst,status,tgt =
+    let _metasenv,subst,status,tgt =
       GrafiteDisambiguate.disambiguate_nterm 
-        status None [] [] [] ("",0,tgt) in
+        status `XTSort [] [] [] ("",0,tgt) in
     let tgt = NCicUntrusted.apply_subst status subst [] tgt in
     (* CHECK che sia unificabile mancante *)
     let rec count_prod = function
@@ -182,7 +182,7 @@ let fresh_uri status prefix suffix =
 
 exception Stop;;
 
-let close_graph name t s d to_s from_d p a status =
+let close_graph _name t s d to_s from_d _p a status =
   let c =
     List.find 
      (function (_,_,NCic.Appl (x::_),_,_) -> x = t | _ -> assert false) 
@@ -228,7 +228,7 @@ let close_graph name t s d to_s from_d p a status =
          let pos = 
            match p with 
            | NCic.Meta (p,_) -> pos_in_list p (List.map fst metasenv) 
-           | t -> raise Stop
+           | _t -> raise Stop
          in
          let ty = NCicTypeChecker.typeof status ~metasenv:[] ~subst:[] [] bo in
          let src,tgt = src_tgt_of_ty_cpos_arity status ty pos arity in
@@ -292,8 +292,8 @@ let record_ncoercion =
   let d = refresh_uri_in_term d in
    basic_index_ncoercion (name,compose,t,s,d,p,a)
  in
- let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term
-  ~refresh_uri_in_reference ~alias_only status
+ let aux_l l ~refresh_uri_in_universe:_ ~refresh_uri_in_term
+  ~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
@@ -321,11 +321,11 @@ let basic_eval_and_record_ncoercion_from_t_cpos_arity
 
 let eval_ncoercion (status: #GrafiteTypes.status) name compose t ty (id,src) tgt = 
  let metasenv,subst,status,ty =
-  GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,ty) in
+  GrafiteDisambiguate.disambiguate_nterm status `XTSort [] [] [] ("",0,ty) in
  assert (metasenv=[]);
  let ty = NCicUntrusted.apply_subst status subst [] ty in
  let metasenv,subst,status,t =
-  GrafiteDisambiguate.disambiguate_nterm status (Some ty) [] [] [] ("",0,t) in
+  GrafiteDisambiguate.disambiguate_nterm status (`XTSome ty) [] [] [] ("",0,t) in
  assert (metasenv=[]);
  let t = NCicUntrusted.apply_subst status subst [] t in
  let status, src, tgt, cpos, arity =