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 140e4171287a73a4b1164f857306f31368bb2806..d36493da616ea233b992ad3477c2b53b50e9ca1a 100644 (file)
--- 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