From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 29 Nov 2004 12:22:23 +0000 (+0000)
Subject: bugfix: FreshNameGenerator uses the type checker on mk_fresh_name
X-Git-Tag: PRE_UNIVERSES~8
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a785a3526d4dcbb6c5810ed4fb943132c9ff2d45;p=helm.git

bugfix: FreshNameGenerator uses the type checker on mk_fresh_name
invocation, thus it should receive in input a subst to be passed to the
type checker in order to avoid "unknown" Metas in the term to be type
checked
---

diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.ml b/helm/ocaml/cic_unification/freshNamesGenerator.ml
index 1a94c3185..3bdde5b59 100644
--- a/helm/ocaml/cic_unification/freshNamesGenerator.ml
+++ b/helm/ocaml/cic_unification/freshNamesGenerator.ml
@@ -27,14 +27,14 @@
 (* returns an identifier which is fresh in the context *)
 (* and that resembles [name] as much as possible.      *)
 (* [typ] will be the type of the variable              *)
-let mk_fresh_name metasenv context name ~typ =
+let mk_fresh_name ~subst metasenv context name ~typ =
  let module C = Cic in
   let basename =
    match name with
       C.Anonymous ->
        (*CSC: great space for improvements here *)
        (try
-         (match CicTypeChecker.type_of_aux' metasenv context typ with
+         (match CicTypeChecker.type_of_aux' ~subst metasenv context typ with
              C.Sort C.Prop
            | C.Sort C.CProp -> "H"
            | C.Sort C.Set -> "x"
diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.mli b/helm/ocaml/cic_unification/freshNamesGenerator.mli
index 02acf9b03..036ba07a9 100644
--- a/helm/ocaml/cic_unification/freshNamesGenerator.mli
+++ b/helm/ocaml/cic_unification/freshNamesGenerator.mli
@@ -28,7 +28,8 @@
 (* and that resembles [name] as much as possible.      *)
 (* [typ] will be the type of the variable              *)
 val mk_fresh_name :
- Cic.metasenv -> Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
+  subst:Cic.substitution ->
+  Cic.metasenv -> Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
 
 (* clean_dummy_dependent_types term                               *)
 (* returns a copy of [term] where every dummy dependent product *)