From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 24 Sep 2009 12:50:25 +0000 (+0000)
Subject: ncheck works in the current ctx
X-Git-Tag: make_still_working~3439
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=590b41b39d52ae1e320bf1c01220b06fadb1ba8d;p=helm.git

ncheck works in the current ctx
---

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 21450e5e7..e191ee7b3 100644
--- 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
-      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 
-          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
diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index 1cb932184..a4ac5d469 100644
--- 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 
-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 
 
-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):