diff options
| author | Pierre-Marie Pédrot | 2018-11-12 16:52:36 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-12 16:52:36 +0100 |
| commit | 040fdec17f7e70fdbef7d400be2dc0e1607a10fa (patch) | |
| tree | 0616768175db18596abbcad32fa1f48f70aae356 /plugins/firstorder/rules.ml | |
| parent | 78ab6a5263d3d0dd4da300fcfb87c5e896acc153 (diff) | |
| parent | 3c940f8e88e8d57681431c483e6d3e41114c8cc8 (diff) | |
Merge PR #8938: [Plugins] Remove some dead code
Diffstat (limited to 'plugins/firstorder/rules.ml')
| -rw-r--r-- | plugins/firstorder/rules.ml | 21 |
1 files changed, 0 insertions, 21 deletions
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index b0c4785d7a..832a98b7f8 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -21,7 +21,6 @@ open Termops open Formula open Sequent open Globnames -open Locus module NamedDecl = Context.Named.Declaration @@ -56,10 +55,6 @@ let wrap n b continue seq = continue seq2 end -let basename_of_global=function - VarRef id->id - | _->assert false - let clear_global=function VarRef id-> clear [id] | _->tclIDTAC @@ -230,19 +225,3 @@ let ll_forall_tac prod backtrack id continue seq= backtrack (* rules for instantiation with unification moved to instances.ml *) - -(* special for compatibility with old Intuition *) - -let constant str = Coqlib.lib_ref str - -let defined_connectives = lazy - [AllOccurrences, EvalConstRef (destConstRef (constant "core.not.type")); - AllOccurrences, EvalConstRef (destConstRef (constant "core.iff.type"))] - -let normalize_evaluables= - Proofview.Goal.enter begin fun gl -> - unfold_in_concl (Lazy.force defined_connectives) <*> - tclMAP - (fun id -> unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly)) - (pf_ids_of_hyps gl) - end |