From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 28 Jun 2004 11:30:14 +0000 (+0000)
Subject: removed a useless test on explicit substitutions on variables with body
X-Git-Tag: pre_subst_in_kernel~14
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8785bed95dc83a39c76356657d8b21b302b18b12;p=helm.git

removed a useless test on explicit substitutions on variables with body
---

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 140e41712..d36493da6 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1636,6 +1636,7 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^
     | ((uri,t) as subst)::tl ->
        let typeofvar =
         CicSubstitution.subst_vars substs (type_of_variable uri) in
+(* CSC: this test should not exist
        (match CicEnvironment.get_cooked_obj ~trust:false uri with
            Cic.Variable (_,Some bo,_,_) ->
             raise
@@ -1647,6 +1648,7 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^
               ("Unknown variable definition:" ^
               UriManager.string_of_uri uri))
        ) ;
+*)
        let typeoft = type_of_aux context t in
         if CicReduction.are_convertible context typeoft typeofvar then
          check_exp_named_subst_aux (substs@[subst]) tl