...

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 634ccc769129e5157564d49fd96fda33be3f88ce..09eb2d34514011de6e606ca1c57d9adbd3021868 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -715,9 +715,9 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
      prerr_endline ("nuovo lemma: " ^ NCicPp.ppmetasenv ~subst:nsubst nmenv);
      { status with
         GrafiteTypes.ng_status = 
-           GrafiteTypes.ProofMode { NTactics.gstatus = ninitial_stack; 
+           GrafiteTypes.ProofMode { NTacStatus.gstatus = ninitial_stack; 
           istatus = { 
-            NTactics.pstatus = 
+            NTacStatus.pstatus = 
              NUri.uri_of_string suri, 0, nmenv, nsubst, 
               (NCic.Constant ([],"",Some nbo,nty,(`Provided,`Definition,`Regular)));
             lstatus = nlexicon_status} }   
@@ -820,7 +820,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
       | GrafiteTypes.ProofMode nstatus ->
          let nstatus = eval_ng_tac (text,prefix_len,tac) nstatus in
          let nstatus = eval_ng_punct (text,prefix_len,punct) nstatus in
-         NTactics.pp_tac_status nstatus;
+         NTacStatus.pp_tac_status nstatus;
          { status with GrafiteTypes.ng_status = GrafiteTypes.ProofMode nstatus }, [])
   | GrafiteAst.NonPunctuationTactical (_, tac, punct) ->
      let status = 

diff --git a/helm/software/components/grafite_engine/grafiteTypes.ml b/helm/software/components/grafite_engine/grafiteTypes.ml
index 83687277965aaa500c390d4fa406efc208045bc2..fc81efcaf29bbffe8fc428799a135c62d900a304 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteTypes.ml
+++ b/helm/software/components/grafite_engine/grafiteTypes.ml
@@ -45,7 +45,7 @@ type proof_status =
       * engine. No status entering/exiting the engine could be in it. *)
 
 type ng_status =
-  | ProofMode of NTactics.tac_status
+  | ProofMode of NTacStatus.tac_status
   | CommandMode of LexiconEngine.status
 
 type status = {

diff --git a/helm/software/components/grafite_engine/grafiteTypes.mli b/helm/software/components/grafite_engine/grafiteTypes.mli
index b159a7fe6b2caf260c3e39256da7672de25d53c6..22386ebbf9b8a2c0a2753f6d7a400d30e29d2ff6 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteTypes.mli
+++ b/helm/software/components/grafite_engine/grafiteTypes.mli
@@ -43,7 +43,7 @@ type proof_status =
   | Intermediate of Cic.metasenv
 
 type ng_status =
-  | ProofMode of NTactics.tac_status
+  | ProofMode of NTacStatus.tac_status
   | CommandMode of LexiconEngine.status
 
 type status = {

diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli
index 4ca302890808c584c32bfcef9cc810700ca7396e..1feac415baec232ebd9fdeeeb6fbc031156de2fd 100644 (file)
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -65,4 +65,6 @@ val select_term:
   lowtac_status -> cic_term -> ast_term option * NCic.term ->
     lowtac_status * cic_term
 
+val pp_tac_status: tac_status -> unit
+
 (* end *)

diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml
index 128f33ac359f12ce0ad7477e55adae06cf9d9003..75c3ebafc5d946b3540157992874b14853c14283 100644 (file)
--- a/helm/software/matita/matitaEngine.ml
+++ b/helm/software/matita/matitaEngine.ml
@@ -73,7 +73,7 @@ let eval_ast ?do_heavy_checks lexicon_status
    | GrafiteTypes.ProofMode s -> 
       { grafite_status with GrafiteTypes.ng_status = 
          GrafiteTypes.ProofMode 
-          { s with NTactics.istatus = { s.NTactics.istatus with NTactics.lstatus =  lexicon_status }}}
+          { s with NTacStatus.istatus = { s.NTacStatus.istatus with NTacStatus.lstatus =  lexicon_status }}}
  in
  let new_grafite_status,new_objs =
   GrafiteEngine.eval_ast
@@ -87,7 +87,7 @@ let eval_ast ?do_heavy_checks lexicon_status
   else
    match new_grafite_status.GrafiteTypes.ng_status with
    | GrafiteTypes.CommandMode l -> l
-   | GrafiteTypes.ProofMode s -> s.NTactics.istatus.NTactics.lstatus
+   | GrafiteTypes.ProofMode s -> s.NTacStatus.istatus.NTacStatus.lstatus
  in
  let new_lexicon_status =
   LexiconSync.add_aliases_for_objs lexicon_status new_objs in

diff --git a/helm/software/matita/matitaExcPp.ml b/helm/software/matita/matitaExcPp.ml
index df4c70ded2498d7fdefaea7f8a1acd176a2bce55..2d6d1cd17187b0c5928bbb67b4c7b0f668b883a4 100644 (file)
--- a/helm/software/matita/matitaExcPp.ml
+++ b/helm/software/matita/matitaExcPp.ml
@@ -163,6 +163,8 @@ let rec to_string =
      None, ("Disambiguation choice not found: " ^ Lazy.force msg)
   | MatitaEngine.EnrichedWithLexiconStatus (exn,_) ->
      None, "EnrichedWithLexiconStatus "^snd(to_string exn)
+  | NTacStatus.Error msg ->
+     None, "NTactic error: " ^ Lazy.force msg
   | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
      let loc =
       match errorll with