Fixing indexing (commit parziale di Claudio?)

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

diff --git a/helm/software/components/grafite_engine/nCicCoercDeclaration.ml b/helm/software/components/grafite_engine/nCicCoercDeclaration.ml
index 2f103cf83f944fe2255a908cf7c10779803b4da1..fa6b163ad97371a71ff238ff118e63227cec944e 100644 (file)
--- a/helm/software/components/grafite_engine/nCicCoercDeclaration.ml
+++ b/helm/software/components/grafite_engine/nCicCoercDeclaration.ml
@@ -32,12 +32,6 @@ let pos_in_list x l =
       | None -> assert false
 ;;
 
-let pos_of x t = 
-  match t with
-  | NCic.Appl l -> pos_in_list x l
-  | _ -> assert false
-;;
-
 let rec count_prod = function
   | NCic.Prod (_,_,x) -> 1 + count_prod x
   | _ -> 0
@@ -223,12 +217,14 @@ let close_graph name t s d to_s from_d p a status =
             (metasenv,[]) upl
          in
          let bo = NCicUntrusted.apply_subst subst [] bo in
+         let p = NCicUntrusted.apply_subst subst [] p in
+         let metasenv = NCicUntrusted.apply_subst_metasenv subst metasenv in
          let metasenv = toposort metasenv in
          let bo = close_in_context bo metasenv in
          let pos = 
            match p with 
            | NCic.Meta (p,_) -> pos_in_list p (List.map fst metasenv) 
-           | _ -> assert false
+           | t -> assert false
          in
          let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] bo in
          let src,tgt = src_tgt_of_ty_cpos_arity ty pos arity in
@@ -294,7 +290,10 @@ let record_ncoercion =
  let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term =
    List.fold_right (aux ~refresh_uri_in_universe ~refresh_uri_in_term) l
  in
-  NCicLibrary.Serializer.register "ncoercion" aux_l
+  NCicLibrary.Serializer.register#run "ncoercion"
+   object(self : 'a NCicLibrary.register_type)
+    method run = aux_l 
+   end
 ;;
 
 let basic_eval_and_record_ncoercion infos status =