Imported Upstream version 8.4~betaupstream/8.4_beta

7 files changed, 227 insertions, 270 deletions

diff --git a/plugins/omega/Omega.v b/plugins/omega/Omega.v
index c8a06265..3f9d0f44 100644
--- a/plugins/omega/Omega.v
+++ b/plugins/omega/Omega.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -13,8 +13,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* $Id: Omega.v 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 (* We do not require [ZArith] anymore, but only what's necessary for Omega *)
 Require Export ZArith_base.
 Require Export OmegaLemmas.
diff --git a/plugins/omega/OmegaLemmas.v b/plugins/omega/OmegaLemmas.v
index ec9faedd..5b6f4670 100644
--- a/plugins/omega/OmegaLemmas.v
+++ b/plugins/omega/OmegaLemmas.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(*i $Id: OmegaLemmas.v 12337 2009-09-17 15:58:14Z glondu $ i*)
-
 Require Import ZArith_base.
 Open Local Scope Z_scope.
 
@@ -300,3 +298,10 @@ Definition fast_Zred_factor5 (x y : Z) (P : Z -> Prop)
 
 Definition fast_Zred_factor6 (x : Z) (P : Z -> Prop)
   (H : P (x + 0)) := eq_ind_r P H (Zred_factor6 x).
+
+Theorem intro_Z :
+  forall n:nat,  exists y : Z, Z_of_nat n = y /\ 0 <= y * 1 + 0.
+Proof.
+  intros n; exists (Z_of_nat n); split; trivial.
+  rewrite Zmult_1_r, Zplus_0_r. apply Zle_0_nat.
+Qed.
diff --git a/plugins/omega/OmegaPlugin.v b/plugins/omega/OmegaPlugin.v
index 69a6ea72..a3ab34a9 100644
--- a/plugins/omega/OmegaPlugin.v
+++ b/plugins/omega/OmegaPlugin.v
@@ -1,11 +1,9 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: OmegaPlugin.v 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 Declare ML Module "omega_plugin".
diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
index a5a085a9..46fd5682 100644
--- a/plugins/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
@@ -28,7 +28,7 @@ Open Local Scope Z_scope.
 
 Ltac zify_unop_core t thm a :=
  (* Let's introduce the specification theorem for t *)
- let H:= fresh "H" in assert (H:=thm a);
+ pose proof (thm a);
  (* Then we replace (t a) everywhere with a fresh variable *)
  let z := fresh "z" in set (z:=t a) in *; clearbody z.
 
@@ -159,11 +159,9 @@ Ltac zify_nat_op :=
 
   (* mult -> Zmult and a positivity hypothesis *)
   | H : context [ Z_of_nat (mult ?a ?b) ] |- _ =>
-        let H:= fresh "H" in
-        assert (H:=Zle_0_nat (mult a b)); rewrite (inj_mult a b) in *
+        pose proof (Zle_0_nat (mult a b)); rewrite (inj_mult a b) in *
   | |- context [ Z_of_nat (mult ?a ?b) ] =>
-        let H:= fresh "H" in
-        assert (H:=Zle_0_nat (mult a b)); rewrite (inj_mult a b) in *
+        pose proof (Zle_0_nat (mult a b)); rewrite (inj_mult a b) in *
 
   (* O -> Z0 *)
   | H : context [ Z_of_nat O ] |- _ => simpl (Z_of_nat O) in H
@@ -184,20 +182,9 @@ Ltac zify_nat_op :=
      end
 
   (* atoms of type nat : we add a positivity condition (if not already there) *)
-  | H : context [ Z_of_nat ?a ] |- _ =>
-        match goal with
-          | H' : 0 <= Z_of_nat a |- _ => hide_Z_of_nat a
-          | H' : 0 <= Z_of_nat' a |- _ => fail
-          | _ => let H:= fresh "H" in
-                 assert (H:=Zle_0_nat a); hide_Z_of_nat a
-        end
-  | |- context [ Z_of_nat ?a ] =>
-        match goal with
-          | H' : 0 <= Z_of_nat a |- _ => hide_Z_of_nat a
-          | H' : 0 <= Z_of_nat' a |- _ => fail
-          | _ => let H:= fresh "H" in
-                 assert (H:=Zle_0_nat a); hide_Z_of_nat a
-        end
+  | _ : 0 <= Z_of_nat ?a |- _ => hide_Z_of_nat a
+  | _ : context [ Z_of_nat ?a ] |- _ => pose proof (Zle_0_nat a); hide_Z_of_nat a
+  | |- context [ Z_of_nat ?a ] => pose proof (Zle_0_nat a); hide_Z_of_nat a
  end.
 
 Ltac zify_nat := repeat zify_nat_rel; repeat zify_nat_op; unfold Z_of_nat' in *.
@@ -223,17 +210,17 @@ Ltac zify_positive_rel :=
   | H : context [ @eq positive ?a ?b ] |- _ => rewrite (Zpos_eq_iff a b) in H
   | |- context [ @eq positive ?a ?b ] =>       rewrite (Zpos_eq_iff a b)
   (* II: less than *)
-  | H : context [ (?a<?b)%positive ] |- _ => change (a<b)%positive with (Zpos a<Zpos b) in H
-  | |- context [ (?a<?b)%positive ] => change (a<b)%positive with (Zpos a<Zpos b)
+  | H : context [ (?a < ?b)%positive ] |- _ => change (a<b)%positive with (Zpos a<Zpos b) in H
+  | |- context [ (?a < ?b)%positive ] => change (a<b)%positive with (Zpos a<Zpos b)
   (* III: less or equal *)
-  | H : context [ (?a<=?b)%positive ] |- _ => change (a<=b)%positive with (Zpos a<=Zpos b) in H
-  | |- context [ (?a<=?b)%positive ] => change (a<=b)%positive with (Zpos a<=Zpos b)
+  | H : context [ (?a <= ?b)%positive ] |- _ => change (a<=b)%positive with (Zpos a<=Zpos b) in H
+  | |- context [ (?a <= ?b)%positive ] => change (a<=b)%positive with (Zpos a<=Zpos b)
   (* IV: greater than *)
-  | H : context [ (?a>?b)%positive ] |- _ => change (a>b)%positive with (Zpos a>Zpos b) in H
-  | |- context [ (?a>?b)%positive ] => change (a>b)%positive with (Zpos a>Zpos b)
+  | H : context [ (?a > ?b)%positive ] |- _ => change (a>b)%positive with (Zpos a>Zpos b) in H
+  | |- context [ (?a > ?b)%positive ] => change (a>b)%positive with (Zpos a>Zpos b)
   (* V: greater or equal *)
-  | H : context [ (?a>=?b)%positive ] |- _ => change (a>=b)%positive with (Zpos a>=Zpos b) in H
-  | |- context [ (?a>=?b)%positive ] => change (a>=b)%positive with (Zpos a>=Zpos b)
+  | H : context [ (?a >= ?b)%positive ] |- _ => change (a>=b)%positive with (Zpos a>=Zpos b) in H
+  | |- context [ (?a >= ?b)%positive ] => change (a>=b)%positive with (Zpos a>=Zpos b)
  end.
 
 Ltac zify_positive_op :=
@@ -282,11 +269,9 @@ Ltac zify_positive_op :=
 
   (* Pmult -> Zmult and a positivity hypothesis *)
   | H : context [ Zpos (Pmult ?a ?b) ] |- _ =>
-        let H:= fresh "H" in
-        assert (H:=Zgt_pos_0 (Pmult a b)); rewrite (Zpos_mult_morphism a b) in *
+        pose proof (Zgt_pos_0 (Pmult a b)); rewrite (Zpos_mult_morphism a b) in *
   | |- context [ Zpos (Pmult ?a ?b) ] =>
-        let H:= fresh "H" in
-        assert (H:=Zgt_pos_0 (Pmult a b)); rewrite (Zpos_mult_morphism a b) in *
+        pose proof (Zgt_pos_0 (Pmult a b)); rewrite (Zpos_mult_morphism a b) in *
 
   (* xO *)
   | H : context [ Zpos (xO ?a) ] |- _ =>
@@ -320,18 +305,9 @@ Ltac zify_positive_op :=
   | |- context [ Zpos xH ] => hide_Zpos xH
 
   (* atoms of type positive : we add a positivity condition (if not already there) *)
-  | H : context [ Zpos ?a ] |- _ =>
-        match goal with
-         | H' : Zpos a > 0 |- _ => hide_Zpos a
-         | H' : Zpos' a > 0 |- _ => fail
-         | _ => let H:= fresh "H" in assert (H:=Zgt_pos_0 a); hide_Zpos a
-        end
-  | |- context [ Zpos ?a ] =>
-        match goal with
-         | H' : Zpos a > 0 |- _ => hide_Zpos a
-         | H' : Zpos' a > 0 |- _ => fail
-         | _ => let H:= fresh "H" in assert (H:=Zgt_pos_0 a); hide_Zpos a
-        end
+  | _ : Zpos ?a > 0 |- _ => hide_Zpos a
+  | _ : context [ Zpos ?a ] |- _ => pose proof (Zgt_pos_0 a); hide_Zpos a
+  | |- context [ Zpos ?a ] => pose proof (Zgt_pos_0 a); hide_Zpos a
  end.
 
 Ltac zify_positive :=
@@ -358,25 +334,25 @@ Ltac zify_N_rel :=
   | H : context [ @eq N ?a ?b ] |- _ => rewrite (Z_of_N_eq_iff a b) in H
   | |- context [ @eq N ?a ?b ] =>       rewrite (Z_of_N_eq_iff a b)
   (* II: less than *)
-  | H : (?a<?b)%N |- _ => generalize (Z_of_N_lt _ _ H); clear H; intro H
-  | |- (?a<?b)%N => apply (Z_of_N_lt_rev a b)
-  | H : context [ (?a<?b)%N ] |- _ => rewrite (Z_of_N_lt_iff a b) in H
-  | |- context [ (?a<?b)%N ] =>       rewrite (Z_of_N_lt_iff a b)
+  | H : (?a < ?b)%N |- _ => generalize (Z_of_N_lt _ _ H); clear H; intro H
+  | |- (?a < ?b)%N => apply (Z_of_N_lt_rev a b)
+  | H : context [ (?a < ?b)%N ] |- _ => rewrite (Z_of_N_lt_iff a b) in H
+  | |- context [ (?a < ?b)%N ] =>       rewrite (Z_of_N_lt_iff a b)
   (* III: less or equal *)
-  | H : (?a<=?b)%N |- _ => generalize (Z_of_N_le _ _ H); clear H; intro H
-  | |- (?a<=?b)%N => apply (Z_of_N_le_rev a b)
-  | H : context [ (?a<=?b)%N ] |- _ => rewrite (Z_of_N_le_iff a b) in H
-  | |- context [ (?a<=?b)%N ] =>       rewrite (Z_of_N_le_iff a b)
+  | H : (?a <= ?b)%N |- _ => generalize (Z_of_N_le _ _ H); clear H; intro H
+  | |- (?a <= ?b)%N => apply (Z_of_N_le_rev a b)
+  | H : context [ (?a <= ?b)%N ] |- _ => rewrite (Z_of_N_le_iff a b) in H
+  | |- context [ (?a <= ?b)%N ] =>       rewrite (Z_of_N_le_iff a b)
   (* IV: greater than *)
-  | H : (?a>?b)%N |- _ => generalize (Z_of_N_gt _ _ H); clear H; intro H
-  | |- (?a>?b)%N => apply (Z_of_N_gt_rev a b)
-  | H : context [ (?a>?b)%N ] |- _ => rewrite (Z_of_N_gt_iff a b) in H
-  | |- context [ (?a>?b)%N ] =>       rewrite (Z_of_N_gt_iff a b)
+  | H : (?a > ?b)%N |- _ => generalize (Z_of_N_gt _ _ H); clear H; intro H
+  | |- (?a > ?b)%N => apply (Z_of_N_gt_rev a b)
+  | H : context [ (?a > ?b)%N ] |- _ => rewrite (Z_of_N_gt_iff a b) in H
+  | |- context [ (?a > ?b)%N ] =>       rewrite (Z_of_N_gt_iff a b)
   (* V: greater or equal *)
-  | H : (?a>=?b)%N |- _ => generalize (Z_of_N_ge _ _ H); clear H; intro H
-  | |- (?a>=?b)%N => apply (Z_of_N_ge_rev a b)
-  | H : context [ (?a>=?b)%N ] |- _ => rewrite (Z_of_N_ge_iff a b) in H
-  | |- context [ (?a>=?b)%N ] =>       rewrite (Z_of_N_ge_iff a b)
+  | H : (?a >= ?b)%N |- _ => generalize (Z_of_N_ge _ _ H); clear H; intro H
+  | |- (?a >= ?b)%N => apply (Z_of_N_ge_rev a b)
+  | H : context [ (?a >= ?b)%N ] |- _ => rewrite (Z_of_N_ge_iff a b) in H
+  | |- context [ (?a >= ?b)%N ] =>       rewrite (Z_of_N_ge_iff a b)
  end.
 
 Ltac zify_N_op :=
@@ -413,25 +389,14 @@ Ltac zify_N_op :=
 
   (* Nmult -> Zmult and a positivity hypothesis *)
   | H : context [ Z_of_N (Nmult ?a ?b) ] |- _ =>
-        let H:= fresh "H" in
-        assert (H:=Z_of_N_le_0 (Nmult a b)); rewrite (Z_of_N_mult a b) in *
+        pose proof (Z_of_N_le_0 (Nmult a b)); rewrite (Z_of_N_mult a b) in *
   | |- context [ Z_of_N  (Nmult ?a ?b) ] =>
-        let H:= fresh "H" in
-        assert (H:=Z_of_N_le_0 (Nmult a b)); rewrite (Z_of_N_mult a b) in *
+        pose proof (Z_of_N_le_0 (Nmult a b)); rewrite (Z_of_N_mult a b) in *
 
   (* atoms of type N : we add a positivity condition (if not already there) *)
-  | H : context [ Z_of_N ?a ] |- _ =>
-        match goal with
-         | H' : 0 <= Z_of_N a |- _ => hide_Z_of_N a
-         | H' : 0 <= Z_of_N' a |- _ => fail
-         | _ => let H:= fresh "H" in assert (H:=Z_of_N_le_0 a); hide_Z_of_N a
-        end
-  | |- context [ Z_of_N ?a ] =>
-        match goal with
-         | H' : 0 <= Z_of_N a |- _ => hide_Z_of_N a
-         | H' : 0 <= Z_of_N' a |- _ => fail
-         | _ => let H:= fresh "H" in assert (H:=Z_of_N_le_0 a); hide_Z_of_N a
-        end
+  | _ : 0 <= Z_of_N ?a |- _ => hide_Z_of_N a
+  | _ : context [ Z_of_N ?a ] |- _ => pose proof (Z_of_N_le_0 a); hide_Z_of_N a
+  | |- context [ Z_of_N ?a ] => pose proof (Z_of_N_le_0 a); hide_Z_of_N a
  end.
 
 Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *.
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 20565d06..d7dfe149 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -13,8 +13,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* $Id: coq_omega.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Util
 open Pp
 open Reduction
@@ -22,7 +20,6 @@ open Proof_type
 open Names
 open Nameops
 open Term
-open Termops
 open Declarations
 open Environ
 open Sign
@@ -60,6 +57,7 @@ open Goptions
 let _ =
   declare_bool_option
     { optsync  = false;
+      optdepr  = false;
       optname  = "Omega system time displaying flag";
       optkey   = ["Omega";"System"];
       optread  = read display_system_flag;
@@ -68,6 +66,7 @@ let _ =
 let _ =
   declare_bool_option
     { optsync  = false;
+      optdepr  = false;
       optname  = "Omega action display flag";
       optkey   = ["Omega";"Action"];
       optread  = read display_action_flag;
@@ -76,6 +75,7 @@ let _ =
 let _ =
   declare_bool_option
     { optsync  = false;
+      optdepr  = false;
       optname  = "Omega old style flag";
       optkey   = ["Omega";"OldStyle"];
       optread  = read old_style_flag;
@@ -128,12 +128,12 @@ let intern_id,unintern_id =
 
 let mk_then = tclTHENLIST
 
-let exists_tac c = constructor_tac false (Some 1) 1 (Rawterm.ImplicitBindings [c])
+let exists_tac c = constructor_tac false (Some 1) 1 (Glob_term.ImplicitBindings [c])
 
 let generalize_tac t = generalize_time (generalize t)
 let elim t = elim_time (simplest_elim t)
 let exact t = exact_time (Tactics.refine t)
-let unfold s = Tactics.unfold_in_concl [all_occurrences, Lazy.force s]
+let unfold s = Tactics.unfold_in_concl [Termops.all_occurrences, Lazy.force s]
 
 let rev_assoc k =
   let rec loop = function
@@ -150,7 +150,7 @@ let tag_hypothesis,tag_of_hyp, hyp_of_tag =
 let hide_constr,find_constr,clear_tables,dump_tables =
   let l = ref ([]:(constr * (identifier * identifier * bool)) list) in
   (fun h id eg b -> l := (h,(id,eg,b)):: !l),
-  (fun h -> try List.assoc h !l with Not_found -> failwith "find_contr"),
+  (fun h -> try list_assoc_f eq_constr h !l with Not_found -> failwith "find_contr"),
   (fun () -> l := []),
   (fun () -> !l)
 
@@ -169,6 +169,8 @@ let coq_modules =
 let init_constant = gen_constant_in_modules "Omega" init_modules
 let constant = gen_constant_in_modules "Omega" coq_modules
 
+let z_constant = gen_constant_in_modules "Omega" [["Coq";"ZArith"]]
+
 (* Zarith *)
 let coq_xH = lazy (constant "xH")
 let coq_xO = lazy (constant "xO")
@@ -184,6 +186,7 @@ let coq_Zmult = lazy (constant "Zmult")
 let coq_Zopp = lazy (constant "Zopp")
 let coq_Zminus = lazy (constant "Zminus")
 let coq_Zsucc = lazy (constant "Zsucc")
+let coq_Zpred = lazy (constant "Zpred")
 let coq_Zgt = lazy (constant "Zgt")
 let coq_Zle = lazy (constant "Zle")
 let coq_Z_of_nat = lazy (constant "Z_of_nat")
@@ -191,13 +194,13 @@ let coq_inj_plus = lazy (constant "inj_plus")
 let coq_inj_mult = lazy (constant "inj_mult")
 let coq_inj_minus1 = lazy (constant "inj_minus1")
 let coq_inj_minus2 = lazy (constant "inj_minus2")
-let coq_inj_S = lazy (constant "inj_S")
-let coq_inj_le = lazy (constant "inj_le")
-let coq_inj_lt = lazy (constant "inj_lt")
-let coq_inj_ge = lazy (constant "inj_ge")
-let coq_inj_gt = lazy (constant "inj_gt")
-let coq_inj_neq = lazy (constant "inj_neq")
-let coq_inj_eq = lazy (constant "inj_eq")
+let coq_inj_S = lazy (z_constant "inj_S")
+let coq_inj_le = lazy (z_constant "Znat.inj_le")
+let coq_inj_lt = lazy (z_constant "Znat.inj_lt")
+let coq_inj_ge = lazy (z_constant "Znat.inj_ge")
+let coq_inj_gt = lazy (z_constant "Znat.inj_gt")
+let coq_inj_neq = lazy (z_constant "inj_neq")
+let coq_inj_eq = lazy (z_constant "inj_eq")
 let coq_fast_Zplus_assoc_reverse = lazy (constant "fast_Zplus_assoc_reverse")
 let coq_fast_Zplus_assoc = lazy (constant "fast_Zplus_assoc")
 let coq_fast_Zmult_assoc_reverse = lazy (constant "fast_Zmult_assoc_reverse")
@@ -255,6 +258,7 @@ let coq_dec_Zgt = lazy (constant "dec_Zgt")
 let coq_dec_Zge = lazy (constant "dec_Zge")
 
 let coq_not_Zeq = lazy (constant "not_Zeq")
+let coq_not_Zne = lazy (constant "not_Zne")
 let coq_Znot_le_gt = lazy (constant "Znot_le_gt")
 let coq_Znot_lt_ge = lazy (constant "Znot_lt_ge")
 let coq_Znot_ge_lt = lazy (constant "Znot_ge_lt")
@@ -323,6 +327,7 @@ let evaluable_ref_of_constr s c = match kind_of_term (Lazy.force c) with
   | _ -> anomaly ("Coq_omega: "^s^" is not an evaluable constant")
 
 let sp_Zsucc =     lazy (evaluable_ref_of_constr "Zsucc" coq_Zsucc)
+let sp_Zpred =     lazy (evaluable_ref_of_constr "Zpred" coq_Zpred)
 let sp_Zminus = lazy (evaluable_ref_of_constr "Zminus" coq_Zminus)
 let sp_Zle = lazy (evaluable_ref_of_constr "Zle" coq_Zle)
 let sp_Zgt = lazy (evaluable_ref_of_constr "Zgt" coq_Zgt)
@@ -356,7 +361,7 @@ let mk_integer n =
 		 [| loop (abs n) |])
 
 type omega_constant =
-  | Zplus | Zmult | Zminus | Zsucc | Zopp
+  | Zplus | Zmult | Zminus | Zsucc | Zopp | Zpred
   | Plus | Mult | Minus | Pred | S | O
   | Zpos | Zneg | Z0 | Z_of_nat
   | Eq | Neq
@@ -376,32 +381,39 @@ type result =
   | Kimp of constr * constr
   | Kufo
 
+(* Nota: Kimp correspond to a binder (Prod), but hopefully we won't
+   have to bother with term lifting: Kimp will correspond to anonymous
+   product, for which (Rel 1) doesn't occur in the right term.
+   Moreover, we'll work on fully introduced goals, hence no Rel's in
+   the term parts that we manipulate, but rather Var's.
+   Said otherwise: all constr manipulated here are closed *)
+
 let destructurate_prop t =
   let c, args = decompose_app t in
   match kind_of_term c, args with
-    | _, [_;_;_] when c = build_coq_eq () -> Kapp (Eq,args)
-    | _, [_;_] when c = Lazy.force coq_neq -> Kapp (Neq,args)
-    | _, [_;_] when c = Lazy.force coq_Zne -> Kapp (Zne,args)
-    | _, [_;_] when c = Lazy.force coq_Zle -> Kapp (Zle,args)
-    | _, [_;_] when c = Lazy.force coq_Zlt -> Kapp (Zlt,args)
-    | _, [_;_] when c = Lazy.force coq_Zge -> Kapp (Zge,args)
-    | _, [_;_] when c = Lazy.force coq_Zgt -> Kapp (Zgt,args)
-    | _, [_;_] when c = build_coq_and () -> Kapp (And,args)
-    | _, [_;_] when c = build_coq_or () -> Kapp (Or,args)
-    | _, [_;_] when c = Lazy.force coq_iff -> Kapp (Iff, args)
-    | _, [_] when c = build_coq_not () -> Kapp (Not,args)
-    | _, [] when c = build_coq_False () -> Kapp (False,args)
-    | _, [] when c = build_coq_True () -> Kapp (True,args)
-    | _, [_;_] when c = Lazy.force coq_le -> Kapp (Le,args)
-    | _, [_;_] when c = Lazy.force coq_lt -> Kapp (Lt,args)
-    | _, [_;_] when c = Lazy.force coq_ge -> Kapp (Ge,args)
-    | _, [_;_] when c = Lazy.force coq_gt -> Kapp (Gt,args)
+    | _, [_;_;_] when eq_constr c (build_coq_eq ()) -> Kapp (Eq,args)
+    | _, [_;_] when eq_constr c (Lazy.force coq_neq) -> Kapp (Neq,args)
+    | _, [_;_] when eq_constr c (Lazy.force coq_Zne) -> Kapp (Zne,args)
+    | _, [_;_] when eq_constr c (Lazy.force coq_Zle) -> Kapp (Zle,args)
+    | _, [_;_] when eq_constr c (Lazy.force coq_Zlt) -> Kapp (Zlt,args)
+    | _, [_;_] when eq_constr c (Lazy.force coq_Zge) -> Kapp (Zge,args)
+    | _, [_;_] when eq_constr c (Lazy.force coq_Zgt) -> Kapp (Zgt,args)
+    | _, [_;_] when eq_constr c (build_coq_and ()) -> Kapp (And,args)
+    | _, [_;_] when eq_constr c (build_coq_or ()) -> Kapp (Or,args)
+    | _, [_;_] when eq_constr c (Lazy.force coq_iff) -> Kapp (Iff, args)
+    | _, [_] when eq_constr c (build_coq_not ()) -> Kapp (Not,args)
+    | _, [] when eq_constr c (build_coq_False ()) -> Kapp (False,args)
+    | _, [] when eq_constr c (build_coq_True ()) -> Kapp (True,args)
+    | _, [_;_] when eq_constr c (Lazy.force coq_le) -> Kapp (Le,args)
+    | _, [_;_] when eq_constr c (Lazy.force coq_lt) -> Kapp (Lt,args)
+    | _, [_;_] when eq_constr c (Lazy.force coq_ge) -> Kapp (Ge,args)
+    | _, [_;_] when eq_constr c (Lazy.force coq_gt) -> Kapp (Gt,args)
     | Const sp, args ->
-	Kapp (Other (string_of_id (basename_of_global (ConstRef sp))),args)
+	Kapp (Other (string_of_path (path_of_global (ConstRef sp))),args)
     | Construct csp , args ->
-	Kapp (Other (string_of_id (basename_of_global (ConstructRef csp))), args)
+	Kapp (Other (string_of_path (path_of_global (ConstructRef csp))), args)
     | Ind isp, args ->
-	Kapp (Other (string_of_id (basename_of_global (IndRef isp))),args)
+	Kapp (Other (string_of_path (path_of_global (IndRef isp))),args)
     | Var id,[] -> Kvar id
     | Prod (Anonymous,typ,body), [] -> Kimp(typ,body)
     | Prod (Name _,_,_),[] -> error "Omega: Not a quantifier-free goal"
@@ -410,43 +422,44 @@ let destructurate_prop t =
 let destructurate_type t =
   let c, args = decompose_app t in
   match kind_of_term c, args with
-    | _, [] when c = Lazy.force coq_Z -> Kapp (Z,args)
-    | _, [] when c = Lazy.force coq_nat -> Kapp (Nat,args)
+    | _, [] when eq_constr c (Lazy.force coq_Z) -> Kapp (Z,args)
+    | _, [] when eq_constr c (Lazy.force coq_nat) -> Kapp (Nat,args)
     | _ -> Kufo
 
 let destructurate_term t =
   let c, args = decompose_app t in
   match kind_of_term c, args with
-    | _, [_;_] when c = Lazy.force coq_Zplus -> Kapp (Zplus,args)
-    | _, [_;_] when c = Lazy.force coq_Zmult -> Kapp (Zmult,args)
-    | _, [_;_] when c = Lazy.force coq_Zminus -> Kapp (Zminus,args)
-    | _, [_] when c = Lazy.force coq_Zsucc -> Kapp (Zsucc,args)
-    | _, [_] when c = Lazy.force coq_Zopp -> Kapp (Zopp,args)
-    | _, [_;_] when c = Lazy.force coq_plus -> Kapp (Plus,args)
-    | _, [_;_] when c = Lazy.force coq_mult -> Kapp (Mult,args)
-    | _, [_;_] when c = Lazy.force coq_minus -> Kapp (Minus,args)
-    | _, [_] when c = Lazy.force coq_pred -> Kapp (Pred,args)
-    | _, [_] when c = Lazy.force coq_S -> Kapp (S,args)
-    | _, [] when c = Lazy.force coq_O -> Kapp (O,args)
-    | _, [_] when c = Lazy.force coq_Zpos -> Kapp (Zneg,args)
-    | _, [_] when c = Lazy.force coq_Zneg -> Kapp (Zpos,args)
-    | _, [] when c = Lazy.force coq_Z0 -> Kapp (Z0,args)
-    | _, [_] when c = Lazy.force coq_Z_of_nat -> Kapp (Z_of_nat,args)
+    | _, [_;_] when eq_constr c (Lazy.force coq_Zplus) -> Kapp (Zplus,args)
+    | _, [_;_] when eq_constr c (Lazy.force coq_Zmult) -> Kapp (Zmult,args)
+    | _, [_;_] when eq_constr c (Lazy.force coq_Zminus) -> Kapp (Zminus,args)
+    | _, [_] when eq_constr c (Lazy.force coq_Zsucc) -> Kapp (Zsucc,args)
+    | _, [_] when eq_constr c (Lazy.force coq_Zpred) -> Kapp (Zpred,args)
+    | _, [_] when eq_constr c (Lazy.force coq_Zopp) -> Kapp (Zopp,args)
+    | _, [_;_] when eq_constr c (Lazy.force coq_plus) -> Kapp (Plus,args)
+    | _, [_;_] when eq_constr c (Lazy.force coq_mult) -> Kapp (Mult,args)
+    | _, [_;_] when eq_constr c (Lazy.force coq_minus) -> Kapp (Minus,args)
+    | _, [_] when eq_constr c (Lazy.force coq_pred) -> Kapp (Pred,args)
+    | _, [_] when eq_constr c (Lazy.force coq_S) -> Kapp (S,args)
+    | _, [] when eq_constr c (Lazy.force coq_O) -> Kapp (O,args)
+    | _, [_] when eq_constr c (Lazy.force coq_Zpos) -> Kapp (Zneg,args)
+    | _, [_] when eq_constr c (Lazy.force coq_Zneg) -> Kapp (Zpos,args)
+    | _, [] when eq_constr c (Lazy.force coq_Z0) -> Kapp (Z0,args)
+    | _, [_] when eq_constr c (Lazy.force coq_Z_of_nat) -> Kapp (Z_of_nat,args)
     | Var id,[] -> Kvar id
     | _ -> Kufo
 
 let recognize_number t =
   let rec loop t =
     match decompose_app t with
-      | f, [t] when f = Lazy.force coq_xI -> one + two * loop t
-      | f, [t] when f = Lazy.force coq_xO -> two * loop t
-      | f, [] when f = Lazy.force coq_xH -> one
+      | f, [t] when eq_constr f (Lazy.force coq_xI) -> one + two * loop t
+      | f, [t] when eq_constr f (Lazy.force coq_xO) -> two * loop t
+      | f, [] when eq_constr f (Lazy.force coq_xH) -> one
       | _ -> failwith "not a number"
   in
   match decompose_app t with
-    | f, [t] when f = Lazy.force coq_Zpos -> loop t
-    | f, [t] when f = Lazy.force coq_Zneg -> neg (loop t)
-    | f, [] when f = Lazy.force coq_Z0 -> zero
+    | f, [t] when eq_constr f (Lazy.force coq_Zpos) -> loop t
+    | f, [t] when eq_constr f (Lazy.force coq_Zneg) -> neg (loop t)
+    | f, [] when eq_constr f (Lazy.force coq_Z0) -> zero
     | _ -> failwith "not a number"
 
 type constr_path =
@@ -891,6 +904,10 @@ let rec transform p t =
 	let tac,t = transform p (mkApp (Lazy.force coq_Zplus,
 					 [| t1; mk_integer one |])) in
 	unfold sp_Zsucc :: tac,t
+    | Kapp(Zpred,[t1]) ->
+	let tac,t = transform p (mkApp (Lazy.force coq_Zplus,
+					 [| t1; mk_integer negone |])) in
+	unfold sp_Zpred :: tac,t
    | Kapp(Zmult,[t1;t2]) ->
        let tac1,t1' = transform (P_APP 1 :: p) t1
        and tac2,t2' = transform (P_APP 2 :: p) t2 in
@@ -1548,6 +1565,38 @@ let nat_inject gl =
   in
   loop (List.rev (pf_hyps_types gl)) gl
 
+let dec_binop = function
+  | Zne -> coq_dec_Zne
+  | Zle -> coq_dec_Zle
+  | Zlt -> coq_dec_Zlt
+  | Zge -> coq_dec_Zge
+  | Zgt -> coq_dec_Zgt
+  | Le -> coq_dec_le
+  | Lt -> coq_dec_lt
+  | Ge -> coq_dec_ge
+  | Gt -> coq_dec_gt
+  | _ -> raise Not_found
+
+let not_binop = function
+  | Zne -> coq_not_Zne
+  | Zle -> coq_Znot_le_gt
+  | Zlt -> coq_Znot_lt_ge
+  | Zge -> coq_Znot_ge_lt
+  | Zgt -> coq_Znot_gt_le
+  | Le -> coq_not_le
+  | Lt -> coq_not_lt
+  | Ge -> coq_not_ge
+  | Gt -> coq_not_gt
+  | _ -> raise Not_found
+
+(** A decidability check : for some [t], could we build a term
+    of type [decidable t] (i.e. [t\/~t]) ? Otherwise, we raise
+    [Undecidable]. Note that a successful check implies that
+    [t] has type Prop.
+*)
+
+exception Undecidable
+
 let rec decidability gl t =
   match destructurate_prop t with
     | Kapp(Or,[t1;t2]) ->
@@ -1560,34 +1609,24 @@ let rec decidability gl t =
 	mkApp (Lazy.force coq_dec_iff, [| t1; t2;
 		  decidability gl t1; decidability gl t2 |])
     | Kimp(t1,t2) ->
-	mkApp (Lazy.force coq_dec_imp, [| t1; t2;
-		  decidability gl t1; decidability gl t2 |])
-    | Kapp(Not,[t1]) -> mkApp (Lazy.force coq_dec_not, [| t1;
-				    decidability gl t1 |])
+        (* This is the only situation where it's not obvious that [t]
+	   is in Prop. The recursive call on [t2] will ensure that. *)
+        mkApp (Lazy.force coq_dec_imp,
+		 [| t1; t2; decidability gl t1; decidability gl t2 |])
+    | Kapp(Not,[t1]) ->
+        mkApp (Lazy.force coq_dec_not, [| t1; decidability gl t1 |])
     | Kapp(Eq,[typ;t1;t2]) ->
 	begin match destructurate_type (pf_nf gl typ) with
           | Kapp(Z,[]) ->  mkApp (Lazy.force coq_dec_eq, [| t1;t2 |])
           | Kapp(Nat,[]) ->  mkApp (Lazy.force coq_dec_eq_nat, [| t1;t2 |])
-          | _ -> errorlabstrm "decidability"
-		(str "Omega: Can't solve a goal with equality on " ++
-		   Printer.pr_lconstr typ)
+          | _ -> raise Undecidable
 	end
-    | Kapp(Zne,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zne, [| t1;t2 |])
-    | Kapp(Zle,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zle, [| t1;t2 |])
-    | Kapp(Zlt,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zlt, [| t1;t2 |])
-    | Kapp(Zge,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zge, [| t1;t2 |])
-    | Kapp(Zgt,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zgt, [| t1;t2 |])
-    | Kapp(Le, [t1;t2]) -> mkApp (Lazy.force coq_dec_le, [| t1;t2 |])
-    | Kapp(Lt, [t1;t2]) -> mkApp (Lazy.force coq_dec_lt, [| t1;t2 |])
-    | Kapp(Ge, [t1;t2]) -> mkApp (Lazy.force coq_dec_ge, [| t1;t2 |])
-    | Kapp(Gt, [t1;t2]) -> mkApp (Lazy.force coq_dec_gt, [| t1;t2 |])
+    | Kapp(op,[t1;t2]) ->
+        (try mkApp (Lazy.force (dec_binop op), [| t1; t2 |])
+	 with Not_found -> raise Undecidable)
     | Kapp(False,[]) -> Lazy.force coq_dec_False
     | Kapp(True,[]) -> Lazy.force coq_dec_True
-    | Kapp(Other t,_::_) -> error
-	("Omega: Unrecognized predicate or connective: "^t)
-    | Kapp(Other t,[]) -> error ("Omega: Unrecognized atomic proposition: "^t)
-    | Kvar _ -> error "Omega: Can't solve a goal with proposition variables"
-    | _ -> error "Omega: Unrecognized proposition"
+    | _ -> raise Undecidable
 
 let onClearedName id tac =
   (* We cannot ensure that hyps can be cleared (because of dependencies), *)
@@ -1598,6 +1637,14 @@ let onClearedName id tac =
       let id = fresh_id [] id gl in
       tclTHEN (introduction id) (tac id) gl)
 
+let onClearedName2 id tac =
+  tclTHEN
+    (tclTRY (clear [id]))
+    (fun gl ->
+      let id1 = fresh_id [] (add_suffix id "_left") gl in
+      let id2 = fresh_id [] (add_suffix id "_right") gl in
+      tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ] gl)
+
 let destructure_hyps gl =
   let rec loop = function
     | [] -> (tclTHEN nat_inject coq_omega)
@@ -1611,50 +1658,24 @@ let destructure_hyps gl =
                 [ onClearedName i (fun i -> (loop ((i,None,t1)::lit)));
                   onClearedName i (fun i -> (loop ((i,None,t2)::lit))) ])
           | Kapp(And,[t1;t2]) ->
-              tclTHENLIST [
-                (elim_id i);
-		(tclTRY (clear [i]));
-		(fun gl ->
-		  let i1 = fresh_id [] (add_suffix i "_left") gl in
-		  let i2 = fresh_id [] (add_suffix i "_right") gl in
-		  tclTHENLIST [
-		    (introduction i1);
-		    (introduction i2);
-		    (loop ((i1,None,t1)::(i2,None,t2)::lit)) ] gl)
-	      ]
+              tclTHEN
+		(elim_id i)
+		(onClearedName2 i (fun i1 i2 ->
+		  loop ((i1,None,t1)::(i2,None,t2)::lit)))
           | Kapp(Iff,[t1;t2]) ->
-              tclTHENLIST [
-                (elim_id i);
-		(tclTRY (clear [i]));
-		(fun gl ->
-		  let i1 = fresh_id [] (add_suffix i "_left") gl in
-		  let i2 = fresh_id [] (add_suffix i "_right") gl in
-		  tclTHENLIST [
-		    introduction i1;
-		    generalize_tac
-		      [mkApp (Lazy.force coq_imp_simp,
-                        [| t1; t2; decidability gl t1; mkVar i1|])];
-		    onClearedName i1 (fun i1 ->
-		      tclTHENLIST [
-			introduction i2;
-			generalize_tac
-			  [mkApp (Lazy.force coq_imp_simp,
-                            [| t2; t1; decidability gl t2; mkVar i2|])];
-			onClearedName i2 (fun i2 ->
-			  loop
-			  ((i1,None,mk_or (mk_not t1) t2)::
-			   (i2,None,mk_or (mk_not t2) t1)::lit))
-		      ])] gl)
-	      ]
+	      tclTHEN
+		(elim_id i)
+		(onClearedName2 i (fun i1 i2 ->
+		  loop ((i1,None,mkArrow t1 t2)::(i2,None,mkArrow t2 t1)::lit)))
           | Kimp(t1,t2) ->
-              if
-                is_Prop (pf_type_of gl t1) &
-                is_Prop (pf_type_of gl t2) &
-                closed0 t2
+	      (* t1 and t2 might be in Type rather than Prop.
+		 For t1, the decidability check will ensure being Prop. *)
+              if is_Prop (pf_type_of gl t2)
               then
+		let d1 = decidability gl t1 in
 		tclTHENLIST [
 		  (generalize_tac [mkApp (Lazy.force coq_imp_simp,
-                    [| t1; t2; decidability gl t1; mkVar i|])]);
+                    [| t1; t2; d1; mkVar i|])]);
 		  (onClearedName i (fun i ->
 		    (loop ((i,None,mk_or (mk_not t1) t2)::lit))))
                 ]
