From d46d2dfe4aecc2fa820311753003567d57b19d31 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 7 Feb 2004 18:03:36 +0000 Subject: [PATCH] - Added mk_implicit_sort. - Used in CicRefine.sort_of_prod. --- helm/ocaml/cic_unification/cicMkImplicit.mli | 2 ++ helm/ocaml/cic_unification/cicRefine.ml | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/helm/ocaml/cic_unification/cicMkImplicit.mli b/helm/ocaml/cic_unification/cicMkImplicit.mli index 897367d6c..2ea1100bb 100644 --- a/helm/ocaml/cic_unification/cicMkImplicit.mli +++ b/helm/ocaml/cic_unification/cicMkImplicit.mli @@ -17,6 +17,8 @@ val mk_implicit: Cic.metasenv -> Cic.context -> Cic.metasenv * int (** as above, but the fresh metavariable represents a type *) val mk_implicit_type: Cic.metasenv -> Cic.context -> Cic.metasenv * int +(** as above, but the fresh metavariable represents a sort *) +val mk_implicit_sort: Cic.metasenv -> Cic.metasenv * int (** [mk_implicit metasenv context] create n fresh metavariables *) val n_fresh_metas: diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 42d792d98..338928e8d 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -484,7 +484,7 @@ and type_of_aux' metasenv context t = * likely to know the exact value of the result e.g. if the rhs is a * Sort (Prop | Set | CProp) then the result is the rhs *) let (metasenv,idx) = - CicMkImplicit.mk_implicit metasenv [] in + CicMkImplicit.mk_implicit_sort metasenv in let (subst, metasenv) = CicUnification.fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' -- 2.39.2