The left parameters coming from the constructor types have been refined in a

longer context. Thus we need to unify them in the longer context (that does not
hurt those coming from the inductive types).

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 56ec069d2c77bb7d30eff3773073908bdc01b6ff..8dc94e9e462f689803c44c346adf18f460a417a8 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -746,7 +746,7 @@ let typeof_obj
                       "and those of its inductive type"))))
                    else
                     metasenv,subst,item1::context
-                ) (metasenv,subst,[]) sx_context_ty_rev sx_context_te_rev
+                ) (metasenv,subst,tys) sx_context_ty_rev sx_context_te_rev
               with Invalid_argument "List.fold_left2" -> assert false in
              let con_sort= NCicTypeChecker.typeof ~subst ~metasenv context te in
               (match