Terms parsed by notations were not localized.

diff --git a/helm/ocaml/grafite/cicNotation.ml b/helm/ocaml/grafite/cicNotation.ml
index bab8cb97bb5b72a49101512d23bd04e4661ab7df..30dd5f4d191d3cdc071f50fb855c92ac9f96d04c 100644 (file)
--- 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