From: Claudio Sacerdoti Coen Date: Sat, 7 Feb 2004 18:01:53 +0000 (+0000) Subject: Added mk_implicit_sort. X-Git-Tag: V_0_2_3~6 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=18b06d9551f845a8323937403fe0c99e52ce7be5;p=helm.git Added mk_implicit_sort. --- diff --git a/helm/ocaml/cic_unification/cicMkImplicit.ml b/helm/ocaml/cic_unification/cicMkImplicit.ml index fc429b381..f433fb19b 100644 --- a/helm/ocaml/cic_unification/cicMkImplicit.ml +++ b/helm/ocaml/cic_unification/cicMkImplicit.ml @@ -33,6 +33,16 @@ let mk_implicit metasenv context = newmeta + 2, context, Cic.Meta (newmeta + 1,irl) ] @ metasenv, newmeta + 2) +let mk_implicit_type metasenv context = + let newmeta = new_meta metasenv in + ([ newmeta, [], Cic.Sort Cic.Type ; + newmeta + 1, context, Cic.Meta (newmeta, []) ] @metasenv, + newmeta + 1) + +let mk_implicit_sort metasenv = + let newmeta = new_meta metasenv in + ([ newmeta, [], Cic.Sort Cic.Type] @ metasenv, newmeta) + let n_fresh_metas metasenv context n = if n = 0 then metasenv, [] else @@ -61,12 +71,6 @@ let fresh_subst metasenv context uris = (uri,Cic.Meta(newmeta+2,irl))::l in aux newmeta uris -let mk_implicit_type metasenv context = - let newmeta = new_meta metasenv in - ([ newmeta, [], Cic.Sort Cic.Type ; - newmeta + 1, context, Cic.Meta (newmeta, []) ] @metasenv, - newmeta + 1) - let expand_implicits metasenv context term = let rec aux metasenv context = function | (Cic.Rel _) as t -> metasenv, t diff --git a/helm/ocaml/cic_unification/cicMkImplicit.mli b/helm/ocaml/cic_unification/cicMkImplicit.mli index 2f8710390..897367d6c 100644 --- a/helm/ocaml/cic_unification/cicMkImplicit.mli +++ b/helm/ocaml/cic_unification/cicMkImplicit.mli @@ -14,6 +14,10 @@ val new_meta : Cic.metasenv -> int * @return the new metasenv and the index of the added conjecture *) 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 + + (** [mk_implicit metasenv context] create n fresh metavariables *) val n_fresh_metas: Cic.metasenv -> Cic.context -> int -> Cic.metasenv * Cic.term list @@ -26,9 +30,6 @@ val fresh_subst: UriManager.uri list -> Cic.metasenv * (Cic.term Cic.explicit_named_substitution) -(** as above, but the fresh metavariable represents a type *) -val mk_implicit_type: Cic.metasenv -> Cic.context -> Cic.metasenv * int - val expand_implicits: Cic.metasenv -> Cic.context -> Cic.term -> Cic.metasenv * Cic.term