reparation Zne

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

3 files changed, 7 insertions, 5 deletions

diff --git a/contrib/romega/ROmega.v b/contrib/romega/ROmega.v
index 0a140faf54..2a9dc10070 100644
--- a/contrib/romega/ROmega.v
+++ b/contrib/romega/ROmega.v
@@ -9,11 +9,9 @@
 Require Omega.
 Require ReflOmegaCore.
 
-Declare ML Module "const_omega".
-Declare ML Module "refl_omega".
-
 Grammar tactic simple_tactic : ast :=
   romega [ "ROmega" ] -> [(ReflOmega)].
 
 Syntax tactic level 0:
-  romega [ << (ReflOmega) >> ] -> ["ROmega"].        
+  romega [ << (ReflOmega) >> ] -> ["ROmega"].   
+     
diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml
index 4c8dcca1b9..9d7330a940 100644
--- a/contrib/romega/const_omega.ml
+++ b/contrib/romega/const_omega.ml
@@ -7,7 +7,7 @@
  *************************************************************************)
 
 let module_refl_name = "ReflOmegaCore"
-let module_refl_path = ["Scratch"; module_refl_name]
+let module_refl_path = ["Coq"; "romega"; module_refl_name]
 
 type result = 
    Kvar of string
diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml
index 3974ab39c7..f92e77e8b3 100644
--- a/contrib/romega/refl_omega.ml
+++ b/contrib/romega/refl_omega.ml
@@ -367,6 +367,9 @@ let rec ocompile env t =
       let t1',env1 = ocompile env t1 in
       let t2',env2 = ocompile env1 t2 in
       (Otimes (t1',t2'), env2)
+  | Kapp("Zs",[t]) ->  
+      let t',env = ocompile env  t in
+       (Oplus (t',Oz(1)), env)
   | Kapp(("POS"|"NEG"|"ZERO"),_) -> 
       begin try (Oz(recognize_number t),env) 
       with _ -> 
@@ -853,3 +856,4 @@ let omega_solver gl =
   (loop concl) gl
 
 let omega = hide_atomic_tactic "ReflOmega" omega_solver
+