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 d5270c192c1191e4b1926b8ce2484a2758530237..c52ab7e62a90002776f77b312e4d6e91d5ffd179 100644 (file)
--- 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