huge commit regarding the grafite_status:

[helm.git] / helm / software / components / grafite_engine / grafiteTypes.mli

diff --git a/helm/software/components/grafite_engine/grafiteTypes.mli b/helm/software/components/grafite_engine/grafiteTypes.mli
index e75c8aa3c565913032cb096127693052380df6c5..c874d43f632cde6e6b44893e32e7df403ea503f0 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteTypes.mli
+++ b/helm/software/components/grafite_engine/grafiteTypes.mli
@@ -44,7 +44,7 @@ type proof_status =
 
 type ng_status =
   | ProofMode of NTacStatus.tac_status
-  | CommandMode of LexiconEngine.status
+  | CommandMode of NEstatus.extra_status
 
 type status = {
   moo_content_rev: GrafiteMarshal.moo;
@@ -73,7 +73,12 @@ val get_proof_metasenv: status ->  Cic.metasenv
 val get_stack: status -> Continuationals.Stack.t
 val get_proof_context : status -> int -> Cic.context
 val get_proof_conclusion : status -> int -> Cic.term
+val get_lexicon : status -> LexiconEngine.status
+val get_estatus : status -> NEstatus.extra_status
+val get_coercions: status -> NCicCoercion.db
 
 val set_stack: Continuationals.Stack.t -> status -> status
 val set_metasenv: Cic.metasenv -> status -> status
+val set_lexicon : LexiconEngine.status -> status -> status
+val set_coercions: NCicCoercion.db -> status -> status