No longer puts anonymous declarations in the canonical contexts during

eat_prods.

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index c9c8f4d8256184569ea8662a2416b3aeaefc74e3..27929645b8cfa8caa17b9fbf19f107f9a723a9d6 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -502,7 +502,13 @@ and type_of_aux' metasenv context t =
            | Some t -> Some (CicMetaSubst.lift subst 1 t)
          ) args in
        let argty' = CicMetaSubst.lift subst (List.length args) argty in
-       let context'' = Some (Cic.Anonymous, Cic.Decl argty') :: context' in
+       let name =
+        FreshNamesGenerator.mk_fresh_name
+         (CicMetaSubst.apply_subst_metasenv subst metasenv)
+         (CicMetaSubst.apply_subst_context subst context)
+         Cic.Anonymous
+         (CicMetaSubst.apply_subst subst argty) in
+       let context'' = Some (name, Cic.Decl argty') :: context' in
        let (metasenv, idx) =
         CicMkImplicit.mk_implicit metasenv (context'' @ context) in
        let irl =
@@ -511,14 +517,7 @@ and type_of_aux' metasenv context t =
             context)
        in
        let newmeta = Cic.Meta (idx, irl) in
-       let prod =
-        Cic.Prod
-         (FreshNamesGenerator.mk_fresh_name
-           (CicMetaSubst.apply_subst_metasenv subst metasenv)
-           (CicMetaSubst.apply_subst_context subst context)
-           Cic.Anonymous
-           (CicMetaSubst.apply_subst subst argty),
-          argty, newmeta) in
+       let prod = Cic.Prod (name, argty, newmeta) in
        let (_, subst, metasenv) = type_of_aux subst metasenv context prod in
        let (subst, metasenv) =
          CicUnification.fo_unif_subst subst context metasenv resty prod