From 99264b3a8247ca0e692bcbdb63087ce35e294e6b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 3 Feb 2004 15:43:24 +0000 Subject: [PATCH] cic_mkimplicit' removed (its implementation was wrong and the function is not really used) --- helm/ocaml/cic_unification/cicMkImplicit.ml | 9 +++------ helm/ocaml/cic_unification/cicMkImplicit.mli | 4 ---- 2 files changed, 3 insertions(+), 10 deletions(-) diff --git a/helm/ocaml/cic_unification/cicMkImplicit.ml b/helm/ocaml/cic_unification/cicMkImplicit.ml index 9db792546..672c90cd8 100644 --- a/helm/ocaml/cic_unification/cicMkImplicit.ml +++ b/helm/ocaml/cic_unification/cicMkImplicit.ml @@ -61,10 +61,6 @@ let fresh_subst metasenv context uris = (uri,Cic.Meta(newmeta+2,irl))::l in aux newmeta uris -let mk_implicit' metasenv context = - let (metasenv, index) = mk_implicit metasenv context in - (metasenv, index - 1, index) - let mk_implicit_type metasenv context = let newmeta = new_meta metasenv in let irl = identity_relocation_list_for_metavariable context in @@ -92,9 +88,9 @@ let expand_implicits metasenv context term = let metasenv', l' = do_local_context metasenv context l in metasenv', Cic.Meta (n, l') | Cic.Implicit -> - let (metasenv', type_index, _) = mk_implicit' metasenv context in + let (metasenv', idx) = mk_implicit metasenv context in let irl = identity_relocation_list_for_metavariable context in - metasenv', Cic.Meta (type_index, irl) + metasenv', Cic.Meta (idx, irl) | Cic.Cast (te, ty) -> let metasenv', ty' = aux metasenv context ty in let metasenv'', te' = aux metasenv' context te in @@ -146,6 +142,7 @@ let expand_implicits metasenv context term = List.fold_right (fun (name, _, typ, _) (metasenv, types) -> let new_metasenv, new_type = aux metasenv context typ in +prerr_endline ("UH? " ^ CicPp.ppterm typ ^ " ==> " ^ CicPp.ppterm new_type) ; (new_metasenv, (name, new_type) :: types)) funs (metasenv, []) in diff --git a/helm/ocaml/cic_unification/cicMkImplicit.mli b/helm/ocaml/cic_unification/cicMkImplicit.mli index 6d9179d8e..2f8710390 100644 --- a/helm/ocaml/cic_unification/cicMkImplicit.mli +++ b/helm/ocaml/cic_unification/cicMkImplicit.mli @@ -26,10 +26,6 @@ val fresh_subst: UriManager.uri list -> Cic.metasenv * (Cic.term Cic.explicit_named_substitution) -(** as above but return both the index of the added conjecture (2nd index) and - * the index of its type (1st index) *) -val mk_implicit': Cic.metasenv -> Cic.context -> Cic.metasenv * int * int - (** as above, but the fresh metavariable represents a type *) val mk_implicit_type: Cic.metasenv -> Cic.context -> Cic.metasenv * int -- 2.39.2