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 ace3c80a4b3e58be099dcd4fb1bff0cd5d155fb4..95b8f783d745df349fa19ac0da270dea74cb1189 100644 (file)
--- 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) ->