diff options
Diffstat (limited to 'plugins/firstorder/rules.ml')
| -rw-r--r-- | plugins/firstorder/rules.ml | 28 |
1 files changed, 3 insertions, 25 deletions
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 8fa676de44..7f06ab6777 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 @@ -168,9 +163,9 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq = let ll_arrow_tac a b c backtrack id continue seq= let open EConstr in let open Vars in - let cc=mkProd(Anonymous,a,(lift 1 b)) in - let d idc = mkLambda (Anonymous,b, - mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in + let cc=mkProd(Context.make_annot Anonymous Sorts.Relevant,a,(lift 1 b)) in + let d idc = mkLambda (Context.make_annot Anonymous Sorts.Relevant,b, + mkApp (idc, [|mkLambda (Context.make_annot Anonymous Sorts.Relevant,(lift 1 a),(mkRel 2))|])) in tclORELSE (tclTHENS (cut c) [tclTHENLIST @@ -230,20 +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 = UnivGen.constr_of_global - @@ Coqlib.lib_ref str - -let defined_connectives = lazy - [AllOccurrences, EvalConstRef (fst (Constr.destConst (constant "core.not.type"))); - AllOccurrences, EvalConstRef (fst (Constr.destConst (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 |