]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/lexicon/lexiconSync.ml
disambiguation even more abstracted
[helm.git] / helm / software / components / lexicon / lexiconSync.ml
index b9c9b1cc2c43a77198fd1240e7d114f6a1407b24..ed243fe196c48a9ff5e7499f7bdce28ed91e0432 100644 (file)
@@ -109,3 +109,5 @@ let time_travel ~present ~past =
   in
    List.iter CicNotation.remove_notation notation_to_remove
 
+let push () = CicNotation.push ();;
+let pop () = CicNotation.pop ();;