This commit avoids cleaning dummy dependent types in the arities of inductive

types. This is an overkilling solution to the problem of avoiding cleaning
dummy dependent types in the left products in the arities of inductive types.
The left products should be _syntactically_ the same as those of the
constructors. Otherwise, error reporting is incorrect.

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 5aa96944d4e50295cac8094e69210f75e5cff99b..45c2d26eacf619df9aeee3c94ac3f88f6b880981 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -322,7 +322,7 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt
              | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
       | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
 
-and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
+and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
      ugraph
 =
   let rec type_of_aux subst metasenv context t ugraph =
@@ -1745,10 +1745,15 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
     (*  substituted_t,substituted_ty,substituted_metasenv *)
     (* ANDREA: spostare tutta questa robaccia da un altra parte *)
   let cleaned_t =
-    FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
+   if clean_dummy_dependent_types then
+    FreshNamesGenerator.clean_dummy_dependent_types substituted_t
+   else substituted_t in
   let cleaned_ty =
-    FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
+   if clean_dummy_dependent_types then
+    FreshNamesGenerator.clean_dummy_dependent_types substituted_ty
+   else substituted_ty in
   let cleaned_metasenv =
+   if clean_dummy_dependent_types then
     List.map
       (function (n,context,ty) ->
          let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
@@ -1768,6 +1773,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
          in
            (n,context',ty')
       ) substituted_metasenv
+   else
+    substituted_metasenv
   in
     (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1) 
 ;;
@@ -1926,7 +1933,12 @@ let typecheck metasenv uri obj ~localization_tbl =
       List.fold_right
        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
          let ty',_,metasenv,ugraph =
-          type_of_aux' ~localization_tbl metasenv [] ty ugraph
+          (* clean_dummy_dependent_types: false to avoid cleaning the names
+             of the left products, that must be identical to those of the
+             constructors; however, non-left products should probably be
+             cleaned *)
+          type_of_aux' ~clean_dummy_dependent_types:false ~localization_tbl
+           metasenv [] ty ugraph
          in
           metasenv,ugraph,(name,b,ty',cl)::res
        ) tys (metasenv,ugraph,[]) in