]> matita.cs.unibo.it Git - helm.git/commitdiff
No longer puts anonymous declarations in the canonical contexts during
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 5 Feb 2004 14:37:14 +0000 (14:37 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 5 Feb 2004 14:37:14 +0000 (14:37 +0000)
eat_prods.

helm/ocaml/cic_unification/cicRefine.ml

index c9c8f4d8256184569ea8662a2416b3aeaefc74e3..27929645b8cfa8caa17b9fbf19f107f9a723a9d6 100644 (file)
@@ -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
            | 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 =
        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
             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
        let (_, subst, metasenv) = type_of_aux subst metasenv context prod in
        let (subst, metasenv) =
          CicUnification.fo_unif_subst subst context metasenv resty prod