From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Wed, 15 Jul 2015 10:36:12 +0200
Subject: Imported Upstream version 8.5~beta2+dfsg

---
 dev/TODO            | 22 ----------------------
 dev/nsis/coq.nsi    |  4 +---
 dev/top_printers.ml |  5 ++---
 3 files changed, 3 insertions(+), 28 deletions(-)
 delete mode 100644 dev/TODO

(limited to 'dev')

diff --git a/dev/TODO b/dev/TODO
deleted file mode 100644
index e62ee6e5..00000000
--- a/dev/TODO
+++ /dev/null
@@ -1,22 +0,0 @@
-
- o options de la ligne de commande
-     - reporter les options de l'ancien script coqtop sur le nouveau coqtop.ml
-
- o arguments implicites
-     - les calculer une fois pour toutes à la déclaration (dans Declare)
-       et stocker cette information dans le in_variable, in_constant, etc.
-
- o Environnements compilés (type Environ.compiled_env)
-     - pas de timestamp mais plutôt un checksum avec Digest (mais comment ?)
-
- o Efficacité
-     - utiliser DOPL plutôt que DOPN (sauf pour Case)
-     - batch mode => pas de undo, ni de reset
-     - conversion : déplier la constante la plus récente
-     - un cache pour type_of_const, type_of_inductive, type_of_constructor,
-       lookup_mind_specif
-
- o Toplevel
-     - parsing de la ligne de commande : utiliser Arg ???
-
-
diff --git a/dev/nsis/coq.nsi b/dev/nsis/coq.nsi
index 90e3fdaa..5b421e49 100755
--- a/dev/nsis/coq.nsi
+++ b/dev/nsis/coq.nsi
@@ -196,14 +196,12 @@ SectionEnd
 
 Section "Uninstall"
 
-;; We keep the settings 
-;; Delete "$INSTDIR\config\coqide-gtk2rc"
- 
   RMDir /r "$INSTDIR\bin"
   RMDir /r "$INSTDIR\dev"
   RMDir /r "$INSTDIR\etc"
   RMDir /r "$INSTDIR\lib"
   RMDir /r "$INSTDIR\share"
+  RMDir /r "$INSTDIR\ide"
 
   Delete "$INSTDIR\man\*.1"
   RMDir "$INSTDIR\man"
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index dea70360..f969f013 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -22,7 +22,6 @@ open Evd
 open Goptions
 open Genarg
 open Clenv
-open Universes
 
 let _ = Detyping.print_evar_arguments := true
 let _ = Detyping.print_universes := true
@@ -503,7 +502,7 @@ open Egramml
 
 let _ =
   try
-    Vernacinterp.vinterp_add ("PrintConstr", 0)
+    Vernacinterp.vinterp_add false ("PrintConstr", 0)
       (function
          [c] when genarg_tag c = ConstrArgType && true ->
            let c = out_gen (rawwit wit_constr) c in
@@ -520,7 +519,7 @@ let _ =
 
 let _ =
   try
-    Vernacinterp.vinterp_add ("PrintPureConstr", 0)
+    Vernacinterp.vinterp_add false ("PrintPureConstr", 0)
       (function
          [c] when genarg_tag c = ConstrArgType && true ->
            let c = out_gen (rawwit wit_constr) c in
-- 
cgit v1.2.3