apply the subst to the metasenv and to p

diff --git a/helm/software/components/grafite_engine/nCicCoercDeclaration.ml b/helm/software/components/grafite_engine/nCicCoercDeclaration.ml
index ea112bf4ebb16deb048be05402c2b91f2221b24d..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