diff options
| author | Vincent Laporte | 2018-11-07 11:43:59 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-11-07 16:08:28 +0000 |
| commit | 61a070f7e6c13729f2ee879b6a419353049b1ea7 (patch) | |
| tree | cf03a316c818af3115e7a39e1d833076308c3206 /plugins/firstorder/rules.ml | |
| parent | ce4d0cb7803a4eb7269026409979a0b046d35552 (diff) | |
[Firstorder plugin] 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 |