@@ -1670,86 +1691,53 @@ let destructure_hyps gl =
                         (loop ((i,None,mk_and (mk_not t1) (mk_not t2)):: lit))))
                     ]
 		| Kapp(And,[t1;t2]) ->
+		    let d1 = decidability gl t1 in
                     tclTHENLIST [
 		      (generalize_tac
-		        [mkApp (Lazy.force coq_not_and, [| t1; t2;
-			  decidability gl t1; mkVar i|])]);
+		        [mkApp (Lazy.force coq_not_and,
+				[| t1; t2; d1; mkVar i |])]);
 		      (onClearedName i (fun i ->
                         (loop ((i,None,mk_or (mk_not t1) (mk_not t2))::lit))))
                     ]
 		| Kapp(Iff,[t1;t2]) ->
+		    let d1 = decidability gl t1 in
+		    let d2 = decidability gl t2 in
                     tclTHENLIST [
 		      (generalize_tac
-		        [mkApp (Lazy.force coq_not_iff, [| t1; t2;
-			  decidability gl t1; decidability gl t2; mkVar i|])]);
+		        [mkApp (Lazy.force coq_not_iff,
+				[| t1; t2; d1; d2; mkVar i |])]);
 		      (onClearedName i (fun i ->
                         (loop ((i,None,
 			        mk_or (mk_and t1 (mk_not t2))
 				      (mk_and (mk_not t1) t2))::lit))))
                     ]
 		| Kimp(t1,t2) ->
