From 90d64647d3fd5dbf5c337944dc0038f0b19b8a51 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 17 Jun 2014 14:26:02 +0200
Subject: Removing dead code.

---
 plugins/cc/ccproof.ml | 1 -
 plugins/cc/cctac.ml   | 2 --
 2 files changed, 3 deletions(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index 4e1806f5a..6177f22f3 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -10,7 +10,6 @@
 (* proof-trees that will be transformed into proof-terms in cctac.ml4   *)
 
 open Errors
-open Names
 open Term
 open Ccalgo
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 2de0fe717..73c050bb2 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -468,8 +468,6 @@ let congruence_tac depth l =
    might be slow now, let's rather do something equivalent
    to a "simple apply refl_equal" *)
 
-let simple_reflexivity () = apply (Universes.constr_of_global _refl_equal)
-
 (* The [f_equal] tactic.
 
    It mimics the use of lemmas [f_equal], [f_equal2], etc.
-- 
cgit v1.2.3