From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 29 Jun 2005 08:46:40 +0000 (+0000)
Subject: Stupid bug fixed in the refinement of let ... in
X-Git-Tag: INDEXING_NO_PROOFS~13
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9122d57540613905332e31ec0d6539f30cf4e240;p=helm.git

Stupid bug fixed in the refinement of let ... in
---

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