ported to typed explicit subst

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 7b3e4179c47b77f65d2939d5fead0e2bea3914f9..dd510797ab3081370ad3e7efb60e3802e9381099 100644 (file)
--- 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 =