From 8785bed95dc83a39c76356657d8b21b302b18b12 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 28 Jun 2004 11:30:14 +0000 Subject: [PATCH] removed a useless test on explicit substitutions on variables with body --- helm/ocaml/cic_proof_checking/cicTypeChecker.ml | 2 ++ 1 file changed, 2 insertions(+) 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 -- 2.39.2