From: Wilmer Ricciotti Date: Thu, 6 Dec 2012 09:48:53 +0000 (+0000) Subject: Fixes a bug in NCicElim.pp (term -> ast conversion used when building X-Git-Tag: make_still_working~1412 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=97c0a87f5af8ef993075dee9a5aa582d4bdd675b;p=helm.git Fixes a bug in NCicElim.pp (term -> ast conversion used when building projections) that was swapping arguments in a let-in, causing projection generation to fail for any record field containing a let-in expression. --- diff --git a/matita/components/ng_tactics/nCicElim.ml b/matita/components/ng_tactics/nCicElim.ml index ace3c80a4..95b8f783d 100644 --- a/matita/components/ng_tactics/nCicElim.ml +++ b/matita/components/ng_tactics/nCicElim.ml @@ -236,7 +236,7 @@ let pp (status: #NCic.status) = | NCic.Lambda (n,s,t) -> let n = mk_id n in NotationPt.Binder (`Lambda, (n,Some (pp rels s)), pp (n::rels) t) - | NCic.LetIn (n,s,ty,t) -> + | NCic.LetIn (n,ty,s,t) -> let n = mk_id n in NotationPt.LetIn ((n, Some (pp rels ty)), pp rels s, pp (n::rels) t) | NCic.Match (NReference.Ref (uri,_) as r,outty,te,patterns) ->