From 9122d57540613905332e31ec0d6539f30cf4e240 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 29 Jun 2005 08:46:40 +0000 Subject: [PATCH] Stupid bug fixed in the refinement of let ... in --- helm/ocaml/cic_unification/cicRefine.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index f30e3c53c..5c031f473 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -287,7 +287,7 @@ and type_of_aux' metasenv context t ugraph = * Moreover the inferred type is closer to the expected one. *) C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty, - subst',metasenv',ugraph2 + subst'',metasenv'',ugraph2 | C.Appl (he::((_::_) as tl)) -> let he',hetype,subst',metasenv',ugraph1 = type_of_aux subst metasenv context he ugraph -- 2.39.5