[omega] Remove dead code

1 files changed, 1 insertions, 27 deletions

diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index f55458de8d..446e71b40c 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -42,7 +42,6 @@ let elim_id id = simplest_elim (mkVar id)
 
 let resolve_id id = apply (mkVar id)
 
-let display_time_flag = ref false
 let display_system_flag = ref false
 let display_action_flag = ref false
 let old_style_flag = ref false
@@ -114,10 +113,6 @@ let new_identifier =
   let cpt = intref 0 in
   (fun () -> let s = "Omega" ^ string_of_int !cpt in incr cpt; Id.of_string s)
 
-let new_identifier_state =
-  let cpt = intref 0 in
-  (fun () -> let s = make_ident "State" (Some !cpt) in incr cpt; s)
-
 let new_identifier_var =
   let cpt = intref 0 in
   (fun () -> let s = "Zvar" ^ string_of_int !cpt in incr cpt; Id.of_string s)
@@ -153,7 +148,6 @@ let mk_then tacs = tclTHENLIST tacs
 let exists_tac c = constructor_tac false (Some 1) 1 (ImplicitBindings [c])
 
 let generalize_tac t = generalize t
-let elim t = simplest_elim t
 let unfold s = Tactics.unfold_in_concl [Locus.AllOccurrences, Lazy.force s]
 let pf_nf gl c = pf_apply Tacred.simpl gl c
 
@@ -165,10 +159,9 @@ let rev_assoc k =
   in
   loop
 
-let tag_hypothesis,tag_of_hyp, hyp_of_tag, clear_tags =
+let tag_hypothesis, hyp_of_tag, clear_tags =
   let l = ref ([]:(Id.t * int) list) in
   (fun h id -> l := (h,id):: !l),
-  (fun h -> try Id.List.assoc h !l with Not_found -> failwith "tag_hypothesis"),
   (fun h -> try rev_assoc h !l with Not_found -> failwith "tag_hypothesis"),
   (fun () -> l := [])
 
@@ -363,23 +356,18 @@ let sp_Zpred =     lazy (evaluable_ref_of_constr "Z.pred" coq_Zpred)
 let sp_Zminus = lazy (evaluable_ref_of_constr "Z.sub" coq_Zminus)
 let sp_Zle = lazy (evaluable_ref_of_constr "Z.le" coq_Zle)
 let sp_Zgt = lazy (evaluable_ref_of_constr "Z.gt" coq_Zgt)
-let sp_Zge = lazy (evaluable_ref_of_constr "Z.ge" coq_Zge)
-let sp_Zlt = lazy (evaluable_ref_of_constr "Z.lt" coq_Zlt)
 let sp_not = lazy (evaluable_ref_of_constr "not" coq_not)
 
-let mk_var v = mkVar (Id.of_string v)
 let mk_plus t1 t2 = mkApp (Lazy.force coq_Zplus, [| t1; t2 |])
 let mk_times t1 t2 = mkApp (Lazy.force coq_Zmult, [| t1; t2 |])
 let mk_minus t1 t2 = mkApp (Lazy.force coq_Zminus, [| t1;t2 |])
 let mk_gen_eq ty t1 t2 = mkApp (Lazy.force coq_eq, [| ty; t1; t2 |])
 let mk_eq t1 t2 = mk_gen_eq (Lazy.force coq_Z) t1 t2
-let mk_le t1 t2 = mkApp (Lazy.force coq_Zle, [| t1; t2 |])
 let mk_gt t1 t2 = mkApp (Lazy.force coq_Zgt, [| t1; t2 |])
 let mk_inv t = mkApp (Lazy.force coq_Zopp, [| t |])
 let mk_and t1 t2 =  mkApp (Lazy.force coq_and, [| t1; t2 |])
 let mk_or t1 t2 =  mkApp (Lazy.force coq_or, [| t1; t2 |])
 let mk_not t = mkApp (Lazy.force coq_not, [| t |])
-let mk_eq_rel t1 t2 = mk_gen_eq (Lazy.force coq_comparison) t1 t2
 let mk_inj t = mkApp (Lazy.force coq_Z_of_nat, [| t |])
 
 let mk_integer n =
@@ -403,10 +391,6 @@ type omega_constant =
   | Le | Lt | Ge | Gt
   | Other of string
 
-type omega_proposition =
-  | Keq of constr * constr * constr
-  | Kn
-
 type result =
   | Kvar of Id.t
   | Kapp of omega_constant * constr list
@@ -584,7 +568,6 @@ let focused_simpl path = focused_simpl path
 
 type oformula =
   | Oplus of oformula * oformula
-  | Oinv of  oformula
   | Otimes of oformula * oformula
   | Oatom of Id.t
   | Oz of bigint
@@ -594,7 +577,6 @@ let rec oprint = function
   | Oplus(t1,t2) ->
       print_string "("; oprint t1; print_string "+";
       oprint t2; print_string ")"
-  | Oinv t -> print_string "~"; oprint t
   | Otimes (t1,t2) ->
       print_string "("; oprint t1; print_string "*";
       oprint t2; print_string ")"
@@ -605,7 +587,6 @@ let rec oprint = function
 let rec weight = function
   | Oatom c -> intern_id c
   | Oz _ -> -1
-  | Oinv c -> weight c
   | Otimes(c,_) -> weight c
   | Oplus _ -> failwith "weight"
   | Oufo _ -> -1
@@ -613,7 +594,6 @@ let rec weight = function
 let rec val_of = function
   | Oatom c -> mkVar c
   | Oz c -> mk_integer c
-  | Oinv c -> mkApp (Lazy.force coq_Zopp, [| val_of c |])
   | Otimes (t1,t2) -> mkApp (Lazy.force coq_Zmult, [| val_of t1; val_of t2 |])
   | Oplus(t1,t2) -> mkApp (Lazy.force coq_Zplus, [| val_of t1; val_of t2 |])
   | Oufo c -> c
@@ -908,10 +888,6 @@ let rec scalar p n = function
       clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2]]
         (Lazy.force coq_fast_Zmult_plus_distr_l) ::
       (tac1 @ tac2), Oplus(t1',t2')
-  | Oinv t ->
-      [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]]
-	 (Lazy.force coq_fast_Zmult_opp_comm);
-       focused_simpl (P_APP 2 :: p)], Otimes(t,Oz(neg n))
   | Otimes(t1,Oz x) ->
       [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2]]
          (Lazy.force coq_fast_Zmult_assoc_reverse);
@@ -963,8 +939,6 @@ let rec negate p = function
         (Lazy.force coq_fast_Zopp_plus_distr) ::
       (tac1 @ tac2),
       Oplus(t1',t2')
-  | Oinv t ->
-      [clever_rewrite p [[P_APP 1;P_APP 1]] (Lazy.force coq_fast_Zopp_involutive)], t
   | Otimes(t1,Oz x) ->
       [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2]]
          (Lazy.force coq_fast_Zopp_mult_distr_r);