X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fequality.mli;h=d3acf8950c6b5cff5225dcf4eb395f3eba06edc7;hb=152966d146348c74302df64e12c7644c00eb447e;hp=bd3d4c2acda6de7212d31697b3ebc18da189a5e3;hpb=041ad23b567b9844ec187ad436595868441802f4;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/equality.mli b/helm/software/components/tactics/paramodulation/equality.mli index bd3d4c2ac..d3acf8950 100644 --- a/helm/software/components/tactics/paramodulation/equality.mli +++ b/helm/software/components/tactics/paramodulation/equality.mli @@ -25,6 +25,8 @@ type rule = SuperpositionRight | SuperpositionLeft | Demodulation +(* every equality group has its own bag. the bag contains the infos necessary + * for building the proof. FIXME: should also contain maxmeta! *) type equality_bag val mk_equality_bag: unit -> equality_bag @@ -44,7 +46,21 @@ val pp_proof: (Cic.name option) list -> goal_proof -> proof -> Subst.substitution -> int -> Cic.term -> string +val draw_proof: + equality_bag -> + (Cic.name option) list -> goal_proof -> proof -> int -> unit + val pp_proofterm: Cic.term -> string + +val mk_eq_ind : + UriManager.uri -> + Cic.term -> + Cic.term -> + Cic.term -> + Cic.term -> + Cic.term -> + Cic.term -> + Cic.term val mk_equality : equality_bag -> int * proof * @@ -74,6 +90,8 @@ val string_of_proof : (* build_goal_proof [eq_URI] [goal_proof] [initial_proof] [ty] * [ty] is the type of the goal *) val build_goal_proof: + ?contextualize:bool -> + ?forward:bool -> equality_bag -> UriManager.uri -> goal_proof -> proof -> Cic.term-> int list -> Cic.context -> Cic.metasenv -> @@ -110,6 +128,8 @@ val meta_convertibility: Cic.term -> Cic.term -> bool (** meta convertibility between two equations *) val meta_convertibility_eq: equality -> equality -> bool +val meta_convertibility_subst: + Cic.term -> Cic.term -> Cic.metasenv -> Cic.substitution option val is_weak_identity: equality -> bool val is_identity: Utils.environment -> equality -> bool