- Correction d'un nouveau bug de undo de CoqIDE ("Admitted" et "Proof t"

  n'étaient pas gérés, merci à Julien). 
- Correction pb blocage CoqIDE quand le browser n'est pas déja lancé
  (utilisation pour cela de Sys.command au lieu de Unix.open_process_full).
- MAJ CHANGES et COMPATIBILITY.


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

6 files changed, 37 insertions, 66 deletions

diff --git a/CHANGES b/CHANGES
index b4d8397e97..c51cbd9dcd 100644
--- a/CHANGES
+++ b/CHANGES
@@ -93,6 +93,8 @@ Libraries (DOC TO CHECK)
 - Slight restructuration of the Logic library regarding choice and classical
   logic. Addition of files providing intuitionistic axiomatizations of
   descriptions: Epsilon.v, Description.v and IndefiniteDescription.v.
+- Definition of pred and minus made compatible with the structural
+  decreasing criterion for use in fixpoints.
 
 Notations, coercions, implicit arguments and type inference
 
@@ -497,7 +499,7 @@ Modules
   "Module Type M(Export/Import X Y: T)"
   (only for interactive definitions)
 - Construct "with" generalized to module paths:
-   T with (Definition|Module) M1.M2....Mn.l := l' (doc TODO).
+   T with (Definition|Module) M1.M2....Mn.l := l'.
 
 Notations
 
diff --git a/COMPATIBILITY b/COMPATIBILITY
index b5d94d584b..7ddc33d47f 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -1,12 +1,12 @@
-Potential sources of incompatibilities between Coq V8.0 and V8.1
+Potential sources of incompatibilities between Coq V8.1 and V8.2
 ----------------------------------------------------------------
 
 (see also file CHANGES)
 
 Language
 
-- Inductive types in Type are now polymorphic over their parameters in
-  Type. This may affect the naming of introduction hypotheses if such
+- Constants hidding polymorphic inductive types are now polymorphic themselves.
+  This may exceptionally affect the naming of introduction hypotheses if such
   an inductive type in Type is used on small types such as Prop or
   Set: the hypothesis names suffix will default to H instead of X.  As
   a matter of fact, it is recommended to systematically name the
@@ -14,45 +14,20 @@ Language
 
 Tactics
 
-- Some bug fixes may lead to incompatibilities. This is e.g. the case
-  of inversion on Type which failed to rewrite some hypotheses as it
-  did on Prop/Set.
-
-- Add Morphism for the Prop/iff setoid now requires a proof of
-  biimplication instead of a proof of implication.
-
-- The order of arguments in compatibility morphisms changed: the
-  premises and the parameters are now interleaved while the whole
-  bunch of parameters used to come first.
-
-- The previous implementation of the ring and field tactics are
-  maintained but their name changed : require modules "LegacyRing" or
-  "LegacyField" and globally replace calls to "ring" and "field" by
-  calls to "legacy ring" and "legacy field".
-
-- Users ready to benefit of the power of the new implemetations have
-  to know that
-
-  - most of the time, ring solves goals similarly and often faster;
-  - if not, it may be because the old ring did some automatic unfold;
-    they now have to be done separately (by hand or using ltac);
-  - most of the time, field solvesp goals similarly but much faster but
-    there are usually less side conditions to prove;
-  - to simplify expressions, use now ring_simplify and field_simplify;
-  - simplifications are most of the time different: the new results are
-    more natural but they may require some adaptation of proof scripts;
-  - the Ring library no longer imports the Bool library (you may have
-    to explicitly request a "Require Import Bool");
-  - to declare new rings and fields, see the documentation.
+- The apply tactic now unfolds the constants if needed to succeed.  As
+  a consequence, use of "try apply" or "repeat apply" or "apply" in
+  other Ltac potentially backtracking code may behave differently. Use
+  "simple apply" instead.
+
+- Add Relation and Add Morphism on polymorphic relations should now be
+  declared with Add Parametric Relation and Add Parametric Morphism.
+
+- Some bug fixes may lead to incompatibilities.
 
 Libraries
 
-- A few changes in the library (as mentioned in the CHANGES file) may
+- Some changes in the library (as mentioned in the CHANGES file) may
   imply the need for local adaptations.
 
