Correction problème de compil (blast.ml)

Correction bugs commentaires pour coqdoc (ChoiceFacts.v)
Test-suite


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

3 files changed, 20 insertions, 11 deletions

diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 7cc43e4ce8..48caa3777c 100644
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -334,7 +334,7 @@ let e_breadth_search debug n db_list local_db gl =
   with Not_found -> error "EAuto: breadth first search failed"
 
 let e_search_auto debug (n,p) db_list gl = 
-  let local_db = make_local_hint_db [] gl in 
+  let local_db = make_local_hint_db true [] gl in 
   if n = 0 then 
     e_depth_search debug p db_list local_db gl
   else 
@@ -354,7 +354,7 @@ let full_eauto debug n gl =
   let dbnames = current_db_names () in
   let dbnames =  list_subtract dbnames ["v62"] in
   let db_list = List.map searchtable_map dbnames in
-  let _local_db = make_local_hint_db [] gl in
+  let _local_db = make_local_hint_db true [] gl in
   tclTRY (e_search_auto debug n db_list) gl
 
 let my_full_eauto n gl = full_eauto false (n,0) gl
@@ -495,7 +495,7 @@ let full_auto n gl =
   let dbnames = list_subtract dbnames ["v62"] in
   let db_list = List.map searchtable_map dbnames in
   let hyps = pf_hyps gl in
-  tclTRY (search n db_list (make_local_hint_db [] gl) hyps) gl
+  tclTRY (search n db_list (make_local_hint_db false [] gl) hyps) gl
   
 let default_full_auto gl = full_auto !default_search_depth gl
 (************************************************************************)
diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v
index a11297ea90..86e55922df 100644
--- a/test-suite/success/rewrite.v
+++ b/test-suite/success/rewrite.v
@@ -29,3 +29,12 @@ Axiom e : forall (A : Set) (EA : A -> A -> Prop) (a : A), EA a a.
 Theorem th : forall x : N, E x x.
 intro x. try rewrite e.
 Abort.
+
+(* Behavior of rewrite wrt conversion *)
+
+Require Import Arith.
+
+Goal forall n, 0 + n = n -> True.
+intros n H.
+rewrite plus_0_l in H.
+Abort.
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 20ffe7b5a7..3f4c4354bb 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -29,7 +29,7 @@ description principles
 
 - OAC_rel = "omniscient" relational form of the (non extensional) axiom of choice
 - OAC_fun = "omniscient" functional form of the (non extensional) axiom of choice
-            (called AC* in Bell [Bell])
+            (called AC* in Bell [[Bell]])
 - OAC!
 
 - ID_iota    = intuitionistic definite description
@@ -43,7 +43,7 @@ description principles
             (an unconstrained generalisation of the constructive principle of
              independence of premises)
 - Drinker = drinker's paradox (small form)
-            (called Ex in Bell [Bell])  
+            (called Ex in Bell [[Bell]])
 
 We let also
 
@@ -75,10 +75,10 @@ Table of contents
 
 References:
 
-[Bell] John L. Bell, Choice principles in intuitionistic set theory,
+[[Bell]] John L. Bell, Choice principles in intuitionistic set theory,
 unpublished.
 
-[Bell93] John L. Bell, Hilbert's Epsilon Operator in Intuitionistic
+[[Bell93]] John L. Bell, Hilbert's Epsilon Operator in Intuitionistic
 Type Theories, Mathematical Logic Quarterly, volume 39, 1993.
 
 [Carlstrøm05] Jesper Carlstrøm, Interpreting descriptions in
@@ -426,7 +426,7 @@ Qed.
 
 (** AC_fun + Drinker = OAC_fun *)
 
-(** This was already observed by Bell [Bell] *)
+(** This was already observed by Bell [[Bell]] *)
 
 Lemma omniscient_fun_choice_imp_small_drinker :
   OmniscientFunctionalChoice -> SmallDrinker'sParadox.
@@ -754,17 +754,17 @@ be applied on the same Type universes on both sides of the first
 (**********************************************************************)
 (** * Excluded-middle + definite description => computational excluded-middle *)
 
-(** The idea for the following proof comes from [ChicliPottierSimpson02] *)
+(** The idea for the following proof comes from [[ChicliPottierSimpson02]] *)
 
 (** Classical logic and axiom of unique choice (i.e. functional
-    relation reification), as shown in [ChicliPottierSimpson02],
+    relation reification), as shown in [[ChicliPottierSimpson02]],
     implies the double-negation of excluded-middle in [Set] (which is
     incompatible with the impredicativity of [Set]).
 
     We adapt the proof to show that constructive definite description
     transports excluded-middle from [Prop] to [Set].
 
-    [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos
+    [[ChicliPottierSimpson02]] Laurent Chicli, Loïc Pottier, Carlos
     Simpson, Mathematical Quotients and Quotient Types in Coq,
     Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646,
     Springer Verlag.  *)