From 590b41b39d52ae1e320bf1c01220b06fadb1ba8d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 24 Sep 2009 12:50:25 +0000 Subject: [PATCH] ncheck works in the current ctx --- helm/software/matita/matitaScript.ml | 8 ++++++-- helm/software/matita/nlibrary/topology/igft.ma | 6 ++++-- 2 files changed, 10 insertions(+), 4 deletions(-) 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): -- 2.39.2