-- Occurrence numbering order for unfold, pattern, etc changed for the
-  match construction: occurrences in the return clause now come after
-  the occurrences in the term matched; this was the opposite before.
-
-For changes in the ML interfaces, see file dev/doc/changes.txt in the
-main archive.
+For the main changes in the ML interfaces, see file
+dev/doc/changes.txt in the main archive.
diff --git a/ide/coq.ml b/ide/coq.ml
index ca28d19485..f45bd9f5c2 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -376,8 +376,9 @@ let compute_reset_info = function
   | VernacStartTheoremProof (_, [Some (_,id), _], _, _) ->
       ResetAtStatement (reset_mark id, ref false)
 
-  | VernacEndProof _ | VernacEndSegment _ -> NoReset
-  | _ -> match Lib.has_top_frozen_state () with
+  | VernacEndProof _ | VernacExactProof _ | VernacEndSegment _ -> NoReset
+  | com -> if is_vernac_tactic_command com then NoReset else
+      match Lib.has_top_frozen_state () with
       | Some sp -> ResetAtRegisteredObject (ResetToState sp, ref true)
       | None -> NoReset
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index dd807443b3..29b34d28ad 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -533,7 +533,7 @@ let push_phrase reset_info start_of_phrase_mark end_of_phrase_mark ast =
 	  } in
   begin
     match snd ast with
-      | VernacEndProof (Proved (_, None)) -> update_on_end_of_proof ()
+      | VernacEndProof _ | VernacExactProof _ -> update_on_end_of_proof ()
       | VernacEndSegment (_,id) -> update_on_end_of_segment id
       | _ -> ()
   end;
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 6a4833ec88..3442910d35 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -289,10 +289,8 @@ let run_command f c =
   let buffe = String.make 127 ' ' in
   let n = ref 0 in
   let ne = ref 0 in
-
-  while n:= input cin buff 0 127 ; ne := input cerr buffe 0 127 ; 
-    !n+ !ne <> 0
-  do 
+  while n:= input cin buff 0 127 ; ne := input cerr buffe 0 127 ; !n+ !ne <> 0
+  do
     let r = try_convert (String.sub buff 0 !n) in 
     f r;
     Buffer.add_string result r;
@@ -304,10 +302,10 @@ let run_command f c =
 
 let browse f url =
   let com = Flags.subst_command_placeholder !current.cmd_browse url in
-  let (s,_res) = run_command f com in
-  if s = Unix.WEXITED 127 then
-    prerr_endline
-      ("Could not execute\n  \""^com^"\"\ncheck your preferences for setting a valid browser command")
+  let s = Sys.command com in
+  if s = 127 then
+    f ("Could not execute\n\""^com^
+       "\"\ncheck your preferences for setting a valid browser command\n")
 
 let url_for_keyword =
   let ht = Hashtbl.create 97 in
@@ -332,8 +330,7 @@ let url_for_keyword =
 
 let browse_keyword f text = 
   try let u = url_for_keyword text in browse f (!current.doc_url ^ u) 
-  with Not_found ->
-    prerr_endline ("No documentation found for "^text)
+  with Not_found -> f ("No documentation found for "^text)
 
 
 let underscore = Glib.Utf8.to_unichar "_" (ref 0)
diff --git a/lib/flags.ml b/lib/flags.ml
index f9c855d86e..0635ad7c1f 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -112,18 +112,14 @@ let boxed_definitions _ = !boxed_definitions
 
 let subst_command_placeholder s t =
   let buff = Buffer.create (String.length s + String.length t) in
-    if String.length s < 2 then
-      Buffer.add_string buff s
-    else
-      begin
-	let i = ref 0 in
-	  while (!i <= String.length s - 2) do
-	    if s.[!i] = '%' & s.[!i+1] = 's' then (Buffer.add_string buff t;incr i)
-	    else Buffer.add_char buff s.[!i];
-	    incr i
-	  done
-      end;
-    Buffer.contents buff
+  let i = ref 0 in
+  while (!i < String.length s) do
+    if s.[!i] = '%' & !i+1 < String.length s & s.[!i+1] = 's'
+    then (Buffer.add_string buff t;incr i)
+    else Buffer.add_char buff s.[!i];
+    incr i
+  done;
+  Buffer.contents buff
 
 let browser_cmd_fmt =
  try