include statement better implemented:

[helm.git] / helm / software / components / lexicon / cicNotation.ml

diff --git a/helm/software/components/lexicon/cicNotation.ml b/helm/software/components/lexicon/cicNotation.ml
index 248e08bcb242c7ada134c5e5325eae86814e2062..32cb3f6382cf327b89d01476312d1d7c953f0a6b 100644 (file)
--- a/helm/software/components/lexicon/cicNotation.ml
+++ b/helm/software/components/lexicon/cicNotation.ml
@@ -106,7 +106,14 @@ let set_active_notations ids =
   in
   TermAcicContent.set_active_interpretations interp_ids
 
-let reset () =
-  TermContentPres.reset ();
-  TermAcicContent.reset ()
+let push () =
+ TermContentPres.push ();
+ TermAcicContent.push ();
+ CicNotationParser.push ()
+;;
+
+let pop () =
+ TermContentPres.pop ();
+ TermAcicContent.pop ();
+ CicNotationParser.pop ()
 ;;