Many improvements in tactics (and tactical) representation:

[helm.git] / helm / gTopLevel / primitiveTactics.mli

diff --git a/helm/gTopLevel/primitiveTactics.mli b/helm/gTopLevel/primitiveTactics.mli
index 87142b564291264f8d8d0be2e5339df1059fa5f0..123b3859df099adad8c26ce7ca1af9286c442edd 100644 (file)
--- a/helm/gTopLevel/primitiveTactics.mli
+++ b/helm/gTopLevel/primitiveTactics.mli
@@ -1,13 +1,13 @@
 val apply_tac:
-  status: ProofEngineTypes.status -> term: Cic.term -> ProofEngineTypes.status
+  term: Cic.term -> ProofEngineTypes.tactic
 val exact_tac:
-  status: ProofEngineTypes.status -> term: Cic.term -> ProofEngineTypes.status
+  term: Cic.term -> ProofEngineTypes.tactic
 val intros_tac:
-  status: ProofEngineTypes.status -> name: string-> ProofEngineTypes.status
+  name: string -> ProofEngineTypes.tactic
 val cut_tac:
-  status: ProofEngineTypes.status -> term: Cic.term -> ProofEngineTypes.status
+  term: Cic.term -> ProofEngineTypes.tactic 
 val letin_tac:
-  status: ProofEngineTypes.status -> term: Cic.term -> ProofEngineTypes.status
+  term: Cic.term -> ProofEngineTypes.tactic 
 
 val elim_intros_simpl_tac:
-  status: ProofEngineTypes.status -> term: Cic.term -> ProofEngineTypes.status
+  term: Cic.term -> ProofEngineTypes.tactic