the tactic now returns as open goals the open metas in the proof

[helm.git] / helm / software / components / tactics / paramodulation / inference.mli

diff --git a/helm/software/components/tactics/paramodulation/inference.mli b/helm/software/components/tactics/paramodulation/inference.mli
index 5fdf694fc01f4d4777820e979a418891602af593..b08054ca4f2c90c72dc97ade2d53e493b8ed0260 100644 (file)
--- a/helm/software/components/tactics/paramodulation/inference.mli
+++ b/helm/software/components/tactics/paramodulation/inference.mli
@@ -25,6 +25,9 @@
 
 val metas_of_proof_time : float ref
 
+(* type substitution = Cic.substitution *)
+type substitution = (int * Cic.term) list 
+
 type equality =
     int *                (* weight *)
     proof *              (* proof *)
@@ -32,14 +35,13 @@ type equality =
      Cic.term *          (* left side *)
      Cic.term *          (* right side *)
      Utils.comparison) * (* ordering *)  
-    Cic.metasenv *       (* environment for metas *)
-    Cic.term list        (* arguments *)
+    Cic.metasenv        (* environment for metas *)
 
 and proof =
   | NoProof   (* no proof *)
-  | BasicProof of Cic.term (* already a proof of a goal *)
+  | BasicProof of substitution * Cic.term (* already a proof of a goal *)
   | ProofBlock of (* proof of a rewrite step *)
-      Cic.substitution * UriManager.uri * (* eq_ind or eq_ind_r *)
+      substitution * UriManager.uri * (* eq_ind or eq_ind_r *)
         (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * proof
   | ProofGoalBlock of proof * proof
       (* proof of the new meta, proof of the goal from which this comes *)
@@ -54,7 +56,7 @@ val build_proof_term: ?noproof:Cic.term -> proof -> Cic.term
 
 val string_of_proof: proof -> string
 
-val filter : Cic.substitution -> Cic.metasenv -> Cic.metasenv
+val filter : substitution -> Cic.metasenv -> Cic.metasenv
 
 exception MatchingFailure
 
@@ -62,7 +64,7 @@ exception MatchingFailure
 val matching:
   Cic.metasenv -> Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
   CicUniv.universe_graph ->
-  Cic.substitution * Cic.metasenv * CicUniv.universe_graph
+  substitution * Cic.metasenv * CicUniv.universe_graph
 
 (**
    special unification that checks if the two terms are "simple", and in
@@ -71,7 +73,7 @@ val matching:
 val unification:
   Cic.metasenv -> Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
   CicUniv.universe_graph ->
-  Cic.substitution * Cic.metasenv * CicUniv.universe_graph
+  substitution * Cic.metasenv * CicUniv.universe_graph
 
     
 (**
@@ -132,8 +134,13 @@ val is_identity: environment -> equality -> bool
 
 val string_of_equality: ?env:environment -> equality -> string
 
+
 val metas_of_term: Cic.term -> int list
 val metas_of_proof: proof -> int list
 
 (** ensures that metavariables in equality are unique *)
 val fix_metas: int -> equality -> int * equality
+
+val apply_subst: substitution -> Cic.term -> Cic.term
+val apply_subst_metasenv: substitution -> Cic.metasenv -> Cic.metasenv
+val ppsubst: substitution -> string