From 56cd805f6f2e277b60fdce8f039f27bb0767e838 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 8 Apr 2008 15:25:46 +0000 Subject: [PATCH] Bad alpha-conversion by Enrico fixed. --- helm/software/components/cic_proof_checking/cicTypeChecker.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 -- 2.39.2