From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 22 Oct 2004 12:18:22 +0000 (+0000)
Subject: ported to typed explicit subst
X-Git-Tag: V_0_0_10~43
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3e30c3516dbb98a0629eb0205085f3b79abe1469;p=helm.git

ported to typed explicit subst
---

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 7b3e4179c..dd510797a 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -159,12 +159,15 @@ and type_of_aux' metasenv context t =
        ty,subst',metasenv'
     | C.Meta (n,l) -> 
         (try
-          let (canonical_context, term) = CicUtil.lookup_subst n subst in
+          let (canonical_context, term,ty) = CicUtil.lookup_subst n subst in
           let subst,metasenv =
             check_metasenv_consistency n subst metasenv context
               canonical_context l
           in
-          type_of_aux subst metasenv context (CicSubstitution.lift_meta l term)
+          (* trust or check ??? *)
+          CicSubstitution.lift_meta l ty, subst, metasenv
+          (* type_of_aux subst metasenv 
+	     context (CicSubstitution.lift_meta l term) *)
         with CicUtil.Subst_not_found _ ->
           let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
           let subst,metasenv =