code mort dans tactinterp; plus de Debug On/Off dans Correctness

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2490 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 8 insertions, 58 deletions

diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index 6d0ad0fb0e..bb9f539bb8 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -18,15 +18,13 @@ open Term
 
 (* debug *)
 
-let debug = ref false
-
 let deb_mess s =
-  if !debug then begin
+  if !Options.debug then begin
     msgnl s; pp_flush()
   end
 
 let deb_print f x =
-  if !debug then begin
+  if !Options.debug then begin
     msgnl (f x); pp_flush()
   end
 
diff --git a/contrib/correctness/pmisc.mli b/contrib/correctness/pmisc.mli
index e93f20a61b..9e32f147eb 100644
--- a/contrib/correctness/pmisc.mli
+++ b/contrib/correctness/pmisc.mli
@@ -70,7 +70,6 @@ val abstract : (identifier * constr) list -> constr -> constr
 
 (* for debugging purposes *)
 
-val debug : bool ref
 val deb_mess : Pp.std_ppcmds -> unit
 val deb_print : ('a -> Pp.std_ppcmds) -> 'a -> unit
 
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index e1fd72fb4b..0791dab78d 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -499,12 +499,6 @@ let is_assumed global ids =
 
 let add = vinterp_add
 
-let _ = add "PROGDEBUGON"
-     (function [] -> fun () -> debug := true | _  -> assert false)
-
-let _ = add "PROGDEBUGOFF"
-     (function [] -> fun () -> debug := false | _  -> assert false)
-
 let _ = add "CORRECTNESS"
      (function
 	 [ VARG_STRING s; VARG_DYN d ] -> 
@@ -583,10 +577,6 @@ GEXTEND Gram
 	let d = Ast.dynamic (in_prog p) in
 	let str = Ast.string s in
 	<:ast< (CORRECTNESS $str (VERNACDYN $d) (TACTIC $tac)) >> ] ];
-  Pcoq.Vernac_.command:
-  [ [ IDENT "Debug"; IDENT "on"; "." -> <:ast< (PROGDEBUGON) >>
-	
-    | IDENT "Debug"; IDENT "off"; "." -> <:ast< (PROGDEBUGOFF) >> ] ];
  END
 ;;
 
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index c2bc2ddcbe..e58d951c42 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -181,32 +181,6 @@ let constrOut = constrOut
 
 let loc = dummy_loc
 
-(* Table of interpretation functions *)
-let interp_tab =
-  (Hashtbl.create 17 : (string , interp_sign -> Coqast.t -> value) Hashtbl.t)
-
-(* Adds an interpretation function *)
-let interp_add (ast_typ,interp_fun) =
-  try
-    Hashtbl.add interp_tab ast_typ interp_fun
-  with
-      Failure _ ->
-        errorlabstrm "interp_add"
-          (str "Cannot add the interpretation function for " ++ str ast_typ ++
-            str " twice")
-
-(* Adds a possible existing interpretation function *)
-let overwriting_interp_add (ast_typ,interp_fun) =
-  if Hashtbl.mem interp_tab ast_typ then
-  begin
-    Hashtbl.remove interp_tab ast_typ;
-    warning ("Overwriting definition of tactic interpreter command " ^ ast_typ)
-  end;
-  Hashtbl.add interp_tab ast_typ interp_fun
-
-(* Finds the interpretation function corresponding to a given ast type *)
-let look_for_interp = Hashtbl.find interp_tab
-
 (* Globalizes the identifier *)
 let glob_const_nvar loc env qid =
   try
@@ -548,23 +522,12 @@ let rec val_interp ist ast =
         VArg ((Intropattern (cvt_intro_pattern ist ast)))
     | Node(_,"LETPATTERNS",astl) ->
         VArg (Letpatterns (List.fold_left (cvt_letpattern ist) (None,[]) astl))
+    | Node(loc,s,[]) ->
+        VFTactic ([],(interp_atomic s))
     | Node(loc,s,l) ->
-        (try
-          ((look_for_interp s) ist ast)
-        with
-           Not_found ->
-             if l = [] then
-               VFTactic ([],(interp_atomic s))
-             else
-               let fv = val_interp ist
-                          (Node(loc,"PRIMTACTIC",[Node(loc,s,[])]))
-               and largs = List.map (val_interp ist) l in
-               app_interp ist fv largs ast)
-
-       (*     val_interp ist (Node(dummy_loc,"APP",[Node(loc,"PRIMTACTIC",
-                            [Node(loc,s,[])])]@l)))*)
- 
-(*             val_interp ist (Node(dummy_loc,"APPTACTIC",[ast])))*)
+        let fv = val_interp ist (Node(loc,"PRIMTACTIC",[Node(loc,s,[])]))
+        and largs = List.map (val_interp ist) l in
+        app_interp ist fv largs ast
     | Dynamic(_,t) ->
       let tg = (tag t) in
       if tg = "tactic" then
diff --git a/theories/IntMap/Adist.v b/theories/IntMap/Adist.v
index 5c3296885c..fbc2870f16 100644
--- a/theories/IntMap/Adist.v
+++ b/theories/IntMap/Adist.v
@@ -270,7 +270,7 @@ Qed.
     d(a,a'')+d(a'',a')$,
   but in fact $d(a,a')\leq max(d(a,a''),d(a'',a'))$.
   This means that $min(pd(a,a''),pd(a'',a'))<=pd(a,a')$ (lemma [ad_pdist_ultra] below).
-  This follows from the fact that $a \Ra |a| = 1/2^{\texttt{ad\_plength}}(a))$
+  This follows from the fact that $a ~Ra~|a| = 1/2^{\texttt{ad\_plength}}(a))$
   is an ultrametric norm, i.e. that $|a-a'| \leq max (|a-a''|, |a''-a'|)$,
   or equivalently that $|a+b|<=max(|a|,|b|)$, i.e. that
   min $(\texttt{ad\_plength}(a), \texttt{ad\_plength}(b)) \leq