From a785a3526d4dcbb6c5810ed4fb943132c9ff2d45 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 29 Nov 2004 12:22:23 +0000 Subject: [PATCH] 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 --- helm/ocaml/cic_unification/freshNamesGenerator.ml | 4 ++-- helm/ocaml/cic_unification/freshNamesGenerator.mli | 3 ++- 2 files changed, 4 insertions(+), 3 deletions(-) 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 *) -- 2.39.2