From db5576383c7c8df01c6672abea9654ee860e4289 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 17 Mar 2006 21:12:12 +0000
Subject: MAJ debugging (et arrêt support version française)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8643 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/deboguage.txt | 30 ------------------------------
 1 file changed, 30 deletions(-)
 delete mode 100644 dev/deboguage.txt

(limited to 'dev')

diff --git a/dev/deboguage.txt b/dev/deboguage.txt
deleted file mode 100644
index 6e48634835..0000000000
--- a/dev/deboguage.txt
+++ /dev/null
@@ -1,30 +0,0 @@
-
-Debuggage
-=========
-
-   dans Emacs. nécessite le mode tuareg.
-   Coq doit être configuré avec -debug et -local (./configure -debug -local)
-
-   1. M-x camldebug
-   2. spécifier le binaire bin/coqtop.byte
-   3. spécifier ../dev/ocamldebug-coq
-   4. source db  (pour avoir les pretty-printers)
-   5. poser ses points d'arrêts avec C-x C-a C-b (penser "add breakpoint")
-      directement dans le source ocaml
-   6. ensuite voir le man d'ocamldebug
-         run
-	 step
-	 next
-	 last
-	 print x
-	 ...
-
-
-Profiling
-=========
-
-   Coq doit être configuré avec -profile
-
-   1. Lancer Coq en natif, qui doit terminer normalement (utiliser Quit
-      ou l'option -batch)
-   2. gprof ./coqtop gmon.out
-- 
cgit v1.2.3