From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 8 May 2009 18:05:00 +0000 (+0000)
Subject: Bug fixed in refinement of inductive types: left parameters were forgot
X-Git-Tag: make_still_working~4006
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1663463fa855cce28e7db1989d9536715b49bf5a;p=helm.git

Bug fixed in refinement of inductive types: left parameters were forgot
during reconstruction of refined object.
---

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index d5270c192..c52ab7e62 100644
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -702,14 +702,26 @@ let typeof_obj hdb
                     (lazy (localise te,
                       "Non positive occurence in " ^ NUri.string_of_uri uri)))
               else
+               let relsno = List.length itl + leftno in
                let te = 
                  NCicSubstitution.psubst 
-                  (fun i -> NCic.Const (NReference.reference_of_spec uri
-                     (NReference.Ind (ind,i,leftno))))
-                  (List.rev (HExtlib.list_seq 0 (List.length itl)))
-                   te 
-               in      
-               metasenv,subst,(k_relev,n,te)::res
+                  (fun i ->
+                    if i <= leftno  then
+                     NCic.Rel i
+                    else
+                     NCic.Const (NReference.reference_of_spec uri
+                      (NReference.Ind (ind,relsno - i,leftno))))
+                  (HExtlib.list_seq 1 (relsno+1))
+                   te in
+               let te =
+                List.fold_right
+                 (fun (name,decl) te ->
+                   match decl with
+                      NCic.Decl ty -> NCic.Prod (name,ty,te)
+                    | NCic.Def (bo,ty) -> NCic.LetIn (name,ty,bo,te)
+                 ) sx_context_te_rev te
+               in
+                metasenv,subst,(k_relev,n,te)::res
               ) cl (metasenv,subst,[])
          in
           metasenv,subst,(it_relev,n,ty,cl)::res,i+1