From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 5 Feb 2004 14:37:14 +0000 (+0000)
Subject: No longer puts anonymous declarations in the canonical contexts during
X-Git-Tag: V_0_2_3~41
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a8c20c4385d6045b848d21af9f30fc583de2aaa2;p=helm.git

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 c9c8f4d82..27929645b 100644
--- 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