+		    (* t2 must be in Prop otherwise ~(t1->t2) wouldn't be ok.
+		       For t1, being decidable implies being Prop. *)
+		    let d1 = decidability gl t1 in
                     tclTHENLIST [
 		      (generalize_tac
-		        [mkApp (Lazy.force coq_not_imp, [| t1; t2;
-		          decidability gl t1;mkVar i |])]);
+		        [mkApp (Lazy.force coq_not_imp,
+				[| t1; t2; d1; mkVar i |])]);
 		      (onClearedName i (fun i ->
                         (loop ((i,None,mk_and t1 (mk_not t2)) :: lit))))
                     ]
 		| Kapp(Not,[t]) ->
+		    let d = decidability gl t in
                     tclTHENLIST [
 		      (generalize_tac
-			[mkApp (Lazy.force coq_not_not, [| t;
-			  decidability gl t; mkVar i |])]);
+			[mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]);
 		      (onClearedName i (fun i -> (loop ((i,None,t)::lit))))
                     ]
-		| Kapp(Zle, [t1;t2]) ->
-                    tclTHENLIST [
-		      (generalize_tac
-                        [mkApp (Lazy.force coq_Znot_le_gt, [| t1;t2;mkVar i|])]);
-		      (onClearedName i (fun _ -> loop lit))
-                    ]
-		| Kapp(Zge, [t1;t2]) ->
-                    tclTHENLIST [
-		      (generalize_tac
-                        [mkApp (Lazy.force coq_Znot_ge_lt, [| t1;t2;mkVar i|])]);
-		      (onClearedName i (fun _ -> loop lit))
-                    ]
-		| Kapp(Zlt, [t1;t2]) ->
-                    tclTHENLIST [
-		      (generalize_tac
-                        [mkApp (Lazy.force coq_Znot_lt_ge, [| t1;t2;mkVar i|])]);
-		      (onClearedName i (fun _ -> loop lit))
-                    ]
-		| Kapp(Zgt, [t1;t2]) ->
-                    tclTHENLIST [
-		      (generalize_tac
-                        [mkApp (Lazy.force coq_Znot_gt_le, [| t1;t2;mkVar i|])]);
-		      (onClearedName i (fun _ -> loop lit))
-                    ]
-		| Kapp(Le, [t1;t2]) ->
-                    tclTHENLIST [
-		      (generalize_tac
-                        [mkApp (Lazy.force coq_not_le, [| t1;t2;mkVar i|])]);
-		      (onClearedName i (fun _ -> loop lit))
-                    ]
-		| Kapp(Ge, [t1;t2]) ->
-                    tclTHENLIST [
-		      (generalize_tac
-                        [mkApp (Lazy.force coq_not_ge, [| t1;t2;mkVar i|])]);
-		      (onClearedName i (fun _ -> loop lit))
-                    ]
-		| Kapp(Lt, [t1;t2]) ->
-                    tclTHENLIST [
-		      (generalize_tac
-                        [mkApp (Lazy.force coq_not_lt, [| t1;t2;mkVar i|])]);
-		      (onClearedName i (fun _ -> loop lit))
-                    ]
-		| Kapp(Gt, [t1;t2]) ->
-                    tclTHENLIST [
-		      (generalize_tac
-                        [mkApp (Lazy.force coq_not_gt, [| t1;t2;mkVar i|])]);
-		      (onClearedName i (fun _ -> loop lit))
-                    ]
+		| Kapp(op,[t1;t2]) ->
+		    (try
+		      let thm = not_binop op in
+                      tclTHENLIST [
+			(generalize_tac
+			   [mkApp (Lazy.force thm, [| t1;t2;mkVar i|])]);
+			(onClearedName i (fun _ -> loop lit))
+                      ]
+		     with Not_found -> loop lit)
 		| Kapp(Eq,[typ;t1;t2]) ->
                     if !old_style_flag then begin
 		      match destructurate_type (pf_nf gl typ) with
