From: Wilmer Ricciotti <ricciott@cs.unibo.it>
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) ->