From d2ad19f46b30ed0f873635289d89bfe46e04ffb6 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 15 Jun 2006 09:35:47 +0000 Subject: [PATCH] exported 2 functions needed by applyS --- .../components/tactics/primitiveTactics.mli | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/helm/software/components/tactics/primitiveTactics.mli b/helm/software/components/tactics/primitiveTactics.mli index 01d200eb7..c47c9e19a 100644 --- a/helm/software/components/tactics/primitiveTactics.mli +++ b/helm/software/components/tactics/primitiveTactics.mli @@ -23,6 +23,25 @@ * http://cs.unibo.it/helm/. *) +(**** useful only to implement tactics similar to apply ****) + +val generalize_exp_named_subst_with_fresh_metas : + Cic.context -> + int -> + UriManager.uri -> + (UriManager.uri * Cic.term) list -> + int * Cic.metasenv * + Cic.term Cic.explicit_named_substitution * + Cic.term Cic.explicit_named_substitution + +val classify_metas : + Cic.term -> + (Cic.term -> bool) -> + (Cic.context -> Cic.term -> Cic.term) -> + (Cic.term * Cic.context * Cic.term) list -> + (Cic.term * Cic.context * Cic.term) list * + (Cic.term * Cic.context * Cic.term) list + (* ALB, needed by the new paramodulation... *) val apply_tac_verbose_with_subst: term:Cic.term -> ProofEngineTypes.proof * int -> -- 2.39.2