From 8b299ba276e095f0fa929a4818d00d253be4c591 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 21 Oct 2009 09:09:14 +0000 Subject: [PATCH] apply the subst to the metasenv and to p --- .../components/grafite_engine/nCicCoercDeclaration.ml | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) 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 -- 2.39.2