fix_left_in_constr still broken, ask enrico

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 1d34d3835697eb42121b9a449e6b79735e3f2e59..739bfa6f92f5e0a4ba6fd46750245400824b2ce5 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -217,6 +217,7 @@ let specialize_inductive_type_constrs ~subst context ty_term =
 ;;
 
 let fix_lefts_in_constrs ~subst r_uri r_len context ty_term =
+  assert false; (* BUG, ask enrico *)
   let _,_,itl,_,i = specialize_inductive_type_constrs ~subst context ty_term in
   let _,_,_,cl = List.nth itl i in  
   let cl =