@@ -1787,7 +1775,9 @@ let destructure_hyps gl =
 		| _ -> loop lit
               end
           | _ -> loop lit
-	with e when catchable_exception e -> loop lit
+	with
+	  | Undecidable -> loop lit
+	  | e when catchable_exception e -> loop lit
 	end
   in
   loop (pf_hyps gl) gl
@@ -1803,13 +1793,16 @@ let destructure_goal gl =
       | Kimp(a,b) -> (tclTHEN intro (loop b))
       | Kapp(False,[]) -> destructure_hyps
       | _ ->
-          (tclTHEN
-	     (tclTHEN
-		(Tactics.refine
-		   (mkApp (Lazy.force coq_dec_not_not, [| t;
-			      decidability gl t; mkNewMeta () |])))
-		intro)
-	     (destructure_hyps))
+	let goal_tac =
+	  try
+	    let dec = decidability gl t in
+	    tclTHEN
+	      (Tactics.refine
+		 (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |])))
+	      intro
+	  with Undecidable -> Tactics.elim_type (build_coq_False ())
+	in
+	tclTHEN goal_tac destructure_hyps
   in
   (loop concl) gl
 
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index cd6472c3..84cc8464 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -15,8 +15,6 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: g_omega.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Coq_omega
 open Refiner
 
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
index 8bb10194..3a5aece7 100644
--- a/plugins/omega/omega.ml
+++ b/plugins/omega/omega.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -214,7 +214,7 @@ let rec display_action print_var = function
             constant factors.\n" e1.id e2.id
       | NEGATE_CONTRADICT(e1,e2,b) ->
           Printf.printf
-            "Equations E%d and E%d state that their body is at the same time
+            "Equations E%d and E%d state that their body is at the same time \
             equal and different\n" e1.id e2.id
       | CONSTANT_NOT_NUL (e,k) ->
           Printf.printf "Equation E%d states %s = 0.\n" e (sbi k)