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 1a94c318599e2678e0898618d1fe40c254653d4b..3bdde5b593426125143aa874e904feb1069d1e4b 100644 (file)
--- 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 02acf9b03f130e28026875538a9574f7574e2875..036ba07a94a6c2fdea4526577741faafd73b6305 100644 (file)
--- 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 *)