From 72cd18d711b3e9ea2ecb0d657187dc5febfbc8e3 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 13 Jul 2007 16:47:34 +0000
Subject: some more useless constant in const_omega

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10001 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/romega/const_omega.ml  | 2 --
 contrib/romega/const_omega.mli | 5 +----
 2 files changed, 1 insertion(+), 6 deletions(-)

diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml
index 90d6c584e6..6303605db3 100644
--- a/contrib/romega/const_omega.ml
+++ b/contrib/romega/const_omega.ml
@@ -76,7 +76,6 @@ let coq_p_left = lazy (constant  "P_LEFT")
 let coq_p_right = lazy (constant  "P_RIGHT")
 let coq_p_invert = lazy (constant  "P_INVERT")
 let coq_p_step = lazy (constant  "P_STEP")
-let coq_p_nop = lazy (constant  "P_NOP")
 
 let coq_t_int = lazy (constant  "Tint")
 let coq_t_plus = lazy (constant  "Tplus")
@@ -108,7 +107,6 @@ let coq_f_left =  lazy (constant  "F_left")
 let coq_f_right =  lazy (constant  "F_right")
 
 (* Constructors for reordering tactics *)
-let coq_step = lazy (constant  "step")
 let coq_c_do_both = lazy (constant  "C_DO_BOTH")
 let coq_c_do_left = lazy (constant  "C_LEFT")
 let coq_c_do_right = lazy (constant  "C_RIGHT")
diff --git a/contrib/romega/const_omega.mli b/contrib/romega/const_omega.mli
index 04b26463a8..0f00e9184a 100644
--- a/contrib/romega/const_omega.mli
+++ b/contrib/romega/const_omega.mli
@@ -10,7 +10,6 @@
 (** Coq objects used in romega *)
 
 (* from Logic *)
-val coq_eq : Term.constr lazy_t
 val coq_refl_equal : Term.constr lazy_t
 val coq_and : Term.constr lazy_t
 val coq_not : Term.constr lazy_t
@@ -26,7 +25,6 @@ val coq_p_left : Term.constr lazy_t
 val coq_p_right : Term.constr lazy_t
 val coq_p_invert : Term.constr lazy_t
 val coq_p_step : Term.constr lazy_t
-val coq_p_nop : Term.constr lazy_t
 
 val coq_t_int : Term.constr lazy_t
 val coq_t_plus : Term.constr lazy_t
@@ -50,13 +48,11 @@ val coq_p_and : Term.constr lazy_t
 val coq_p_imp : Term.constr lazy_t
 val coq_p_prop : Term.constr lazy_t
 
-val coq_t_fusion : Term.constr lazy_t
 val coq_f_equal : Term.constr lazy_t
 val coq_f_cancel : Term.constr lazy_t
 val coq_f_left : Term.constr lazy_t
 val coq_f_right : Term.constr lazy_t
 
-val coq_step : Term.constr lazy_t
 val coq_c_do_both : Term.constr lazy_t
 val coq_c_do_left : Term.constr lazy_t
 val coq_c_do_right : Term.constr lazy_t
@@ -108,6 +104,7 @@ val coq_d_mono : Term.constr lazy_t
 val coq_e_split : Term.constr lazy_t
 val coq_e_extract : Term.constr lazy_t
 val coq_e_solve : Term.constr lazy_t
+
 val coq_interp_sequent : Term.constr lazy_t
 val coq_do_omega : Term.constr lazy_t
 
-- 
cgit v1.2.3