From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 30 Nov 2005 10:59:52 +0000 (+0000)
Subject: Terms parsed by notations were not localized.
X-Git-Tag: make_still_working~8066
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=019d5023aefd04aff9ac0849405306612d54ba64;p=helm.git

Terms parsed by notations were not localized.
---

diff --git a/helm/ocaml/grafite/cicNotation.ml b/helm/ocaml/grafite/cicNotation.ml
index bab8cb97b..30dd5f4d1 100644
--- a/helm/ocaml/grafite/cicNotation.ml
+++ b/helm/ocaml/grafite/cicNotation.ml
@@ -36,7 +36,9 @@ let process_notation st =
       let rule_id =
         if dir <> Some `RightToLeft then
           [ RuleId (CicNotationParser.extend l1 ?precedence ?associativity
-              (fun env loc -> TermContentPres.instantiate_level2 env l2)) ]
+              (fun env loc ->
+                CicNotationPt.AttributedTerm
+                 (`Loc loc,TermContentPres.instantiate_level2 env l2))) ]
         else
           []
       in