diff options
| author | letouzey | 2007-07-13 16:47:34 +0000 |
|---|---|---|
| committer | letouzey | 2007-07-13 16:47:34 +0000 |
| commit | 72cd18d711b3e9ea2ecb0d657187dc5febfbc8e3 (patch) | |
| tree | 221bf8bfeaf71662bb12287e4fc52ca44a436c87 /contrib | |
| parent | f25f87bdfa79fc59918d2f15a6b9aedbcf8d479a (diff) | |
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
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/romega/const_omega.ml | 2 | ||||
| -rw-r--r-- | contrib/romega/const_omega.mli | 5 |
2 files changed, 1 insertions, 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 |