ncheck works in the current ctx

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 21450e5e796e7d74c8f7549e156f079799e80646..e191ee7b31d6c09a01795c2b824297c0dfb534e3 100644 (file)
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -377,10 +377,14 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us
        [status, parsed_text], "", parsed_text_length
   | TA.NCheck (_,t) ->
       let status = script#grafite_status in
        [status, parsed_text], "", parsed_text_length
   | TA.NCheck (_,t) ->
       let status = script#grafite_status in

-      let ctx = [] in
+      let _,_,menv,subst,_ = status#obj in
+      let ctx = 
+        try let _,(_,ctx,_) = List.hd menv in ctx
+        with Failure "hd" -> []
+      in

       let m, s, status, t = 
         GrafiteDisambiguate.disambiguate_nterm 
       let m, s, status, t = 
         GrafiteDisambiguate.disambiguate_nterm 

-          None status [] [] ctx (parsed_text,parsed_text_length,
+          None status ctx menv subst (parsed_text,parsed_text_length,

             CicNotationPt.Cast (t,CicNotationPt.Implicit `JustOne))  
           (* XXX use the metasenv, if possible *)
       in
             CicNotationPt.Cast (t,CicNotationPt.Implicit `JustOne))  
           (* XXX use the metasenv, if possible *)
       in

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index 1cb932184a64e9fc03d69969a52865a18e0018c1..a4ac5d46914340de617c304a9b3d40937c53113a 100644 (file)
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -16,14 +16,16 @@ The tutorial spends a considerable amount of effort in defining
 notations that resemble the ones used in the original paper. We believe
 this a important part of every formalization, not only for the estetic 
 point of view, but also from the practical point of view. Being 
 notations that resemble the ones used in the original paper. We believe
 this a important part of every formalization, not only for the estetic 
 point of view, but also from the practical point of view. Being 

-consistent allows to follow the paper in a pedantic way. 
+consistent allows to follow the paper in a pedantic way, and hopefully
+to make the formalization (at least the definitions and proved
+statements) readable to the author of the paper. 

 
 Orientering
 -----------
 
 TODO 
 
 
 Orientering
 -----------
 
 TODO 
 

-buttons, PG-interaction-model, sequent window, script window
+buttons, PG-interaction-model, sequent window, script window, ncheck

 
 The library, inclusion of `sets/sets.ma`, notation defined: Ω^A.
 Symbols (see menu: View ▹ TeX/UTF-8 Table):
 
 The library, inclusion of `sets/sets.ma`, notation defined: Ω^A.
 Symbols (see menu: View ▹ TeX/UTF-8 Table):