From 97c0a87f5af8ef993075dee9a5aa582d4bdd675b Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Thu, 6 Dec 2012 09:48:53 +0000 Subject: [PATCH] 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. --- matita/components/ng_tactics/nCicElim.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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) -> -- 2.39.2