X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.ml;h=414d0b976a316f9168d8aaca09d9035d3eef352a;hb=a7ab0ef67114c3152920f03ae1d7bfaaf1fae290;hp=5715778fb07cd91ba54ce9cc1ca5b180374fb4fc;hpb=cf5d6fab96c47ccb7d623d72742717d9b08bae7b;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 5715778fb..414d0b976 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1330,19 +1330,9 @@ and check_metasenv_consistency ?(subst=[]) metasenv context canonical_context l
              let type_t = type_of_aux' ~subst metasenv context t in
              if not (R.are_convertible ~subst ~metasenv context type_t ct) then
 	       (* debug *)
-	       (
-                 (*
-		 (match type_t with 
-		     Cic.Meta (n,l) ->
-		       try 
-			 let (cc, ecco) = CicUtil.lookup_subst n subst in
-			 prerr_endline (CicPp.ppterm ecco)
-		       with CicUtil.Subst_not_found _ ->
-                         prerr_endline "Non lo trovo"
-		    | _ -> ()); *)
               raise (TypeCheckerFailure (sprintf
                 "Not well typed metavariable local context: expected a term of type %s, found %s of type %s"
-                (CicPp.ppterm ct) (CicPp.ppterm t) (CicPp.ppterm type_t))))
+                (CicPp.ppterm ct) (CicPp.ppterm t) (CicPp.ppterm type_t)))
          | None, _  ->
              raise (TypeCheckerFailure
               "Not well typed metavariable local context: an hypothesis, that is not hidden, is not instantiated")
@@ -1379,15 +1369,17 @@ and type_of_aux' ?(subst = []) metasenv context t =
        ty
     | 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
           check_metasenv_consistency 
 	    ~subst metasenv context canonical_context l;
-          type_of_aux context (CicSubstitution.lift_meta l term)
+          (* assuming subst is well typed !!!!! *)
+          CicSubstitution.lift_meta l ty
+          (* type_of_aux context (CicSubstitution.lift_meta l term) *)
 	with CicUtil.Subst_not_found _ ->
 	  let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
-            check_metasenv_consistency 
-	      ~subst metasenv context canonical_context l;
-            CicSubstitution.lift_meta l ty)
+          check_metasenv_consistency 
+	     ~subst metasenv context canonical_context l;
+          CicSubstitution.lift_meta l ty)
       (* TASSI: CONSTRAINTS *)
     | C.Sort (C.Type t) -> 
        let t' = CicUniv.fresh() in