From: Claudio Sacerdoti Coen Date: Tue, 8 Apr 2008 15:25:46 +0000 (+0000) Subject: Bad alpha-conversion by Enrico fixed. X-Git-Tag: make_still_working~5405 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=inline;h=56cd805f6f2e277b60fdce8f039f27bb0767e838;p=helm.git Bad alpha-conversion by Enrico fixed. --- diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index ab43c3732..d34c82919 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -2003,7 +2003,7 @@ end; let (_,ty,_) = List.nth fl i in ty,ugraph2 - and check_exp_named_subst ~logger ~subst context ugraph = + and check_exp_named_subst ~logger ~subst context = let rec check_exp_named_subst_aux ~logger esubsts l ugraph = match l with [] -> ugraph @@ -2029,7 +2029,7 @@ end; raise (TypeCheckerFailure (lazy "Wrong Explicit Named Substitution")) end in - check_exp_named_subst_aux ~logger [] ugraph + check_exp_named_subst_aux ~logger [] and sort_of_prod ~subst context (name,s) (t1, t2) ugraph = let module C = Cic in