From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 21 Oct 2009 09:09:14 +0000 (+0000)
Subject: apply the subst to the metasenv and to p
X-Git-Tag: make_still_working~3275
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=8b299ba276e095f0fa929a4818d00d253be4c591;p=helm.git

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 ea112bf4e..fa6b163ad 100644
--- 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