From 118d24281bc62bb7ff503abee56f156545eb9eea Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 10 Mar 2018 23:54:14 +0100 Subject: [api] Remove deprecated object from `Term` We remove most of what was deprecated in `Term`. Now, `intf` and `kernel` are almost deprecation-free, tho I am not very convinced about the whole `Term -> Constr` renaming but I'm afraid there is no way back. Inconsistencies with the constructor policy (see #6440) remain along the code-base and I'm afraid I don't see a plan to reconcile them. The `Sorts` deprecation is hard to finalize, opening `Sorts` is not a good idea as someone added a `List` module inside it. --- plugins/btauto/refl_btauto.ml | 26 +++++++++++++++++++------- plugins/firstorder/unify.ml | 2 +- plugins/funind/glob_termops.ml | 3 ++- plugins/funind/indfun_common.ml | 2 +- plugins/ltac/evar_tactics.ml | 2 +- plugins/ltac/extratactics.ml4 | 2 +- plugins/ltac/g_auto.ml4 | 3 ++- plugins/ltac/tauto.ml | 2 +- plugins/micromega/coq_micromega.ml | 36 ++++++++++++++++++------------------ plugins/omega/coq_omega.ml | 2 +- plugins/romega/refl_omega.ml | 5 +++-- plugins/ssr/ssrcommon.ml | 8 ++++---- plugins/ssr/ssrelim.ml | 1 + plugins/ssr/ssripats.ml | 19 ++++++++++--------- plugins/ssr/ssrparser.ml4 | 4 ++-- plugins/ssr/ssrtacticals.ml | 7 ++++--- 16 files changed, 71 insertions(+), 53 deletions(-) (limited to 'plugins') diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 7f98ed427..c2bc8c079 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -1,3 +1,15 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* + | App (head, args) -> if head === andb && Array.length args = 2 then Andb (aux args.(0), aux args.(1)) else if head === orb && Array.length args = 2 then @@ -116,9 +128,9 @@ module Bool = struct else if head === negb && Array.length args = 1 then Negb (aux args.(0)) else Var (Env.add env c) - | Term.Case (info, r, arg, pats) -> + | Case (info, r, arg, pats) -> let is_bool = - let i = info.Term.ci_ind in + let i = info.ci_ind in Names.eq_ind i (Lazy.force ind) in if is_bool then @@ -176,9 +188,9 @@ module Btauto = struct let _, var = Tacmach.pf_reduction_of_red_expr gl (Genredexpr.CbvVm None) var in let var = EConstr.Unsafe.to_constr var in let rec to_list l = match decomp_term (Tacmach.project gl) l with - | Term.App (c, _) + | App (c, _) when c === (Lazy.force CoqList._nil) -> [] - | Term.App (c, [|_; h; t|]) + | App (c, [|_; h; t|]) when c === (Lazy.force CoqList._cons) -> if h === (Lazy.force Bool.trueb) then (true :: to_list t) else if h === (Lazy.force Bool.falseb) then (false :: to_list t) @@ -218,7 +230,7 @@ module Btauto = struct let concl = EConstr.Unsafe.to_constr concl in let t = decomp_term (Tacmach.New.project gl) concl in match t with - | Term.App (c, [|typ; p; _|]) when c === eq -> + | App (c, [|typ; p; _|]) when c === eq -> (* should be an equality [@eq poly ?p (Cst false)] *) let tac = Tacticals.New.tclORELSE0 Tactics.reflexivity (Proofview.V82.tactic (print_counterexample p env)) in tac @@ -236,7 +248,7 @@ module Btauto = struct let bool = Lazy.force Bool.typ in let t = decomp_term sigma concl in match t with - | Term.App (c, [|typ; tl; tr|]) + | App (c, [|typ; tl; tr|]) when typ === bool && c === eq -> let env = Env.empty () in let fl = Bool.quote env sigma tl in diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index b869c04a2..06f56d06e 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -9,7 +9,7 @@ (************************************************************************) open Util -open Term +open Constr open EConstr open Vars open Termops diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index ae238b846..bb1587507 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -1,4 +1,5 @@ open Pp +open Constr open Glob_term open CErrors open Util @@ -16,7 +17,7 @@ let mkGApp(rt,rtl) = DAst.make @@ GApp(rt,rtl) let mkGLambda(n,t,b) = DAst.make @@ GLambda(n,Explicit,t,b) let mkGProd(n,t,b) = DAst.make @@ GProd(n,Explicit,t,b) let mkGLetIn(n,b,t,c) = DAst.make @@ GLetIn(n,b,t,c) -let mkGCases(rto,l,brl) = DAst.make @@ GCases(Term.RegularStyle,rto,l,brl) +let mkGCases(rto,l,brl) = DAst.make @@ GCases(RegularStyle,rto,l,brl) let mkGHole () = DAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None) (* diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index b0c9ff8fc..c6faa142a 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -109,7 +109,7 @@ let const_of_id id = let def_of_const t = match Constr.kind t with - Term.Const sp -> + Const sp -> (try (match Environ.constant_opt_value_in (Global.env()) sp with | Some c -> c | _ -> assert false) diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index 5463893ad..ea8dcf57d 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -10,7 +10,7 @@ open Util open Names -open Term +open Constr open CErrors open Evar_refiner open Tacmach diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 17011f206..c5254b37c 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -9,6 +9,7 @@ (************************************************************************) open Pp +open Constr open Genarg open Stdarg open Tacarg @@ -286,7 +287,6 @@ END (**********************************************************************) (* Hint Resolve *) -open Term open EConstr open Vars open Coqlib diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 07047d016..642e52155 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -9,6 +9,7 @@ (************************************************************************) open Pp +open Constr open Genarg open Stdarg open Pcoq.Prim @@ -169,7 +170,7 @@ END TACTIC EXTEND convert_concl_no_check -| ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x Term.DEFAULTcast ] +| ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x DEFAULTcast ] END let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_reference diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index a51c09ca4..8eeb8903e 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Term +open Constr open EConstr open Hipattern open Names diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 4c0357dd8..c7abd58b0 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -19,10 +19,10 @@ (************************************************************************) open Pp -open Mutils -open Goptions open Names open Constr +open Goptions +open Mutils (** * Debug flag @@ -601,10 +601,10 @@ struct let get_left_construct sigma term = match EConstr.kind sigma term with - | Term.Construct((_,i),_) -> (i,[| |]) - | Term.App(l,rst) -> + | Construct((_,i),_) -> (i,[| |]) + | App(l,rst) -> (match EConstr.kind sigma l with - | Term.Construct((_,i),_) -> (i,rst) + | Construct((_,i),_) -> (i,rst) | _ -> raise ParseError ) | _ -> raise ParseError @@ -688,7 +688,7 @@ struct let parse_q sigma term = match EConstr.kind sigma term with - | Term.App(c, args) -> if EConstr.eq_constr sigma c (Lazy.force coq_Qmake) then + | App(c, args) -> if EConstr.eq_constr sigma c (Lazy.force coq_Qmake) then {Mc.qnum = parse_z sigma args.(0) ; Mc.qden = parse_positive sigma args.(1) } else raise ParseError | _ -> raise ParseError @@ -904,8 +904,8 @@ struct let parse_zop gl (op,args) = let sigma = gl.sigma in match EConstr.kind sigma op with - | Term.Const (x,_) -> (assoc_const sigma op zop_table, args.(0) , args.(1)) - | Term.Ind((n,0),_) -> + | Const (x,_) -> (assoc_const sigma op zop_table, args.(0) , args.(1)) + | Ind((n,0),_) -> if EConstr.eq_constr sigma op (Lazy.force coq_Eq) && is_convertible gl args.(0) (Lazy.force coq_Z) then (Mc.OpEq, args.(1), args.(2)) else raise ParseError @@ -914,8 +914,8 @@ struct let parse_rop gl (op,args) = let sigma = gl.sigma in match EConstr.kind sigma op with - | Term.Const (x,_) -> (assoc_const sigma op rop_table, args.(0) , args.(1)) - | Term.Ind((n,0),_) -> + | Const (x,_) -> (assoc_const sigma op rop_table, args.(0) , args.(1)) + | Ind((n,0),_) -> if EConstr.eq_constr sigma op (Lazy.force coq_Eq) && is_convertible gl args.(0) (Lazy.force coq_R) then (Mc.OpEq, args.(1), args.(2)) else raise ParseError @@ -926,7 +926,7 @@ struct let is_constant sigma t = (* This is an approx *) match EConstr.kind sigma t with - | Term.Construct(i,_) -> true + | Construct(i,_) -> true | _ -> false type 'a op = @@ -1011,10 +1011,10 @@ struct try (Mc.PEc (parse_constant term) , env) with ParseError -> match EConstr.kind sigma term with - | Term.App(t,args) -> + | App(t,args) -> ( match EConstr.kind sigma t with - | Term.Const c -> + | Const c -> ( match assoc_ops sigma t ops_spec with | Binop f -> combine env f (args.(0),args.(1)) | Opp -> let (expr,env) = parse_expr env args.(0) in @@ -1077,13 +1077,13 @@ struct let rec rconstant sigma term = match EConstr.kind sigma term with - | Term.Const x -> + | Const x -> if EConstr.eq_constr sigma term (Lazy.force coq_R0) then Mc.C0 else if EConstr.eq_constr sigma term (Lazy.force coq_R1) then Mc.C1 else raise ParseError - | Term.App(op,args) -> + | App(op,args) -> begin try (* the evaluation order is important in the following *) @@ -1153,7 +1153,7 @@ struct if debug then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr_env gl.env sigma cstr ++ fnl ()); match EConstr.kind sigma cstr with - | Term.App(op,args) -> + | App(op,args) -> let (op,lhs,rhs) = parse_op gl (op,args) in let (e1,env) = parse_expr sigma env lhs in let (e2,env) = parse_expr sigma env rhs in @@ -1208,7 +1208,7 @@ struct let rec xparse_formula env tg term = match EConstr.kind sigma term with - | Term.App(l,rst) -> + | App(l,rst) -> (match rst with | [|a;b|] when EConstr.eq_constr sigma l (Lazy.force coq_and) -> let f,env,tg = xparse_formula env tg a in @@ -1225,7 +1225,7 @@ struct let g,env,tg = xparse_formula env tg b in mkformula_binary mkIff term f g,env,tg | _ -> parse_atom env tg term) - | Term.Prod(typ,a,b) when EConstr.Vars.noccurn sigma 1 b -> + | Prod(typ,a,b) when EConstr.Vars.noccurn sigma 1 b -> let f,env,tg = xparse_formula env tg a in let g,env,tg = xparse_formula env tg b in mkformula_binary mkI term f g,env,tg diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 3594c8765..c615cf278 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -18,8 +18,8 @@ open CErrors open Util open Names +open Constr open Nameops -open Term open EConstr open Tacticals.New open Tacmach.New diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index d18249784..e60348065 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -8,6 +8,7 @@ open Pp open Util +open Constr open Const_omega module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint) open OmegaSolver @@ -1036,13 +1037,13 @@ let resolution unsafe sigma env (reified_concl,reified_hyps) systems_list = let decompose_tactic = decompose_tree env context solution_tree in Tactics.generalize (l_generalize_arg @ l_reified_hypnames) >> - Tactics.convert_concl_no_check reified Term.DEFAULTcast >> + Tactics.convert_concl_no_check reified DEFAULTcast >> Tactics.apply (app coq_do_omega [|decompose_tactic|]) >> show_goal >> (if unsafe then (* Trust the produced term. Faster, but might fail later at Qed. Also handy when debugging, e.g. via a Show Proof after romega. *) - Tactics.convert_concl_no_check (Lazy.force coq_True) Term.VMcast + Tactics.convert_concl_no_check (Lazy.force coq_True) VMcast else Tactics.normalise_vm_in_concl) >> Tactics.apply (Lazy.force coq_I) diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index c0026616d..3f6503e73 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -423,12 +423,12 @@ let mk_anon_id t gl_ids = (set s i (Char.chr (Char.code (get s i) + 1)); s) in Id.of_bytes (loop (n - 1)) -let convert_concl_no_check t = Tactics.convert_concl_no_check t Term.DEFAULTcast -let convert_concl t = Tactics.convert_concl t Term.DEFAULTcast +let convert_concl_no_check t = Tactics.convert_concl_no_check t DEFAULTcast +let convert_concl t = Tactics.convert_concl t DEFAULTcast let rename_hd_prod orig_name_ref gl = match EConstr.kind (project gl) (pf_concl gl) with - | Term.Prod(_,src,tgt) -> + | Prod(_,src,tgt) -> Proofview.V82.of_tactic (convert_concl_no_check (EConstr.mkProd (!orig_name_ref,src,tgt))) gl | _ -> CErrors.anomaly (str "gentac creates no product") @@ -1446,7 +1446,7 @@ let tclINTRO_ANON = tclINTRO ~id:None ~conclusion:return let tclRENAME_HD_PROD name = Goal.enter begin fun gl -> let convert_concl_no_check t = - Tactics.convert_concl_no_check t Term.DEFAULTcast in + Tactics.convert_concl_no_check t DEFAULTcast in let concl = Goal.concl gl in let sigma = Goal.sigma gl in match EConstr.kind sigma concl with diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 87d107d65..83b4d6562 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -14,6 +14,7 @@ open Util open Names open Printer open Term +open Constr open Termops open Globnames open Misctypes diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index b397c5531..8207bc11e 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -12,6 +12,7 @@ open Ssrmatching_plugin open Util open Names +open Constr open Proofview open Proofview.Notations @@ -90,11 +91,11 @@ open State (** Warning: unlike [nb_deps_assums], it does not perform reduction *) let rec nb_assums cur env sigma t = match EConstr.kind sigma t with - | Term.Prod(name,ty,body) -> + | Prod(name,ty,body) -> nb_assums (cur+1) env sigma body - | Term.LetIn(name,ty,t1,t2) -> + | LetIn(name,ty,t1,t2) -> nb_assums (cur+1) env sigma t2 - | Term.Cast(t,_,_) -> + | Cast(t,_,_) -> nb_assums cur env sigma t | _ -> cur let nb_assums = nb_assums 0 @@ -556,7 +557,7 @@ let rec eqmoveipats eqpat = function let ssrsmovetac = Goal.enter begin fun g -> let sigma, concl = Goal.(sigma g, concl g) in match EConstr.kind sigma concl with - | Term.Prod _ | Term.LetIn _ -> tclUNIT () + | Prod _ | LetIn _ -> tclUNIT () | _ -> Tactics.hnf_in_concl end @@ -594,8 +595,8 @@ let rec is_Evar_or_CastedMeta sigma x = let occur_existential_or_casted_meta sigma c = let rec occrec c = match EConstr.kind sigma c with - | Term.Evar _ -> raise Not_found - | Term.Cast (m,_,_) when EConstr.isMeta sigma m -> raise Not_found + | Evar _ -> raise Not_found + | Cast (m,_,_) when EConstr.isMeta sigma m -> raise Not_found | _ -> EConstr.iter sigma occrec c in try occrec c; false @@ -625,7 +626,7 @@ let tacFIND_ABSTRACT_PROOF check_lock abstract_n = let sigma, env = Goal.(sigma g, env g) in let l = Evd.fold_undefined (fun e ei l -> match EConstr.kind sigma ei.Evd.evar_concl with - | Term.App(hd, [|ty; n; lock|]) + | App(hd, [|ty; n; lock|]) when (not check_lock || (occur_existential_or_casted_meta sigma ty && is_Evar_or_CastedMeta sigma lock)) && @@ -654,8 +655,8 @@ let ssrabstract dgens = let sigma, env, concl = Goal.(sigma g, env g, concl g) in let t = args_id.(0) in match EConstr.kind sigma t with - | (Term.Evar _ | Term.Meta _) -> Ssrcommon.tacUNIFY concl t <*> tclUNIT id - | Term.Cast(m,_,_) + | (Evar _ | Meta _) -> Ssrcommon.tacUNIFY concl t <*> tclUNIT id + | Cast(m,_,_) when EConstr.isEvar sigma m || EConstr.isMeta sigma m -> Ssrcommon.tacUNIFY concl t <*> tclUNIT id | _ -> diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 5f3967440..138b42e54 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -10,6 +10,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +let _vmcast = Constr.VMcast open Names open Pp open Pcoq @@ -17,7 +18,6 @@ open Ltac_plugin open Genarg open Stdarg open Tacarg -open Term open Libnames open Tactics open Tacmach @@ -1938,7 +1938,7 @@ END let vmexacttac pf = Goal.nf_enter begin fun gl -> - exact_no_check (EConstr.mkCast (pf, VMcast, Tacmach.New.pf_concl gl)) + exact_no_check (EConstr.mkCast (pf, _vmcast, Tacmach.New.pf_concl gl)) end TACTIC EXTEND ssrexact diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index 937e68b06..372ae86bd 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -11,6 +11,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) open Names +open Constr open Termops open Tacmach open Misctypes @@ -103,10 +104,10 @@ let endclausestac id_map clseq gl_id cl0 gl = | ids, dc' -> forced && ids = [] && (not hide_goal || dc' = [] && c_hidden) in let rec unmark c = match EConstr.kind (project gl) c with - | Term.Var id when hidden_clseq clseq && id = gl_id -> cl0 - | Term.Prod (Name id, t, c') when List.mem_assoc id id_map -> + | Var id when hidden_clseq clseq && id = gl_id -> cl0 + | Prod (Name id, t, c') when List.mem_assoc id id_map -> EConstr.mkProd (Name (orig_id id), unmark t, unmark c') - | Term.LetIn (Name id, v, t, c') when List.mem_assoc id id_map -> + | LetIn (Name id, v, t, c') when List.mem_assoc id id_map -> EConstr.mkLetIn (Name (orig_id id), unmark v, unmark t, unmark c') | _ -> EConstr.map (project gl) unmark c in let utac hyp = -- cgit v1.2.3