diff options
Diffstat (limited to 'plugins')
70 files changed, 629 insertions, 579 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 6281b2675e..da8955f0d7 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -12,12 +12,12 @@ let get_inductive dir s = let glob_ref () = Coqlib.find_reference contrib_name ("Coq" :: dir) s in Lazy.from_fun (fun () -> Globnames.destIndRef (glob_ref ())) -let decomp_term sigma (c : Term.constr) = - Term.kind_of_term (EConstr.Unsafe.to_constr (Termops.strip_outer_cast sigma (EConstr.of_constr c))) +let decomp_term sigma (c : Constr.t) = + Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast sigma (EConstr.of_constr c))) -let lapp c v = Term.mkApp (Lazy.force c, v) +let lapp c v = Constr.mkApp (Lazy.force c, v) -let (===) = Term.eq_constr +let (===) = Constr.equal module CoqList = struct let path = ["Init"; "Datatypes"] @@ -53,17 +53,11 @@ end module Env = struct - module ConstrHashed = struct - type t = Term.constr - let equal = Term.eq_constr - let hash = Term.hash_constr - end - - module ConstrHashtbl = Hashtbl.Make (ConstrHashed) + module ConstrHashtbl = Hashtbl.Make (Constr) type t = (int ConstrHashtbl.t * int ref) - let add (tbl, off) (t : Term.constr) = + let add (tbl, off) (t : Constr.t) = try ConstrHashtbl.find tbl t with | Not_found -> @@ -103,7 +97,7 @@ module Bool = struct | Negb of t | Ifb of t * t * t - let quote (env : Env.t) sigma (c : Term.constr) : t = + let quote (env : Env.t) sigma (c : Constr.t) : t = let trueb = Lazy.force trueb in let falseb = Lazy.force falseb in let andb = Lazy.force andb in @@ -170,7 +164,7 @@ module Btauto = struct | Bool.Xorb (b1, b2) -> lapp f_xor [|convert b1; convert b2|] | Bool.Ifb (b1, b2, b3) -> lapp f_ifb [|convert b1; convert b2; convert b3|] - let convert_env env : Term.constr = + let convert_env env : Constr.t = CoqList.of_list (Lazy.force Bool.typ) env let reify env t = lapp eval [|convert_env env; convert t|] @@ -249,7 +243,7 @@ module Btauto = struct let env = Env.to_list env in let fl = reify env fl in let fr = reify env fr in - let changed_gl = Term.mkApp (c, [|typ; fl; fr|]) in + let changed_gl = Constr.mkApp (c, [|typ; fl; fr|]) in let changed_gl = EConstr.of_constr changed_gl in Tacticals.New.tclTHENLIST [ Tactics.change_concl changed_gl; diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 1828213227..faabd7c143 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -11,14 +11,15 @@ (* Plus some e-matching and constructor handling by P. Corbineau *) open CErrors -open Util open Pp open Goptions open Names open Term +open Constr open Vars open Tacmach open Evd +open Util let init_size=5 @@ -154,7 +155,7 @@ let rec term_equal t1 t2 = open Hashset.Combine let rec hash_term = function - | Symb c -> combine 1 (hash_constr c) + | Symb c -> combine 1 (Constr.hash c) | Product (s1, s2) -> combine3 2 (Sorts.hash s1) (Sorts.hash s2) | Eps i -> combine 3 (Id.hash i) | Appli (t1, t2) -> combine3 4 (hash_term t1) (hash_term t2) @@ -215,7 +216,7 @@ type representative= mutable lfathers:Int.Set.t; mutable fathers:Int.Set.t; mutable inductive_status: inductive_status; - class_type : Term.types; + class_type : types; mutable functions: Int.Set.t PafMap.t} (*pac -> term = app(constr,t) *) type cl = Rep of representative| Eqto of int*equality @@ -232,7 +233,7 @@ type node = module Constrhash = Hashtbl.Make (struct type t = constr let equal = eq_constr_nounivs - let hash = hash_constr + let hash = Constr.hash end) module Typehash = Constrhash @@ -438,7 +439,7 @@ and applist_proj c l = | Symb s -> applist_projection s l | _ -> applistc (constr_of_term c) l and applist_projection c l = - match kind_of_term c with + match Constr.kind c with | Const c when Environ.is_projection (fst c) (Global.env()) -> let p = Projection.make (fst c) false in (match l with @@ -454,7 +455,7 @@ and applist_projection c l = let rec canonize_name sigma c = let c = EConstr.Unsafe.to_constr c in let func c = canonize_name sigma (EConstr.of_constr c) in - match kind_of_term c with + match Constr.kind c with | Const (kn,u) -> let canon_const = Constant.make1 (Constant.canonical kn) in (mkConstU (canon_const,u)) diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index f904aa3e68..23cd2161d7 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -7,7 +7,7 @@ (************************************************************************) open Util -open Term +open Constr open Names type pa_constructor = @@ -85,7 +85,7 @@ type representative= mutable lfathers:Int.Set.t; mutable fathers:Int.Set.t; mutable inductive_status: inductive_status; - class_type : Term.types; + class_type : types; mutable functions: Int.Set.t PafMap.t} (*pac -> term = app(constr,t) *) type cl = Rep of representative| Eqto of int*equality diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index a43a167e86..97efaced8f 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -10,7 +10,7 @@ (* proof-trees that will be transformed into proof-terms in cctac.ml4 *) open CErrors -open Term +open Constr open Ccalgo open Pp diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli index 9f53123db1..a3e4501342 100644 --- a/plugins/cc/ccproof.mli +++ b/plugins/cc/ccproof.mli @@ -7,7 +7,7 @@ (************************************************************************) open Ccalgo -open Term +open Constr type rule= Ax of constr diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 150319f6b9..7dec34d4d7 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -13,6 +13,7 @@ open Names open Inductiveops open Declarations open Term +open Constr open EConstr open Vars open Tactics @@ -76,11 +77,11 @@ let rec decompose_term env sigma t= let (mind,i_ind),u = c in let u = EInstance.kind sigma u in let canon_mind = MutInd.make1 (MutInd.canonical mind) in - let canon_ind = canon_mind,i_ind in (Symb (Term.mkIndU (canon_ind,u))) + let canon_ind = canon_mind,i_ind in (Symb (Constr.mkIndU (canon_ind,u))) | Const (c,u) -> let u = EInstance.kind sigma u in let canon_const = Constant.make1 (Constant.canonical c) in - (Symb (Term.mkConstU (canon_const,u))) + (Symb (Constr.mkConstU (canon_const,u))) | Proj (p, c) -> let canon_const kn = Constant.make1 (Constant.canonical kn) in let p' = Projection.map canon_const p in @@ -198,7 +199,7 @@ let make_prb gls depth additionnal_terms = (fun decl -> let id = NamedDecl.get_id decl in begin - let cid=Term.mkVar id in + let cid=Constr.mkVar id in match litteral_of_constr env sigma (NamedDecl.get_type decl) with `Eq (t,a,b) -> add_equality state cid a b | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 6d3d4b7432..fb65a8639a 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -6,9 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Constr open Context.Named.Declaration -let map_const_entry_body (f:Term.constr->Term.constr) (x:Safe_typing.private_constants Entries.const_entry_body) +let map_const_entry_body (f:constr->constr) (x:Safe_typing.private_constants Entries.const_entry_body) : Safe_typing.private_constants Entries.const_entry_body = Future.chain x begin fun ((b,ctx),fx) -> (f b , ctx) , fx @@ -67,7 +68,7 @@ let start_deriving f suchthat lemma = let f_def = { f_def with Entries.const_entry_opaque = false } in let f_def = Entries.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in let f_kn = Declare.declare_constant f f_def in - let f_kn_term = Term.mkConst f_kn in + let f_kn_term = mkConst f_kn in (** In the type and body of the proof of [suchthat] there can be references to the variable [f]. It needs to be replaced by references to the constant [f] declared above. This substitution diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 3c46d5c43b..bc84df76b7 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -7,7 +7,7 @@ (************************************************************************) open Miniml -open Term +open Constr open Declarations open Names open ModPath @@ -138,7 +138,7 @@ let check_arity env cb = let check_fix env cb i = match cb.const_body with | Def lbody -> - (match kind_of_term (Mod_subst.force_constr lbody) with + (match Constr.kind (Mod_subst.force_constr lbody) with | Fix ((_,j),recd) when Int.equal i j -> check_arity env cb; (true,recd) | CoFix (j,recd) when Int.equal i j -> check_arity env cb; (false,recd) | _ -> raise Impossible) @@ -146,8 +146,8 @@ let check_fix env cb i = let prec_declaration_equal (na1, ca1, ta1) (na2, ca2, ta2) = Array.equal Name.equal na1 na2 && - Array.equal eq_constr ca1 ca2 && - Array.equal eq_constr ta1 ta2 + Array.equal Constr.equal ca1 ca2 && + Array.equal Constr.equal ta1 ta2 let factor_fix env l cb msb = let _,recd as check = check_fix env cb 0 in diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 7bbb825b10..dd86177381 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -34,4 +34,4 @@ val print_one_decl : (* Used by Extraction Compute *) val structure_for_compute : - Term.constr -> (Miniml.ml_decl list) * Miniml.ml_ast * Miniml.ml_type + Constr.t -> (Miniml.ml_decl list) * Miniml.ml_ast * Miniml.ml_type diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index a227478d0f..47e8123191 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -10,6 +10,7 @@ open Util open Names open Term +open Constr open Vars open Declarations open Declareops @@ -81,7 +82,7 @@ let whd_betaiotazeta t = let rec flag_of_type env t : flag = let t = whd_all env t in - match kind_of_term t with + match Constr.kind t with | Prod (x,t,c) -> flag_of_type (push_rel (LocalAssum (x,t)) env) c | Sort s when Sorts.is_prop s -> (Logic,TypeScheme) | Sort _ -> (Info,TypeScheme) @@ -111,14 +112,14 @@ let push_rel_assum (n, t) env = (*s [type_sign] gernerates a signature aimed at treating a type application. *) let rec type_sign env c = - match kind_of_term (whd_all env c) with + match Constr.kind (whd_all env c) with | Prod (n,t,d) -> (if is_info_scheme env t then Keep else Kill Kprop) :: (type_sign (push_rel_assum (n,t) env) d) | _ -> [] let rec type_scheme_nb_args env c = - match kind_of_term (whd_all env c) with + match Constr.kind (whd_all env c) with | Prod (n,t,d) -> let n = type_scheme_nb_args (push_rel_assum (n,t) env) d in if is_info_scheme env t then n+1 else n @@ -145,7 +146,7 @@ let make_typvar n vl = next_ident_away id' vl let rec type_sign_vl env c = - match kind_of_term (whd_all env c) with + match Constr.kind (whd_all env c) with | Prod (n,t,d) -> let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in if not (is_info_scheme env t) then Kill Kprop::s, vl @@ -153,7 +154,7 @@ let rec type_sign_vl env c = | _ -> [],[] let rec nb_default_params env c = - match kind_of_term (whd_all env c) with + match Constr.kind (whd_all env c) with | Prod (n,t,d) -> let n = nb_default_params (push_rel_assum (n,t) env) d in if is_default env t then n+1 else n @@ -207,7 +208,7 @@ let parse_ind_args si args relmax = | [] -> Int.Map.empty | Kill _ :: s -> parse (i+1) j s | Keep :: s -> - (match kind_of_term args.(i-1) with + (match Constr.kind args.(i-1) with | Rel k -> Int.Map.add (relmax+1-k) j (parse (i+1) (j+1) s) | _ -> parse (i+1) (j+1) s) in parse 1 1 si @@ -224,7 +225,7 @@ let parse_ind_args si args relmax = let rec extract_type env db j c args = - match kind_of_term (whd_betaiotazeta c) with + match Constr.kind (whd_betaiotazeta c) with | App (d, args') -> (* We just accumulate the arguments. *) extract_type env db j d (Array.to_list args' @ args) @@ -299,7 +300,7 @@ let rec extract_type env db j c args = | Proj (p,t) -> (* Let's try to reduce, if it hasn't already been done. *) if Projection.unfolded p then Tunknown - else extract_type env db j (Term.mkProj (Projection.unfold p, t)) args + else extract_type env db j (mkProj (Projection.unfold p, t)) args | Case _ | Fix _ | CoFix _ -> Tunknown | _ -> assert false @@ -331,7 +332,7 @@ and extract_type_scheme env db c p = if Int.equal p 0 then extract_type env db 0 c [] else let c = whd_betaiotazeta c in - match kind_of_term c with + match Constr.kind c with | Lambda (n,t,d) -> extract_type_scheme (push_rel_assum (n,t) env) db d (p-1) | _ -> @@ -415,8 +416,8 @@ and extract_really_ind env kn mib = let t = snd (decompose_prod_n npar types.(j)) in let prods,head = dest_prod epar t in let nprods = List.length prods in - let args = match kind_of_term head with - | App (f,args) -> args (* [kind_of_term f = Ind ip] *) + let args = match Constr.kind head with + | App (f,args) -> args (* [Constr.kind f = Ind ip] *) | _ -> [||] in let dbmap = parse_ind_args p.ip_sign args (nprods + npar) in @@ -444,7 +445,7 @@ and extract_really_ind env kn mib = if Option.is_empty mib.mind_record then raise (I Standard); (* Now we're sure it's a record. *) (* First, we find its field names. *) - let rec names_prod t = match kind_of_term t with + let rec names_prod t = match Constr.kind t with | Prod(n,_,t) -> n::(names_prod t) | LetIn(_,_,_,t) -> names_prod t | Cast(t,_,_) -> names_prod t @@ -503,7 +504,7 @@ and extract_really_ind env kn mib = *) and extract_type_cons env db dbmap c i = - match kind_of_term (whd_all env c) with + match Constr.kind (whd_all env c) with | Prod (n,t,d) -> let env' = push_rel_assum (n,t) env in let db' = (try Int.Map.find i dbmap with Not_found -> 0) :: db in @@ -564,7 +565,7 @@ let record_constant_type env kn opt_typ = (* [mlt] is the ML type we want our extraction of [(c args)] to have. *) let rec extract_term env mle mlt c args = - match kind_of_term c with + match Constr.kind c with | App (f,a) -> extract_term env mle mlt f (Array.to_list a @ args) | Lambda (n, t, d) -> @@ -874,7 +875,7 @@ let decomp_lams_eta_n n m env c t = (* Let's try to identify some situation where extracted code will allow generalisation of type variables *) -let rec gentypvar_ok c = match kind_of_term c with +let rec gentypvar_ok c = match Constr.kind c with | Lambda _ | Const _ -> true | App (c,v) -> (* if all arguments are variables, these variables will diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index e1d43f3405..b15b88ed2c 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -9,7 +9,7 @@ (*s Extraction from Coq terms to Miniml. *) open Names -open Term +open Constr open Declarations open Environ open Miniml diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index cc93f294b3..e52e419fd3 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -180,7 +180,7 @@ val implicits_of_global : global_reference -> Int.Set.t (*s Table for user-given custom ML extractions. *) (* UGLY HACK: registration of a function defined in [extraction.ml] *) -val type_scheme_nb_args_hook : (Environ.env -> Term.constr -> int) Hook.t +val type_scheme_nb_args_hook : (Environ.env -> Constr.t -> int) Hook.t val is_custom : global_reference -> bool val is_inline_custom : global_reference -> bool diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index db1a46a035..c55040df03 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -8,7 +8,7 @@ open Hipattern open Names -open Term +open Constr open EConstr open Vars open Termops @@ -39,7 +39,7 @@ exception Is_atom of constr let meta_succ m = m+1 let rec nb_prod_after n c= - match kind_of_term c with + match Constr.kind c with | Prod (_,_,b) ->if n>0 then nb_prod_after (n-1) b else 1+(nb_prod_after 0 b) | _ -> 0 diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli index 106c469c62..3b6b711c0a 100644 --- a/plugins/firstorder/formula.mli +++ b/plugins/firstorder/formula.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term +open Constr open EConstr open Globnames diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index c2606dbe8e..3409471a7a 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -24,7 +24,7 @@ open Misctypes open Context.Rel.Declaration let compare_instance inst1 inst2= - let cmp c1 c2 = OrderedConstr.compare (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) in + let cmp c1 c2 = Constr.compare (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) in match inst1,inst2 with Phantom(d1),Phantom(d2)-> (cmp d1 d2) diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli index d8d4c1a38a..5c46f4cec2 100644 --- a/plugins/firstorder/rules.mli +++ b/plugins/firstorder/rules.mli @@ -6,9 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term -open EConstr open Names +open Constr +open EConstr open Globnames type tactic = unit Proofview.tactic diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 05194164b0..ea2d076ed9 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -54,13 +54,7 @@ struct (priority e1.pat) - (priority e2.pat) end -module OrderedConstr= -struct - type t=Term.constr - let compare=Term.compare -end - -type h_item = global_reference * (int*Term.constr) option +type h_item = global_reference * (int*Constr.t) option module Hitem= struct @@ -70,13 +64,13 @@ struct if c = 0 then let cmp (i1, c1) (i2, c2) = let c = Int.compare i1 i2 in - if c = 0 then OrderedConstr.compare c1 c2 else c + if c = 0 then Constr.compare c1 c2 else c in Option.compare cmp co1 co2 else c end -module CM=Map.Make(OrderedConstr) +module CM=Map.Make(Constr) module History=Set.Make(Hitem) diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index ca6079c8b0..7f4a6dd86a 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -10,11 +10,9 @@ open EConstr open Formula open Globnames -module OrderedConstr: Set.OrderedType with type t=Term.constr +module CM: CSig.MapS with type key=Constr.t -module CM: CSig.MapS with type key=Term.constr - -type h_item = global_reference * (int*Term.constr) option +type h_item = global_reference * (int*Constr.t) option module History: Set.S with type elt = h_item diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli index d3e8aeee88..390aa8c85c 100644 --- a/plugins/firstorder/unify.mli +++ b/plugins/firstorder/unify.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term +open Constr open EConstr exception UFAIL of constr*constr diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 68af1b3b63..d9e9375c0c 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -12,7 +12,7 @@ des inéquations et équations sont entiers. En attendant la tactique Field. *) -open Term +open Constr open Tactics open Names open Globnames @@ -27,11 +27,7 @@ qui donne le coefficient d'un terme du calcul des constructions, qui est zéro si le terme n'y est pas. *) -module Constrhash = Hashtbl.Make - (struct type t = constr - let equal = eq_constr - let hash = hash_constr - end) +module Constrhash = Hashtbl.Make(Constr) type flin = {fhom: rational Constrhash.t; fcste:rational};; @@ -84,7 +80,7 @@ let string_of_R_constant kn = | _ -> "constant_not_of_R" let rec string_of_R_constr c = - match kind_of_term c with + match Constr.kind c with Cast (c,_,_) -> string_of_R_constr c |Const (c,_) -> string_of_R_constant c | _ -> "not_of_constant" @@ -92,7 +88,7 @@ let rec string_of_R_constr c = exception NoRational let rec rational_of_constr c = - match kind_of_term c with + match Constr.kind c with | Cast (c,_,_) -> (rational_of_constr c) | App (c,args) -> (match (string_of_R_constr c) with @@ -125,7 +121,7 @@ exception NoLinear let rec flin_of_constr c = try( - match kind_of_term c with + match Constr.kind c with | Cast (c,_,_) -> (flin_of_constr c) | App (c,args) -> (match (string_of_R_constr c) with @@ -192,9 +188,9 @@ exception NoIneq let ineq1_of_constr (h,t) = let h = EConstr.Unsafe.to_constr h in let t = EConstr.Unsafe.to_constr t in - match (kind_of_term t) with + match (Constr.kind t) with | App (f,args) -> - (match kind_of_term f with + (match Constr.kind f with | Const (c,_) when Array.length args = 2 -> let t1= args.(0) in let t2= args.(1) in @@ -233,7 +229,7 @@ let ineq1_of_constr (h,t) = let t0= args.(0) in let t1= args.(1) in let t2= args.(2) in - (match (kind_of_term t0) with + (match (Constr.kind t0) with | Const (c,_) -> (match (string_of_R_constant c) with | "R"-> @@ -438,7 +434,7 @@ let tac_use h = (* let is_ineq (h,t) = - match (kind_of_term t) with + match (Constr.kind t) with App (f,args) -> (match (string_of_R_constr f) with "Rlt" -> true @@ -479,7 +475,7 @@ let rec fourier () = (* si le but est une inéquation, on introduit son contraire, et le but à prouver devient False *) try - match (kind_of_term goal) with + match (Constr.kind goal) with App (f,args) -> let get = eget in (match (string_of_R_constr f) with diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 018b515170..722dbc16b5 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -2,6 +2,7 @@ open Printer open CErrors open Util open Term +open Constr open Vars open Namegen open Names @@ -80,7 +81,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let is_pte = let set = List.fold_right Id.Set.add ptes_vars Id.Set.empty in fun t -> - match kind_of_term t with + match Constr.kind t with | Var id -> Id.Set.mem id set | _ -> false in @@ -100,13 +101,13 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let pre_princ = EConstr.Unsafe.to_constr pre_princ in let pre_princ = substl (List.map mkVar ptes_vars) pre_princ in let is_dom c = - match kind_of_term c with + match Constr.kind c with | Ind((u,_),_) -> MutInd.equal u rel_as_kn | Construct(((u,_),_),_) -> MutInd.equal u rel_as_kn | _ -> false in let get_fun_num c = - match kind_of_term c with + match Constr.kind c with | Ind((_,num),_) -> num | Construct(((_,num),_),_) -> num | _ -> assert false @@ -119,7 +120,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = in let rec compute_new_princ_type remove env pre_princ : types*(constr list) = let (new_princ_type,_) as res = - match kind_of_term pre_princ with + match Constr.kind pre_princ with | Rel n -> begin try match Environ.lookup_rel n env with @@ -149,12 +150,12 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = in let new_f,binders_to_remove_from_f = compute_new_princ_type remove env f in applistc new_f new_args, - list_union_eq eq_constr binders_to_remove_from_f binders_to_remove + list_union_eq Constr.equal binders_to_remove_from_f binders_to_remove | LetIn(x,v,t,b) -> compute_new_princ_type_for_letin remove env x v t b | _ -> pre_princ,[] in -(* let _ = match kind_of_term pre_princ with *) +(* let _ = match Constr.kind pre_princ with *) (* | Prod _ -> *) (* observe(str "compute_new_princ_type for "++ *) (* pr_lconstr_env env pre_princ ++ *) @@ -170,13 +171,13 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let new_x : Name.t = get_name (Termops.ids_of_context env) x in let new_env = Environ.push_rel (LocalAssum (x,t)) env in let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in - if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b - then (pop new_b), filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b + if List.exists (Constr.equal (mkRel 1)) binders_to_remove_from_b + then (pop new_b), filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b else ( bind_fun(new_x,new_t,new_b), list_union_eq - eq_constr + Constr.equal binders_to_remove_from_t (List.map pop binders_to_remove_from_b) ) @@ -189,7 +190,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = | Toberemoved_with_rel (n,c) -> (* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *) let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in - new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b) + new_b, list_add_set_eq Constr.equal (mkRel n) (List.map pop binders_to_remove_from_b) end and compute_new_princ_type_for_letin remove env x v t b = begin @@ -199,14 +200,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let new_x : Name.t = get_name (Termops.ids_of_context env) x in let new_env = Environ.push_rel (LocalDef (x,v,t)) env in let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in - if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b - then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b + if List.exists (Constr.equal (mkRel 1)) binders_to_remove_from_b + then (pop new_b),filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b else ( mkLetIn(new_x,new_v,new_t,new_b), list_union_eq - eq_constr - (list_union_eq eq_constr binders_to_remove_from_t binders_to_remove_from_v) + Constr.equal + (list_union_eq Constr.equal binders_to_remove_from_t binders_to_remove_from_v) (List.map pop binders_to_remove_from_b) ) @@ -218,12 +219,12 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = | Toberemoved_with_rel (n,c) -> (* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *) let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in - new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b) + new_b, list_add_set_eq Constr.equal (mkRel n) (List.map pop binders_to_remove_from_b) end and compute_new_princ_type_with_acc remove env e (c_acc,to_remove_acc) = let new_e,to_remove_from_e = compute_new_princ_type remove env e in - new_e::c_acc,list_union_eq eq_constr to_remove_from_e to_remove_acc + new_e::c_acc,list_union_eq Constr.equal to_remove_from_e to_remove_acc in (* observe (str "Computing new principe from " ++ pr_lconstr_env env_with_params_and_predicates pre_princ); *) let pre_res,_ = @@ -329,7 +330,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) | Some (id) -> id,id | None -> let id_of_f = Label.to_id (Constant.label (fst f)) in - id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort) + id_of_f,Indrec.make_elimination_ident id_of_f (Sorts.family type_sort) in let names = ref [new_princ_name] in let hook = @@ -389,7 +390,7 @@ exception Not_Rec let get_funs_constant mp dp = let get_funs_constant const e : (Names.Constant.t*int) array = - match kind_of_term ((strip_lam e)) with + match Constr.kind ((strip_lam e)) with | Fix((_,(na,_,_))) -> Array.mapi (fun i na -> @@ -430,7 +431,7 @@ let get_funs_constant mp dp = let first_params = List.hd l_params in List.iter (fun params -> - if not (List.equal (fun (n1, c1) (n2, c2) -> Name.equal n1 n2 && eq_constr c1 c2) first_params params) + if not (List.equal (fun (n1, c1) (n2, c2) -> Name.equal n1 n2 && Constr.equal c1 c2) first_params params) then user_err Pp.(str "Not a mutal recursive block") ) l_params @@ -439,7 +440,7 @@ let get_funs_constant mp dp = let _check_bodies = try let extract_info is_first body = - match kind_of_term body with + match Constr.kind body with | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca) | _ -> if is_first && Int.equal (List.length l_bodies) 1 @@ -450,7 +451,7 @@ let get_funs_constant mp dp = let check body = (* Hope this is correct *) let eq_infos (ia1, na1, ta1, ca1) (ia2, na2, ta2, ca2) = Array.equal Int.equal ia1 ia2 && Array.equal Name.equal na1 na2 && - Array.equal eq_constr ta1 ta2 && Array.equal eq_constr ca1 ca2 + Array.equal Constr.equal ta1 ta2 && Array.equal Constr.equal ca1 ca2 in if not (eq_infos first_infos (extract_info false body)) then user_err Pp.(str "Not a mutal recursive block") @@ -574,7 +575,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ let t = (strip_prod_assum t) in let applied_g = List.hd (List.rev (snd (decompose_app t))) in let g = fst (decompose_app applied_g) in - if eq_constr f g + if Constr.equal f g then raise (Found_type j); observe (Printer.pr_lconstr f ++ str " <> " ++ Printer.pr_lconstr g) diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index 2eb1b7935d..a3315f22cf 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr val generate_functional_principle : Evd.evar_map ref -> diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 62ecaa552b..829556a71e 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -144,8 +144,7 @@ END let () = let raw_printer _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in - let printer _ _ _ _ = str "<Unavailable printer for rec_definition>" in - Pptactic.declare_extra_genarg_pprule wit_function_rec_definition_loc raw_printer printer printer + Pptactic.declare_extra_vernac_genarg_pprule wit_function_rec_definition_loc raw_printer (* TASSI: n'importe quoi ! *) VERNAC COMMAND EXTEND Function diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index e8e5bfccc1..8ab6dbcdf3 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -2,6 +2,7 @@ open Printer open Pp open Names open Term +open Constr open Vars open Glob_term open Glob_ops @@ -1015,7 +1016,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in observe (str " computing new type for jmeq : done") ; let new_args = - match kind_of_term eq'_as_constr with + match Constr.kind eq'_as_constr with | App(_,[|_;_;ty;_|]) -> let ty = Array.to_list (snd (destApp ty)) in let ty' = snd (Util.List.chop nparam ty) in @@ -1297,7 +1298,7 @@ let rec rebuild_return_type rt = CAst.make @@ Constrexpr.CSort(GType [])) let do_build_inductive - evd (funconstants: Term.pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list) + evd (funconstants: pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list) returned_types (rtl:glob_constr list) = let _time1 = System.get_time () in diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli index 0cab5a6d35..ff0e98d00f 100644 --- a/plugins/funind/glob_term_to_relation.mli +++ b/plugins/funind/glob_term_to_relation.mli @@ -11,7 +11,7 @@ val build_inductive : Id.t list -> (* The list of function name *) *) Evd.evar_map -> - Term.pconstant list -> + Constr.pconstant list -> (Name.t*Glob_term.glob_constr*Glob_term.glob_constr option) list list -> (* The list of function args *) Constrexpr.constr_expr list -> (* The list of function returned type *) Glob_term.glob_constr list -> (* the list of body *) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 76fcd5ec87..e9102e9c82 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -1,8 +1,10 @@ open Names open Pp +open Constr open Libnames open Globnames open Refiner + let mk_prefix pre id = Id.of_string (pre^(Id.to_string id)) let mk_rel_id = mk_prefix "R_" let mk_correct_id id = Nameops.add_suffix (mk_rel_id id) "_correct" @@ -111,7 +113,7 @@ let const_of_id id = (str "cannot find " ++ Id.print id) let def_of_const t = - match (Term.kind_of_term t) with + match Constr.kind t with Term.Const sp -> (try (match Environ.constant_opt_value_in (Global.env()) sp with | Some c -> c @@ -330,8 +332,6 @@ let discharge_Function (_,finfos) = is_general = finfos.is_general } -open Term - let pr_ocst c = Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) c (mt ()) @@ -545,9 +545,9 @@ let prodn n env b = (* compose_prod [xn:Tn;..;x1:T1] b = (x1:T1)..(xn:Tn)b *) let compose_prod l b = prodn (List.length l) l b -type tcc_lemma_value = +type tcc_lemma_value = | Undefined - | Value of Term.constr + | Value of constr | Not_needed (* We only "purify" on exceptions *) diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index d41abee87e..5cc7163aa3 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -38,7 +38,7 @@ val chop_rlambda_n : int -> Glob_term.glob_constr -> val chop_rprod_n : int -> Glob_term.glob_constr -> (Name.t*Glob_term.glob_constr) list * Glob_term.glob_constr -val def_of_const : Term.constr -> Term.constr +val def_of_const : Constr.t -> Constr.t val eq : EConstr.constr Lazy.t val refl_equal : EConstr.constr Lazy.t val const_of_id: Id.t -> Globnames.global_reference(* constantyes *) @@ -118,10 +118,10 @@ val decompose_lam_n : Evd.evar_map -> int -> EConstr.t -> (Names.Name.t * EConstr.t) list * EConstr.t val compose_lam : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t val compose_prod : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t - -type tcc_lemma_value = + +type tcc_lemma_value = | Undefined - | Value of Term.constr + | Value of Constr.t | Not_needed val funind_purify : ('a -> 'b) -> ('a -> 'b) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 9cb2a0a3f5..692a874d36 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -12,6 +12,7 @@ open CErrors open Util open Names open Term +open Constr open EConstr open Vars open Pp @@ -570,6 +571,11 @@ let rec reflexivity_with_destruct_cases g = with e when CErrors.noncritical e -> Proofview.V82.of_tactic reflexivity in let eq_ind = make_eq () in + let my_inj_flags = Some { + Equality.keep_proof_equalities = false; + injection_in_context = false; (* for compatibility, necessary *) + injection_pattern_l2r_order = false; (* probably does not matter; except maybe with dependent hyps *) + } in let discr_inject = Tacticals.onAllHypsAndConcl ( fun sc g -> @@ -580,8 +586,8 @@ let rec reflexivity_with_destruct_cases g = | App(eq,[|_;t1;t2|]) when EConstr.eq_constr (project g) eq eq_ind -> if Equality.discriminable (pf_env g) (project g) t1 t2 then Proofview.V82.of_tactic (Equality.discrHyp id) g - else if Equality.injectable (pf_env g) (project g) t1 t2 - then tclTHENLIST [Proofview.V82.of_tactic (Equality.injHyp None id);thin [id];intros_with_rewrite] g + else if Equality.injectable (pf_env g) (project g) ~keep_proofs:None t1 t2 + then tclTHENLIST [Proofview.V82.of_tactic (Equality.injHyp my_inj_flags None id);thin [id];intros_with_rewrite] g else tclIDTAC g | _ -> tclIDTAC g ) diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 77c26f8ce6..b372241d20 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -18,6 +18,7 @@ open Vernacexpr open Pp open Names open Term +open Constr open Vars open Declarations open Glob_term @@ -36,19 +37,19 @@ let rec popn i c = if i<=0 then c else pop (popn (i-1) c) (** Substitutions in constr *) let compare_constr_nosub t1 t2 = - if compare_constr (fun _ _ -> false) t1 t2 + if Constr.compare_head (fun _ _ -> false) t1 t2 then true else false let rec compare_constr' t1 t2 = if compare_constr_nosub t1 t2 then true - else (compare_constr (compare_constr') t1 t2) + else (Constr.compare_head (compare_constr') t1 t2) let rec substitterm prof t by_t in_u = if (compare_constr' (lift prof t) in_u) then (lift prof by_t) - else map_constr_with_binders succ + else Constr.map_with_binders succ (fun i -> substitterm i t by_t) prof in_u let lift_ldecl n ldecl = List.map (fun (x,y) -> x,lift n y) ldecl @@ -954,16 +955,16 @@ let funify_branches relinfo nfuns branch = | Some (IndRef ((mutual_ind,i) as ind)) -> mutual_ind,ind | _ -> assert false in let is_dom c = - match kind_of_term c with + match Constr.kind c with | Ind(((u,_),_)) | Construct(((u,_),_),_) -> MutInd.equal u mut_induct | _ -> false in let _dom_i c = assert (is_dom c); - match kind_of_term c with + match Constr.kind c with | Ind((u,i)) | Construct((u,_),i) -> i | _ -> assert false in let _is_pred c shift = - match kind_of_term c with + match Constr.kind c with | Rel i -> let reali = i-shift in (reali>=0 && reali<relinfo.nbranches) | _ -> false in (* FIXME: *) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 76f859ed72..2fdc3bc37e 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -10,6 +10,7 @@ module CVars = Vars open Term +open Constr open EConstr open Vars open Namegen @@ -69,7 +70,7 @@ let declare_fun f_id kind ?(ctx=Univ.UContext.empty) value = let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Transparent,None))) let def_of_const t = - match (kind_of_term t) with + match (Constr.kind t) with Const sp -> (try (match constant_opt_value_in (Global.env ()) sp with | Some c -> c @@ -143,7 +144,7 @@ let nat = function () -> (coq_init_constant "nat") let iter_ref () = try find_reference ["Recdef"] "iter" with Not_found -> user_err Pp.(str "module Recdef not loaded") -let iter = function () -> (constr_of_global (delayed_force iter_ref)) +let iter_rd = function () -> (constr_of_global (delayed_force iter_ref)) let eq = function () -> (coq_init_constant "eq") let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS") let le_lt_n_Sm = function () -> (coq_constant arith_Lt "le_lt_n_Sm") @@ -175,8 +176,9 @@ let simpl_iter clause = clause (* Others ugly things ... *) -let (value_f:Term.constr list -> global_reference -> Term.constr) = +let (value_f: Constr.t list -> global_reference -> Constr.t) = let open Term in + let open Constr in fun al fterm -> let rev_x_id_l = ( @@ -207,7 +209,7 @@ let (value_f:Term.constr list -> global_reference -> Term.constr) = let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in it_mkLambda_or_LetIn body context -let (declare_f : Id.t -> logical_kind -> Term.constr list -> global_reference -> global_reference) = +let (declare_f : Id.t -> logical_kind -> Constr.t list -> global_reference -> global_reference) = fun f_id kind input_type fterm_ref -> declare_fun f_id kind (value_f input_type fterm_ref);; @@ -1039,11 +1041,12 @@ let prove_eq = travel equation_info *) let compute_terminate_type nb_args func = let open Term in + let open Constr in let open CVars in let _,a_arrow_b,_ = destLambda(def_of_const (constr_of_global func)) in let rev_args,b = decompose_prod_n nb_args a_arrow_b in let left = - mkApp(delayed_force iter, + mkApp(delayed_force iter_rd, Array.of_list (lift 5 a_arrow_b:: mkRel 3:: constr_of_global func::mkRel 1:: @@ -1460,7 +1463,7 @@ let start_equation (f:global_reference) (term_f:global_reference) let (com_eqn : int -> Id.t -> global_reference -> global_reference -> global_reference - -> Term.constr -> unit) = + -> Constr.t -> unit) = fun nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type -> let open CVars in let opacity = @@ -1514,6 +1517,7 @@ let (com_eqn : int -> Id.t -> let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq generate_induction_principle using_lemmas : unit = let open Term in + let open Constr in let open CVars in let env = Global.env() in let evd = ref (Evd.from_env env) in @@ -1536,7 +1540,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num (* Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *) (* Pp.msgnl (str "rec_arg_num := " ++ str (string_of_int rec_arg_num)); *) (* Pp.msgnl (str "eq' := " ++ str (string_of_int rec_arg_num)); *) - match kind_of_term eq' with + match Constr.kind eq' with | App(e,[|_;_;eq_fix|]) -> mkLambda (Name function_name,function_type,subst_var function_name (compose_lam res_vars eq_fix)) | _ -> failwith "Recursive Definition (res not eq)" diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index 63bbdbe7e3..50b84731b5 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -1,3 +1,4 @@ +open Constr (* val evaluable_of_global_reference : Libnames.global_reference -> Names.evaluable_global_reference *) val tclUSER_if_not_mes : @@ -11,9 +12,9 @@ bool -> Constrintern.internalization_env -> Constrexpr.constr_expr -> Constrexpr.constr_expr -> - int -> Constrexpr.constr_expr -> (Term.pconstant -> + int -> Constrexpr.constr_expr -> (pconstant -> Indfun_common.tcc_lemma_value ref -> - Term.pconstant -> - Term.pconstant -> int -> EConstr.types -> int -> EConstr.constr -> 'a) -> Constrexpr.constr_expr list -> unit + pconstant -> + pconstant -> int -> EConstr.types -> int -> EConstr.constr -> 'a) -> Constrexpr.constr_expr list -> unit diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index d9150a7bbd..1f628803a3 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -17,6 +17,7 @@ open Refiner open Evd open Locus open Context.Named.Declaration +open Ltac_pretype module NamedDecl = Context.Named.Declaration @@ -27,7 +28,7 @@ let instantiate_evar evk (ist,rawc) sigma = let filtered = Evd.evar_filtered_env evi in let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in let lvar = { - Glob_term.ltac_constrs = constrvars; + ltac_constrs = constrvars; ltac_uconstrs = Names.Id.Map.empty; ltac_idents = Names.Id.Map.empty; ltac_genargs = ist.Geninterp.lfun; diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index a7aebf9e15..4b1555e551 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -91,12 +91,12 @@ let elimOnConstrWithHoles tac with_evars c = (fun c -> tac with_evars (Some (None,ElimOnConstr c))) TACTIC EXTEND simplify_eq - [ "simplify_eq" ] -> [ dEq false None ] -| [ "simplify_eq" destruction_arg(c) ] -> [ mytclWithHoles dEq false c ] + [ "simplify_eq" ] -> [ dEq ~keep_proofs:None false None ] +| [ "simplify_eq" destruction_arg(c) ] -> [ mytclWithHoles (dEq ~keep_proofs:None) false c ] END TACTIC EXTEND esimplify_eq -| [ "esimplify_eq" ] -> [ dEq true None ] -| [ "esimplify_eq" destruction_arg(c) ] -> [ mytclWithHoles dEq true c ] +| [ "esimplify_eq" ] -> [ dEq ~keep_proofs:None true None ] +| [ "esimplify_eq" destruction_arg(c) ] -> [ mytclWithHoles (dEq ~keep_proofs:None) true c ] END let discr_main c = elimOnConstrWithHoles discr_tac false c @@ -117,31 +117,31 @@ let discrHyp id = discr_main (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings))) let injection_main with_evars c = - elimOnConstrWithHoles (injClause None) with_evars c + elimOnConstrWithHoles (injClause None None) with_evars c TACTIC EXTEND injection -| [ "injection" ] -> [ injClause None false None ] -| [ "injection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None) false c ] +| [ "injection" ] -> [ injClause None None false None ] +| [ "injection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None None) false c ] END TACTIC EXTEND einjection -| [ "einjection" ] -> [ injClause None true None ] -| [ "einjection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None) true c ] +| [ "einjection" ] -> [ injClause None None true None ] +| [ "einjection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None None) true c ] END TACTIC EXTEND injection_as | [ "injection" "as" intropattern_list(ipat)] -> - [ injClause (Some ipat) false None ] + [ injClause None (Some ipat) false None ] | [ "injection" destruction_arg(c) "as" intropattern_list(ipat)] -> - [ mytclWithHoles (injClause (Some ipat)) false c ] + [ mytclWithHoles (injClause None (Some ipat)) false c ] END TACTIC EXTEND einjection_as | [ "einjection" "as" intropattern_list(ipat)] -> - [ injClause (Some ipat) true None ] + [ injClause None (Some ipat) true None ] | [ "einjection" destruction_arg(c) "as" intropattern_list(ipat)] -> - [ mytclWithHoles (injClause (Some ipat)) true c ] + [ mytclWithHoles (injClause None (Some ipat)) true c ] END TACTIC EXTEND simple_injection -| [ "simple" "injection" ] -> [ simpleInjClause false None ] -| [ "simple" "injection" destruction_arg(c) ] -> [ mytclWithHoles simpleInjClause false c ] +| [ "simple" "injection" ] -> [ simpleInjClause None false None ] +| [ "simple" "injection" destruction_arg(c) ] -> [ mytclWithHoles (simpleInjClause None) false c ] END let injHyp id = @@ -415,7 +415,7 @@ VERNAC COMMAND EXTEND DeriveInversionClear -> [ add_inversion_lemma_exn na c s false inv_clear_tac ] | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => [ seff na ] - -> [ add_inversion_lemma_exn na c InProp false inv_clear_tac ] + -> [ add_inversion_lemma_exn na c Sorts.InProp false inv_clear_tac ] END VERNAC COMMAND EXTEND DeriveInversion @@ -424,7 +424,7 @@ VERNAC COMMAND EXTEND DeriveInversion -> [ add_inversion_lemma_exn na c s false inv_tac ] | [ "Derive" "Inversion" ident(na) "with" constr(c) ] => [ seff na ] - -> [ add_inversion_lemma_exn na c InProp false inv_tac ] + -> [ add_inversion_lemma_exn na c Sorts.InProp false inv_tac ] END VERNAC COMMAND EXTEND DeriveDependentInversion @@ -514,7 +514,7 @@ let cache_transitivity_lemma (_,(left,lem)) = let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref) -let inTransitivity : bool * Term.constr -> obj = +let inTransitivity : bool * Constr.t -> obj = declare_object {(default_object "TRANSITIVITY-STEPS") with cache_function = cache_transitivity_lemma; open_function = (fun i o -> if Int.equal i 1 then cache_transitivity_lemma o); diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4 index 104977aef3..ed2d9da63a 100644 --- a/plugins/ltac/g_class.ml4 +++ b/plugins/ltac/g_class.ml4 @@ -91,7 +91,7 @@ END (** TODO: DEPRECATE *) (* A progress test that allows to see if the evars have changed *) -open Term +open Constr open Proofview.Notations let rec eq_constr_mod_evars sigma x y = diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index c577cb2198..1161525689 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -232,10 +232,12 @@ GEXTEND Gram | l = ident -> Name.Name l ] ] ; let_clause: - [ [ id = identref; ":="; te = tactic_expr -> - (id, arg_of_expr te) - | id = identref; args = LIST1 input_fun; ":="; te = tactic_expr -> - (id, arg_of_expr (TacFun(args,te))) ] ] + [ [ (l,id) = identref; ":="; te = tactic_expr -> + ((l,Name id), arg_of_expr te) + | na = ["_" -> (Some !@loc,Anonymous)]; ":="; te = tactic_expr -> + (na, arg_of_expr te) + | (l,id) = identref; args = LIST1 input_fun; ":="; te = tactic_expr -> + ((l,Name id), arg_of_expr (TacFun(args,te))) ] ] ; match_pattern: [ [ IDENT "context"; oid = OPT Constr.ident; diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index 1a2d895868..fea9e837b1 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -155,6 +155,4 @@ let () = | None -> mt () | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic tac in - (* should not happen *) - let dummy _ _ _ expr = assert false in - Pptactic.declare_extra_genarg_pprule wit_withtac printer dummy dummy + Pptactic.declare_extra_vernac_genarg_pprule wit_withtac printer diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index c22e683235..b148d962ed 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -195,8 +195,7 @@ let binders = Pcoq.create_generic_entry Pcoq.utactic "binders" (Genarg.rawwit wi let () = let raw_printer _ _ _ l = Pp.pr_non_empty_arg Ppconstr.pr_binders l in - let printer _ _ _ _ = Pp.str "<Unavailable printer for binders>" in - Pptactic.declare_extra_genarg_pprule wit_binders raw_printer printer printer + Pptactic.declare_extra_vernac_genarg_pprule wit_binders raw_printer open Pcoq diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index d588c888c4..38460c669f 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -116,7 +116,13 @@ type 'a extra_genarg_printer = | Val.Base t -> begin match Val.eq t tag with | None -> default - | Some Refl -> Genprint.generic_top_print (in_gen (Topwit wit) x) + | Some Refl -> + let open Genprint in + match generic_top_print (in_gen (Topwit wit) x) with + | PrinterBasic pr -> pr () + | PrinterNeedsContext pr -> pr (Global.env()) Evd.empty + | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + printer (Global.env()) Evd.empty default_ensure_surrounded end | _ -> default @@ -432,12 +438,13 @@ type 'a extra_genarg_printer = let pr_occs = pr_with_occurrences (fun () -> str" |- *") (occs,()) in (prlist_with_sep (fun () -> str", ") (pr_hyp_location pr_id) l ++ pr_occs) - let pr_clauses default_is_concl pr_id = function + (* Some true = default is concl; Some false = default is all; None = no default *) + let pr_clauses has_default pr_id = function | { onhyps=Some []; concl_occs=occs } - when (match default_is_concl with Some true -> true | _ -> false) -> + when (match has_default with Some true -> true | _ -> false) -> pr_with_occurrences mt (occs,()) | { onhyps=None; concl_occs=AllOccurrences } - when (match default_is_concl with Some false -> true | _ -> false) -> mt () + when (match has_default with Some false -> true | _ -> false) -> mt () | { onhyps=None; concl_occs=NoOccurrences } -> pr_in (str " * |-") | { onhyps=None; concl_occs=occs } -> @@ -529,8 +536,8 @@ let pr_goal_selector ~toplevel s = let pr_funvar n = spc () ++ Name.print n - let pr_let_clause k pr (id,(bl,t)) = - hov 0 (keyword k ++ spc () ++ pr_lident id ++ prlist pr_funvar bl ++ + let pr_let_clause k pr (na,(bl,t)) = + hov 0 (keyword k ++ spc () ++ pr_lname na ++ prlist pr_funvar bl ++ str " :=" ++ brk (1,1) ++ pr (TacArg (Loc.tag t))) let pr_let_clauses recflag pr = function @@ -1113,10 +1120,10 @@ let pr_goal_selector ~toplevel s = let ty = EConstr.Unsafe.to_constr ty in let rec strip_ty acc n ty = if n=0 then (List.rev acc, EConstr.of_constr ty) else - match Term.kind_of_term ty with - Term.Prod(na,a,b) -> - strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b - | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in + match Constr.kind ty with + | Constr.Prod(na,a,b) -> + strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b + | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in strip_ty [] n ty let pr_atomic_tactic_level env sigma n t = @@ -1174,83 +1181,122 @@ let declare_extra_genarg_pprule wit g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) x in let h x = - let env = Global.env () in - h (pr_econstr_env env Evd.empty) (pr_leconstr_env env Evd.empty) (fun _ _ -> str "<tactic>") x + Genprint.PrinterNeedsContext (fun env sigma -> + h (pr_econstr_env env sigma) (pr_leconstr_env env sigma) (fun _ _ -> str "<tactic>") x) in Genprint.register_print0 wit f g h +let declare_extra_vernac_genarg_pprule wit f = + let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in + Genprint.register_vernac_print0 wit f + (** Registering *) -let run_delayed c = c (Global.env ()) Evd.empty +let pr_intro_pattern_env p = Genprint.PrinterNeedsContext (fun env sigma -> + let print_constr c = let (sigma, c) = c env sigma in pr_econstr_env env sigma c in + Miscprint.pr_intro_pattern print_constr p) + +let pr_red_expr_env r = Genprint.PrinterNeedsContext (fun env sigma -> + pr_red_expr (pr_econstr_env env sigma, pr_leconstr_env env sigma, + pr_evaluable_reference_env env, pr_constr_pattern_env env sigma) r) + +let pr_bindings_env bl = Genprint.PrinterNeedsContext (fun env sigma -> + let sigma, bl = bl env sigma in + Miscprint.pr_bindings + (pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl) + +let pr_with_bindings_env bl = Genprint.PrinterNeedsContext (fun env sigma -> + let sigma, bl = bl env sigma in + pr_with_bindings + (pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl) + +let pr_destruction_arg_env c = Genprint.PrinterNeedsContext (fun env sigma -> + let sigma, c = match c with + | clear_flag,ElimOnConstr g -> let sigma,c = g env sigma in sigma,(clear_flag,ElimOnConstr c) + | clear_flag,ElimOnAnonHyp n as x -> sigma, x + | clear_flag,ElimOnIdent id as x -> sigma, x in + pr_destruction_arg + (pr_econstr_env env sigma) (pr_leconstr_env env sigma) c) -let run_delayed_destruction_arg = function (* HH: Using Evd.empty looks suspicious *) - | clear_flag,ElimOnConstr g -> clear_flag,ElimOnConstr (snd (run_delayed g)) - | clear_flag,ElimOnAnonHyp n as x -> x - | clear_flag,ElimOnIdent id as x -> x +let make_constr_printer f c = + Genprint.PrinterNeedsContextAndLevel { + Genprint.default_already_surrounded = Ppconstr.ltop; + Genprint.default_ensure_surrounded = Ppconstr.lsimpleconstr; + Genprint.printer = (fun env sigma n -> f env sigma n c)} + +let lift f a = Genprint.PrinterBasic (fun () -> f a) let () = let pr_bool b = if b then str "true" else str "false" in let pr_unit _ = str "()" in - let pr_string s = str "\"" ++ str s ++ str "\"" in Genprint.register_print0 wit_int_or_var - (pr_or_var int) (pr_or_var int) int; + (pr_or_var int) (pr_or_var int) (lift int); Genprint.register_print0 wit_ref - pr_reference (pr_or_var (pr_located pr_global)) pr_global; + pr_reference (pr_or_var (pr_located pr_global)) (lift pr_global); Genprint.register_print0 wit_ident - pr_id pr_id pr_id; + pr_id pr_id (lift pr_id); Genprint.register_print0 wit_var - (pr_located pr_id) (pr_located pr_id) pr_id; + (pr_located pr_id) (pr_located pr_id) (lift pr_id); Genprint.register_print0 wit_intro_pattern (Miscprint.pr_intro_pattern pr_constr_expr) (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c)) - (Miscprint.pr_intro_pattern (fun c -> pr_econstr (snd (run_delayed c)))); + pr_intro_pattern_env; Genprint.register_print0 wit_clause_dft_concl (pr_clauses (Some true) pr_lident) (pr_clauses (Some true) pr_lident) - (pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id))) + (fun c -> Genprint.PrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)) c)) ; Genprint.register_print0 wit_constr Ppconstr.pr_constr_expr (fun (c, _) -> Printer.pr_glob_constr c) - Printer.pr_econstr + (make_constr_printer Printer.pr_econstr_n_env) ; Genprint.register_print0 wit_uconstr Ppconstr.pr_constr_expr (fun (c,_) -> Printer.pr_glob_constr c) - Printer.pr_closed_glob + (make_constr_printer Printer.pr_closed_glob_n_env) ; Genprint.register_print0 wit_open_constr Ppconstr.pr_constr_expr (fun (c, _) -> Printer.pr_glob_constr c) - Printer.pr_econstr + (make_constr_printer Printer.pr_econstr_n_env) ; Genprint.register_print0 wit_red_expr (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr)) (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_and_constr_expr pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr)) - (pr_red_expr (pr_econstr, pr_leconstr, pr_evaluable_reference, pr_constr_pattern)); - Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis; + pr_red_expr_env + ; + Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis (lift pr_quantified_hypothesis); Genprint.register_print0 wit_bindings (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr) (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) - (fun it -> Miscprint.pr_bindings_no_with pr_econstr pr_leconstr (snd (run_delayed it))); + pr_bindings_env + ; Genprint.register_print0 wit_constr_with_bindings (pr_with_bindings pr_constr_expr pr_lconstr_expr) (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) - (fun it -> pr_with_bindings pr_econstr pr_leconstr (snd (run_delayed it))); + pr_with_bindings_env + ; + Genprint.register_print0 wit_open_constr_with_bindings + (pr_with_bindings pr_constr_expr pr_lconstr_expr) + (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + pr_with_bindings_env + ; Genprint.register_print0 Tacarg.wit_destruction_arg (pr_destruction_arg pr_constr_expr pr_lconstr_expr) (pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) - (fun it -> pr_destruction_arg pr_econstr pr_leconstr (run_delayed_destruction_arg it)); - Genprint.register_print0 Stdarg.wit_int int int int; - Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool; - Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit; - Genprint.register_print0 Stdarg.wit_pre_ident str str str; - Genprint.register_print0 Stdarg.wit_string pr_string pr_string pr_string + pr_destruction_arg_env + ; + Genprint.register_print0 Stdarg.wit_int int int (lift int); + Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool (lift pr_bool); + Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit (lift pr_unit); + Genprint.register_print0 Stdarg.wit_pre_ident str str (lift str); + Genprint.register_print0 Stdarg.wit_string qstring qstring (lift qstring) let () = let printer _ _ prtac = prtac (0, E) in diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index d9da954fe6..5ecfaf590c 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -46,6 +46,10 @@ val declare_extra_genarg_pprule : 'b glob_extra_genarg_printer -> 'c extra_genarg_printer -> unit +val declare_extra_vernac_genarg_pprule : + ('a, 'b, 'c) genarg_type -> + 'a raw_extra_genarg_printer -> unit + type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list type pp_tactic = { @@ -69,11 +73,16 @@ val pr_may_eval : val pr_and_short_name : ('a -> Pp.t) -> 'a and_short_name -> Pp.t val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t +val pr_evaluable_reference_env : env -> evaluable_global_reference -> Pp.t + +val pr_quantified_hypothesis : quantified_hypothesis -> Pp.t + val pr_in_clause : ('a -> Pp.t) -> 'a Locus.clause_expr -> Pp.t -val pr_clauses : bool option -> +val pr_clauses : (* default: *) bool option -> ('a -> Pp.t) -> 'a Locus.clause_expr -> Pp.t + (* Some true = default is concl; Some false = default is all; None = no default *) val pr_raw_generic : env -> rlevel generic_argument -> Pp.t @@ -116,3 +125,6 @@ val pr_value : tolerability -> Val.t -> Pp.t val ltop : tolerability + +val make_constr_printer : (env -> Evd.evar_map -> Notation_term.tolerability -> 'a -> Pp.t) -> + 'a Genprint.top_printer diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 1809f0fcdb..705a51edd3 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -12,7 +12,7 @@ open CErrors open Util open Nameops open Namegen -open Term +open Constr open EConstr open Vars open Reduction @@ -426,7 +426,7 @@ let split_head = function | [] -> assert(false) let eq_pb (ty, env, x, y as pb) (ty', env', x', y' as pb') = - pb == pb' || (ty == ty' && Term.eq_constr x x' && Term.eq_constr y y') + pb == pb' || (ty == ty' && Constr.equal x x' && Constr.equal y y') let problem_inclusion x y = List.for_all (fun pb -> List.exists (fun pb' -> eq_pb pb pb') y) x @@ -928,8 +928,8 @@ let fold_match ?(force=false) env sigma c = it_mkProd_or_LetIn (subst1 mkProp body) (List.tl ctx) in let sk = - if sortp == InProp then - if sortc == InProp then + if sortp == Sorts.InProp then + if sortc == Sorts.InProp then if dep then case_dep_scheme_kind_from_prop else case_scheme_kind_from_prop else ( diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 63e891b455..1306c590ba 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -37,7 +37,7 @@ type ('constr,'redexpr) strategy_ast = type rewrite_proof = | RewPrf of constr * constr - | RewCast of Term.cast_kind + | RewCast of Constr.cast_kind type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *) diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 9e3a54cc86..c03a867326 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -8,9 +8,8 @@ open Util open Names -open Term +open Constr open EConstr -open Pattern open Misctypes open Genarg open Stdarg @@ -18,15 +17,23 @@ open Geninterp exception CannotCoerceTo of string +let base_val_typ wit = + match val_tag (topwit wit) with Val.Base t -> t | _ -> CErrors.anomaly (Pp.str "Not a base val.") + let (wit_constr_context : (Empty.t, Empty.t, EConstr.constr) Genarg.genarg_type) = let wit = Genarg.create_arg "constr_context" in let () = register_val0 wit None in + let () = Genprint.register_val_print0 (base_val_typ wit) + (Pptactic.make_constr_printer Printer.pr_econstr_n_env) in wit (* includes idents known to be bound and references *) -let (wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) Genarg.genarg_type) = +let (wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_binders) Genarg.genarg_type) = let wit = Genarg.create_arg "constr_under_binders" in let () = register_val0 wit None in + let () = Genprint.register_val_print0 (base_val_typ wit) + (fun c -> + Genprint.PrinterNeedsContext (fun env sigma -> Printer.pr_constr_under_binders_env env sigma c)) in wit (** All the types considered here are base types *) @@ -165,8 +172,8 @@ let id_of_name = function | Sort s -> begin match ESorts.kind sigma s with - | Prop _ -> Label.to_id (Label.make "Prop") - | Type _ -> Label.to_id (Label.make "Type") + | Sorts.Prop _ -> Label.to_id (Label.make "Prop") + | Sorts.Type _ -> Label.to_id (Label.make "Type") end | _ -> fail() diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index 1a67f6f888..d7b253a687 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -10,7 +10,6 @@ open Util open Names open EConstr open Misctypes -open Pattern open Genarg open Geninterp @@ -37,8 +36,8 @@ sig val of_constr : constr -> t val to_constr : t -> constr option - val of_uconstr : Glob_term.closed_glob_constr -> t - val to_uconstr : t -> Glob_term.closed_glob_constr option + val of_uconstr : Ltac_pretype.closed_glob_constr -> t + val to_uconstr : t -> Ltac_pretype.closed_glob_constr option val of_int : int -> t val to_int : t -> int option val to_list : t -> t list option @@ -63,9 +62,9 @@ val coerce_to_hint_base : Value.t -> string val coerce_to_int : Value.t -> int -val coerce_to_constr : Environ.env -> Value.t -> constr_under_binders +val coerce_to_constr : Environ.env -> Value.t -> Ltac_pretype.constr_under_binders -val coerce_to_uconstr : Environ.env -> Value.t -> Glob_term.closed_glob_constr +val coerce_to_uconstr : Environ.env -> Value.t -> Ltac_pretype.closed_glob_constr val coerce_to_closed_constr : Environ.env -> Value.t -> constr @@ -93,4 +92,4 @@ val coerce_to_int_or_var_list : Value.t -> int or_var list val wit_constr_context : (Empty.t, Empty.t, EConstr.constr) genarg_type -val wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) genarg_type +val wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_binders) genarg_type diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 0bf6e3d155..ee84be5414 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -63,28 +63,37 @@ let get_separator = function | None -> user_err Pp.(str "Missing separator.") | Some sep -> sep -let rec parse_user_entry s sep = +let check_separator ?loc = function +| None -> () +| Some _ -> user_err ?loc (str "Separator is only for arguments with suffix _list_sep.") + +let rec parse_user_entry ?loc s sep = let l = String.length s in if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then - let entry = parse_user_entry (String.sub s 3 (l-8)) None in + let entry = parse_user_entry ?loc (String.sub s 3 (l-8)) None in + check_separator ?loc sep; Ulist1 entry else if l > 12 && coincide s "ne_" 0 && coincide s "_list_sep" (l-9) then - let entry = parse_user_entry (String.sub s 3 (l-12)) None in + let entry = parse_user_entry ?loc (String.sub s 3 (l-12)) None in Ulist1sep (entry, get_separator sep) else if l > 5 && coincide s "_list" (l-5) then - let entry = parse_user_entry (String.sub s 0 (l-5)) None in + let entry = parse_user_entry ?loc (String.sub s 0 (l-5)) None in + check_separator ?loc sep; Ulist0 entry else if l > 9 && coincide s "_list_sep" (l-9) then - let entry = parse_user_entry (String.sub s 0 (l-9)) None in + let entry = parse_user_entry ?loc (String.sub s 0 (l-9)) None in Ulist0sep (entry, get_separator sep) else if l > 4 && coincide s "_opt" (l-4) then - let entry = parse_user_entry (String.sub s 0 (l-4)) None in + let entry = parse_user_entry ?loc (String.sub s 0 (l-4)) None in + check_separator ?loc sep; Uopt entry else if Int.equal l 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then let n = Char.code s.[6] - 48 in + check_separator ?loc sep; Uentryl ("tactic", n) else + let _ = check_separator ?loc sep in Uentry s let interp_entry_name interp symb = @@ -203,7 +212,7 @@ let register_tactic_notation_entry name entry = let interp_prod_item = function | TacTerm s -> TacTerm s | TacNonTerm (loc, ((nt, sep), ido)) -> - let symbol = parse_user_entry nt sep in + let symbol = parse_user_entry ?loc nt sep in let interp s = function | None -> if String.Map.mem s !entry_names then String.Map.find s !entry_names diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 2c36faeff4..9bd3efc6b7 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -254,7 +254,7 @@ and 'a gen_tactic_expr = | TacFail of global_flag * int or_var * 'n message_token list | TacInfo of 'a gen_tactic_expr | TacLetIn of rec_flag * - (Id.t located * 'a gen_tactic_arg) list * + (Name.t located * 'a gen_tactic_arg) list * 'a gen_tactic_expr | TacMatch of lazy_flag * 'a gen_tactic_expr * @@ -386,7 +386,7 @@ type ltac_call_kind = | LtacNameCall of ltac_constant | LtacAtomCall of glob_atomic_tactic_expr | LtacVarCall of Id.t * glob_tactic_expr - | LtacConstrInterp of Glob_term.glob_constr * Glob_term.ltac_var_map + | LtacConstrInterp of Glob_term.glob_constr * Ltac_pretype.ltac_var_map type ltac_trace = ltac_call_kind Loc.located list diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 99d7684d36..b16b0a7bae 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -322,13 +322,23 @@ let intern_constr_pattern ist ~as_type ~ltacvars pc = let dummy_pat = PRel 0 -let intern_typed_pattern ist p = +let intern_typed_pattern ist ~as_type ~ltacvars p = (* we cannot ensure in non strict mode that the pattern is closed *) (* keeping a constr_expr copy is too complicated and we want anyway to *) (* type it, so we remember the pattern as a glob_constr only *) + let metas,pat = + if !strict_check then + let ltacvars = { + Constrintern.ltac_vars = ltacvars; + ltac_bound = Id.Set.empty; + ltac_extra = ist.extra; + } in + Constrintern.intern_constr_pattern ist.genv ~as_type ~ltacvars p + else + [], dummy_pat in let (glob,_ as c) = intern_constr_gen true false ist p in let bound_names = Glob_ops.bound_glob_vars glob in - (bound_names,c,dummy_pat) + metas,(bound_names,c,pat) let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = let interp_ref r = @@ -364,7 +374,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = (* We interpret similarly @ref and ref *) interp_ref (AN r) | Inr c -> - Inr (intern_typed_pattern ist c)) + Inr (snd (intern_typed_pattern ist ~as_type:false ~ltacvars:ist.ltacvars c))) (* This seems fairly hacky, but it's the first way I've found to get proper globalization of [unfold]. --adamc *) @@ -458,9 +468,10 @@ let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function (* Utilities *) let extract_let_names lrc = let fold accu ((loc, name), _) = - if Id.Set.mem name accu then user_err ?loc + Nameops.Name.fold_right (fun id accu -> + if Id.Set.mem id accu then user_err ?loc ~hdr:"glob_tactic" (str "This variable is bound several times.") - else Id.Set.add name accu + else Id.Set.add id accu) name accu in List.fold_left fold Id.Set.empty lrc @@ -529,7 +540,12 @@ let rec intern_atomic lf ist x = then intern_type ist c else intern_constr ist c), clause_app (intern_hyp_location ist) cl) | TacChange (Some p,c,cl) -> - TacChange (Some (intern_typed_pattern ist p),intern_constr ist c, + let { ltacvars } = ist in + let metas,pat = intern_typed_pattern ist ~as_type:false ~ltacvars p in + let fold accu x = Id.Set.add x accu in + let ltacvars = List.fold_left fold ltacvars metas in + let ist' = { ist with ltacvars } in + TacChange (Some pat,intern_constr ist' c, clause_app (intern_hyp_location ist) cl) (* Equality and inversion *) @@ -797,7 +813,7 @@ let notation_subst bindings tac = let fold id c accu = let loc = Glob_ops.loc_of_glob_constr (fst c) in let c = ConstrMayEval (ConstrTerm c) in - ((loc, id), c) :: accu + ((loc, Name id), c) :: accu in let bindings = Id.Map.fold fold bindings [] in (** This is theoretically not correct due to potential variable capture, but diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 20f117ff4f..1a8ec6d6f6 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -38,6 +38,7 @@ open Tacintern open Taccoerce open Proofview.Notations open Context.Named.Declaration +open Ltac_pretype let ltac_trace_info = Tactic_debug.ltac_trace_info @@ -75,6 +76,9 @@ let out_gen wit v = let val_tag wit = val_tag (topwit wit) +let base_val_typ wit = + match val_tag wit with Val.Base t -> t | _ -> anomaly (str "Not a base val.") + let pr_argument_type arg = let Val.Dyn (tag, _) = arg in Val.pr tag @@ -123,6 +127,8 @@ type tacvalue = let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) = let wit = Genarg.create_arg "tacvalue" in let () = register_val0 wit None in + let () = Genprint.register_val_print0 (base_val_typ wit) + (fun _ -> Genprint.PrinterBasic (fun () -> str "<tactic closure>")) in wit let of_tacvalue v = in_gen (topwit wit_tacvalue) v @@ -230,24 +236,16 @@ let curr_debug ist = match TacStore.get ist.extra f_debug with (* Displays a value *) let pr_value env v = let v = Value.normalize v in - if has_type v (topwit wit_tacvalue) then str "a tactic" - else if has_type v (topwit wit_constr_context) then - let c = out_gen (topwit wit_constr_context) v in - match env with - | Some (env,sigma) -> pr_leconstr_env env sigma c - | _ -> str "a term" - else if has_type v (topwit wit_constr) then - let c = out_gen (topwit wit_constr) v in + let pr_with_env pr = match env with - | Some (env,sigma) -> pr_leconstr_env env sigma c - | _ -> str "a term" - else if has_type v (topwit wit_constr_under_binders) then - let c = out_gen (topwit wit_constr_under_binders) v in - match env with - | Some (env,sigma) -> pr_lconstr_under_binders_env env sigma c - | _ -> str "a term" - else - str "a value of type" ++ spc () ++ pr_argument_type v + | Some (env,sigma) -> pr env sigma + | None -> str "a value of type" ++ spc () ++ pr_argument_type v in + let open Genprint in + match generic_val_print v with + | PrinterBasic pr -> pr () + | PrinterNeedsContext pr -> pr_with_env pr + | PrinterNeedsContextAndLevel { default_already_surrounded; printer } -> + pr_with_env (fun env sigma -> printer env sigma default_already_surrounded) let pr_closure env ist body = let pp_body = Pptactic.pr_glob_tactic env body in @@ -551,7 +549,6 @@ let interp_fresh_id ist env sigma l = (* Extract the uconstr list from lfun *) let extract_ltac_constr_context ist env sigma = - let open Glob_term in let add_uconstr id v map = try Id.Map.add id (coerce_to_uconstr env v) map with CannotCoerceTo _ -> map @@ -602,10 +599,10 @@ let interp_gen kind ist pattern_mode flags env sigma c = let { closure = constrvars ; term } = interp_glob_closure ist env sigma ~kind:kind_for_intern ~pattern_mode c in let vars = { - Glob_term.ltac_constrs = constrvars.typed; - Glob_term.ltac_uconstrs = constrvars.untyped; - Glob_term.ltac_idents = constrvars.idents; - Glob_term.ltac_genargs = ist.lfun; + ltac_constrs = constrvars.typed; + ltac_uconstrs = constrvars.untyped; + ltac_idents = constrvars.idents; + ltac_genargs = ist.lfun; } in (* Jason Gross: To avoid unnecessary modifications to tacinterp, as suggested by Arnaud Spiwack, we run push_trace immediately. We do @@ -818,51 +815,16 @@ let interp_constr_may_eval ist env sigma c = end (** TODO: should use dedicated printers *) -let rec message_of_value v = +let message_of_value v = let v = Value.normalize v in - let open Ftactic in - if has_type v (topwit wit_tacvalue) then - Ftactic.return (str "<tactic>") - else if has_type v (topwit wit_constr) then - let v = out_gen (topwit wit_constr) v in - Ftactic.enter begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) v) end - else if has_type v (topwit wit_constr_under_binders) then - let c = out_gen (topwit wit_constr_under_binders) v in - Ftactic.enter begin fun gl -> - Ftactic.return (pr_constr_under_binders_env (pf_env gl) (project gl) c) - end - else if has_type v (topwit wit_unit) then - Ftactic.return (str "()") - else if has_type v (topwit wit_int) then - Ftactic.return (int (out_gen (topwit wit_int) v)) - else if has_type v (topwit wit_intro_pattern) then - let p = out_gen (topwit wit_intro_pattern) v in - let print env sigma c = - let (sigma, c) = c env sigma in - pr_econstr_env env sigma c - in - Ftactic.enter begin fun gl -> - Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (project gl) c) p) - end - else if has_type v (topwit wit_constr_context) then - let c = out_gen (topwit wit_constr_context) v in - Ftactic.enter begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) c) end - else if has_type v (topwit wit_uconstr) then - let c = out_gen (topwit wit_uconstr) v in - Ftactic.enter begin fun gl -> - Ftactic.return (pr_closed_glob_env (pf_env gl) - (project gl) c) - end - else if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in - Ftactic.enter begin fun gl -> Ftactic.return (Id.print id) end - else match Value.to_list v with - | Some l -> - Ftactic.List.map message_of_value l >>= fun l -> - Ftactic.return (prlist_with_sep spc (fun x -> x) l) - | None -> - let tag = pr_argument_type v in - Ftactic.return (str "<" ++ tag ++ str ">") (** TODO *) + let pr_with_env pr = + Ftactic.enter begin fun gl -> Ftactic.return (pr (pf_env gl) (project gl)) end in + let open Genprint in + match generic_val_print v with + | PrinterBasic pr -> Ftactic.return (pr ()) + | PrinterNeedsContext pr -> pr_with_env pr + | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + pr_with_env (fun env sigma -> printer env sigma default_ensure_surrounded) let interp_message_token ist = function | MsgString s -> Ftactic.return (str s) @@ -946,13 +908,13 @@ let interp_in_hyp_as ist env sigma (id,ipat) = let sigma, ipat = interp_intro_pattern_option ist env sigma ipat in sigma,(interp_hyp ist env sigma id,ipat) -let interp_binding_name ist sigma = function +let interp_binding_name ist env sigma = function | AnonHyp n -> AnonHyp n | NamedHyp id -> (* If a name is bound, it has to be a quantified hypothesis *) (* user has to use other names for variables if these ones clash with *) (* a name intented to be used as a (non-variable) identifier *) - try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist None(Loc.tag id) + try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist (Some (env,sigma)) (Loc.tag id) with Not_found -> NamedHyp id let interp_declared_or_quantified_hypothesis ist env sigma = function @@ -964,7 +926,7 @@ let interp_declared_or_quantified_hypothesis ist env sigma = function let interp_binding ist env sigma (loc,(b,c)) = let sigma, c = interp_open_constr ist env sigma c in - sigma, (loc,(interp_binding_name ist sigma b,c)) + sigma, (loc,(interp_binding_name ist env sigma b,c)) let interp_bindings ist env sigma = function | NoBindings -> @@ -1386,10 +1348,14 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = end >>= fun v -> (* No errors happened, we propagate the trace *) let v = append_trace trace v in - Proofview.tclLIFT begin - debugging_step ist - (fun () -> - str"evaluation returns"++fnl()++pr_value None v) + let call_debug env = + Proofview.tclLIFT (debugging_step ist (fun () -> str"evaluation returns"++fnl()++pr_value env v)) in + begin + let open Genprint in + match generic_val_print v with + | PrinterBasic _ -> call_debug None + | PrinterNeedsContext _ | PrinterNeedsContextAndLevel _ -> + Proofview.Goal.enter (fun gl -> call_debug (Some (pf_env gl,project gl))) end <*> if List.is_empty lval then Ftactic.return v else interp_app loc ist v lval else @@ -1431,9 +1397,9 @@ and tactic_of_value ist vle = and interp_letrec ist llc u = Proofview.tclUNIT () >>= fun () -> (* delay for the effects of [lref], just in case. *) let lref = ref ist.lfun in - let fold accu ((_, id), b) = + let fold accu ((_, na), b) = let v = of_tacvalue (VRec (lref, TacArg (Loc.tag b))) in - Id.Map.add id v accu + Name.fold_right (fun id -> Id.Map.add id v) na accu in let lfun = List.fold_left fold ist.lfun llc in let () = lref := lfun in @@ -1446,9 +1412,9 @@ and interp_letin ist llc u = | [] -> let ist = { ist with lfun } in val_interp ist u - | ((_, id), body) :: defs -> + | ((_, na), body) :: defs -> Ftactic.bind (interp_tacarg ist body) (fun v -> - fold (Id.Map.add id v lfun) defs) + fold (Name.fold_right (fun id -> Id.Map.add id v) na lfun) defs) in fold ist.lfun llc diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index d0a0a81d4c..5f2723a1e3 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -44,7 +44,7 @@ val f_avoid_ids : Id.Set.t TacStore.field val f_debug : debug_info TacStore.field val extract_ltac_constr_values : interp_sign -> Environ.env -> - Pattern.constr_under_binders Id.Map.t + Ltac_pretype.constr_under_binders Id.Map.t (** Given an interpretation signature, extract all values which are coercible to a [constr]. *) @@ -57,7 +57,7 @@ val get_debug : unit -> debug_info val type_uconstr : ?flags:Pretyping.inference_flags -> ?expected_type:Pretyping.typing_constraint -> - Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr Tactypes.delayed_open + Geninterp.interp_sign -> Ltac_pretype.closed_glob_constr -> constr Tactypes.delayed_open (** Adds an interpretation function for extra generic arguments *) @@ -79,10 +79,10 @@ val interp_hyp : interp_sign -> Environ.env -> Evd.evar_map -> val interp_glob_closure : interp_sign -> Environ.env -> Evd.evar_map -> ?kind:Pretyping.typing_constraint -> ?pattern_mode:bool -> glob_constr_and_expr -> - Glob_term.closed_glob_constr + Ltac_pretype.closed_glob_constr val interp_uconstr : interp_sign -> Environ.env -> Evd.evar_map -> - glob_constr_and_expr -> Glob_term.closed_glob_constr + glob_constr_and_expr -> Ltac_pretype.closed_glob_constr val interp_constr_gen : Pretyping.typing_constraint -> interp_sign -> Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Evd.evar_map * constr diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 5394b1e116..a669692fc9 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -363,7 +363,7 @@ let explain_ltac_call_trace last trace loc = | Tacexpr.LtacAtomCall te -> quote (Pptactic.pr_glob_tactic (Global.env()) (Tacexpr.TacAtom (Loc.tag te))) - | Tacexpr.LtacConstrInterp (c, { Glob_term.ltac_constrs = vars }) -> + | Tacexpr.LtacConstrInterp (c, { Ltac_pretype.ltac_constrs = vars }) -> quote (Printer.pr_glob_constr_env (Global.env()) c) ++ (if not (Id.Map.is_empty vars) then strbrk " (with " ++ diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index 18bb7d2dbd..89b78e5907 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -22,7 +22,7 @@ module NamedDecl = Context.Named.Declaration those of {!Matching.matching_result}), and a {!Term.constr} substitution mapping corresponding to matched hypotheses. *) type 'a t = { - subst : Constr_matching.bound_ident_map * Pattern.extended_patvar_map ; + subst : Constr_matching.bound_ident_map * Ltac_pretype.extended_patvar_map ; context : EConstr.constr Id.Map.t; terms : EConstr.constr Id.Map.t; lhs : 'a; @@ -36,8 +36,8 @@ type 'a t = { (** Some of the functions of {!Matching} return the substitution with a [patvar_map] instead of an [extended_patvar_map]. [adjust] coerces substitution of the former type to the latter. *) -let adjust : Constr_matching.bound_ident_map * Pattern.patvar_map -> - Constr_matching.bound_ident_map * Pattern.extended_patvar_map = +let adjust : Constr_matching.bound_ident_map * Ltac_pretype.patvar_map -> + Constr_matching.bound_ident_map * Ltac_pretype.extended_patvar_map = fun (l, lc) -> (l, Id.Map.map (fun c -> [], c) lc) diff --git a/plugins/ltac/tactic_matching.mli b/plugins/ltac/tactic_matching.mli index 01334d36c9..955f8105fb 100644 --- a/plugins/ltac/tactic_matching.mli +++ b/plugins/ltac/tactic_matching.mli @@ -18,7 +18,7 @@ those of {!Matching.matching_result}), and a {!Term.constr} substitution mapping corresponding to matched hypotheses. *) type 'a t = { - subst : Constr_matching.bound_ident_map * Pattern.extended_patvar_map ; + subst : Constr_matching.bound_ident_map * Ltac_pretype.extended_patvar_map ; context : EConstr.constr Names.Id.Map.t; terms : EConstr.constr Names.Id.Map.t; lhs : 'a; diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index fc6781b067..218342efe4 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -20,6 +20,7 @@ open Pp open Mutils open Goptions open Names +open Constr (** * Debug flag @@ -580,9 +581,9 @@ struct | Ukn | BadStr of string | BadNum of int - | BadTerm of Term.constr + | BadTerm of constr | Msg of string - | Goal of (Term.constr list ) * Term.constr * parse_error + | Goal of (constr list ) * constr * parse_error let string_of_error = function | Ukn -> "ukn" @@ -1521,7 +1522,7 @@ let rec witness prover l1 l2 = let rec apply_ids t ids = match ids with | [] -> t - | i::ids -> apply_ids (Term.mkApp(t,[| Term.mkVar i |])) ids + | i::ids -> apply_ids (mkApp(t,[| mkVar i |])) ids let coq_Node = lazy (gen_constant_in_modules "VarMap" diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index 72934a15d9..559dfab524 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -8,7 +8,7 @@ open CErrors open Util -open Term +open Constr open Tactics open Coqlib @@ -204,42 +204,42 @@ else mkt_app ttpow [Lazy.force tz; mkt_term t1; mkt_n (num_of_int n)] let rec parse_pos p = - match kind_of_term p with + match Constr.kind p with | App (a,[|p2|]) -> - if eq_constr a (Lazy.force pxO) then num_2 */ (parse_pos p2) + if Constr.equal a (Lazy.force pxO) then num_2 */ (parse_pos p2) else num_1 +/ (num_2 */ (parse_pos p2)) | _ -> num_1 let parse_z z = - match kind_of_term z with + match Constr.kind z with | App (a,[|p2|]) -> - if eq_constr a (Lazy.force zpos) then parse_pos p2 else (num_0 -/ (parse_pos p2)) + if Constr.equal a (Lazy.force zpos) then parse_pos p2 else (num_0 -/ (parse_pos p2)) | _ -> num_0 let parse_n z = - match kind_of_term z with + match Constr.kind z with | App (a,[|p2|]) -> parse_pos p2 | _ -> num_0 let rec parse_term p = - match kind_of_term p with + match Constr.kind p with | App (a,[|_;p2|]) -> - if eq_constr a (Lazy.force ttvar) then Var (string_of_num (parse_pos p2)) - else if eq_constr a (Lazy.force ttconst) then Const (parse_z p2) - else if eq_constr a (Lazy.force ttopp) then Opp (parse_term p2) + if Constr.equal a (Lazy.force ttvar) then Var (string_of_num (parse_pos p2)) + else if Constr.equal a (Lazy.force ttconst) then Const (parse_z p2) + else if Constr.equal a (Lazy.force ttopp) then Opp (parse_term p2) else Zero | App (a,[|_;p2;p3|]) -> - if eq_constr a (Lazy.force ttadd) then Add (parse_term p2, parse_term p3) - else if eq_constr a (Lazy.force ttsub) then Sub (parse_term p2, parse_term p3) - else if eq_constr a (Lazy.force ttmul) then Mul (parse_term p2, parse_term p3) - else if eq_constr a (Lazy.force ttpow) then + if Constr.equal a (Lazy.force ttadd) then Add (parse_term p2, parse_term p3) + else if Constr.equal a (Lazy.force ttsub) then Sub (parse_term p2, parse_term p3) + else if Constr.equal a (Lazy.force ttmul) then Mul (parse_term p2, parse_term p3) + else if Constr.equal a (Lazy.force ttpow) then Pow (parse_term p2, int_of_num (parse_n p3)) else Zero | _ -> Zero let rec parse_request lp = - match kind_of_term lp with + match Constr.kind lp with | App (_,[|_|]) -> [] | App (_,[|_;p;lp1|]) -> (parse_term p)::(parse_request lp1) diff --git a/plugins/nsatz/nsatz.mli b/plugins/nsatz/nsatz.mli index d6e3071aa3..e50a12a509 100644 --- a/plugins/nsatz/nsatz.mli +++ b/plugins/nsatz/nsatz.mli @@ -6,4 +6,4 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -val nsatz_compute : Term.constr -> unit Proofview.tactic +val nsatz_compute : Constr.t -> unit Proofview.tactic diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index e1e73b1c32..96bf31b11a 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -166,11 +166,7 @@ exchange ?1 and ?2 in the example above) *) -module ConstrSet = Set.Make( - struct - type t = Term.constr - let compare = Term.compare - end) +module ConstrSet = Set.Make(Constr) type inversion_scheme = { normal_lhs_rhs : (constr * constr_pattern) list; @@ -385,11 +381,7 @@ let rec sort_subterm gl l = | [] -> [] | h::t -> insert h (sort_subterm gl t) -module Constrhash = Hashtbl.Make - (struct type t = Term.constr - let equal = Term.eq_constr - let hash = Term.hash_constr - end) +module Constrhash = Hashtbl.Make(Constr) let subst_meta subst c = let subst = List.map (fun (i, c) -> i, EConstr.Unsafe.to_constr c) subst in diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index c27ac2ea44..5397b00656 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -7,14 +7,16 @@ *************************************************************************) open Names +open Term +open Constr let module_refl_name = "ReflOmegaCore" let module_refl_path = ["Coq"; "romega"; module_refl_name] type result = | Kvar of string - | Kapp of string * Term.constr list - | Kimp of Term.constr * Term.constr + | Kapp of string * constr list + | Kimp of constr * constr | Kufo let meaningful_submodule = [ "Z"; "N"; "Pos" ] @@ -30,27 +32,27 @@ let string_of_global r = prefix^(Names.Id.to_string (Nametab.basename_of_global r)) let destructurate t = - let c, args = Term.decompose_app t in - match Term.kind_of_term c, args with - | Term.Const (sp,_), args -> + let c, args = decompose_app t in + match Constr.kind c, args with + | Const (sp,_), args -> Kapp (string_of_global (Globnames.ConstRef sp), args) - | Term.Construct (csp,_) , args -> + | Construct (csp,_) , args -> Kapp (string_of_global (Globnames.ConstructRef csp), args) - | Term.Ind (isp,_), args -> + | Ind (isp,_), args -> Kapp (string_of_global (Globnames.IndRef isp), args) - | Term.Var id, [] -> Kvar(Names.Id.to_string id) - | Term.Prod (Anonymous,typ,body), [] -> Kimp(typ,body) + | Var id, [] -> Kvar(Names.Id.to_string id) + | Prod (Anonymous,typ,body), [] -> Kimp(typ,body) | _ -> Kufo exception DestConstApp let dest_const_apply t = - let f,args = Term.decompose_app t in + let f,args = decompose_app t in let ref = - match Term.kind_of_term f with - | Term.Const (sp,_) -> Globnames.ConstRef sp - | Term.Construct (csp,_) -> Globnames.ConstructRef csp - | Term.Ind (isp,_) -> Globnames.IndRef isp + match Constr.kind f with + | Const (sp,_) -> Globnames.ConstRef sp + | Construct (csp,_) -> Globnames.ConstructRef csp + | Ind (isp,_) -> Globnames.IndRef isp | _ -> raise DestConstApp in Nametab.basename_of_global ref, args @@ -129,7 +131,7 @@ let coq_O = lazy(init_constant "O") let rec mk_nat = function | 0 -> Lazy.force coq_O - | n -> Term.mkApp (Lazy.force coq_S, [| mk_nat (n-1) |]) + | n -> mkApp (Lazy.force coq_S, [| mk_nat (n-1) |]) (* Lists *) @@ -141,47 +143,47 @@ let mkListConst c = if Global.is_polymorphic r then fun u -> Univ.Instance.of_array [|u|] else fun _ -> Univ.Instance.empty in - fun u -> Term.mkConstructU (Globnames.destConstructRef r, inst u) + fun u -> mkConstructU (Globnames.destConstructRef r, inst u) -let coq_cons univ typ = Term.mkApp (mkListConst "cons" univ, [|typ|]) -let coq_nil univ typ = Term.mkApp (mkListConst "nil" univ, [|typ|]) +let coq_cons univ typ = mkApp (mkListConst "cons" univ, [|typ|]) +let coq_nil univ typ = mkApp (mkListConst "nil" univ, [|typ|]) let mk_list univ typ l = let rec loop = function | [] -> coq_nil univ typ | (step :: l) -> - Term.mkApp (coq_cons univ typ, [| step; loop l |]) in + mkApp (coq_cons univ typ, [| step; loop l |]) in loop l let mk_plist = let type1lev = Universes.new_univ_level (Global.current_dirpath ()) in - fun l -> mk_list type1lev Term.mkProp l + fun l -> mk_list type1lev mkProp l let mk_list = mk_list Univ.Level.set type parse_term = - | Tplus of Term.constr * Term.constr - | Tmult of Term.constr * Term.constr - | Tminus of Term.constr * Term.constr - | Topp of Term.constr - | Tsucc of Term.constr + | Tplus of constr * constr + | Tmult of constr * constr + | Tminus of constr * constr + | Topp of constr + | Tsucc of constr | Tnum of Bigint.bigint | Tother type parse_rel = - | Req of Term.constr * Term.constr - | Rne of Term.constr * Term.constr - | Rlt of Term.constr * Term.constr - | Rle of Term.constr * Term.constr - | Rgt of Term.constr * Term.constr - | Rge of Term.constr * Term.constr + | Req of constr * constr + | Rne of constr * constr + | Rlt of constr * constr + | Rle of constr * constr + | Rgt of constr * constr + | Rge of constr * constr | Rtrue | Rfalse - | Rnot of Term.constr - | Ror of Term.constr * Term.constr - | Rand of Term.constr * Term.constr - | Rimp of Term.constr * Term.constr - | Riff of Term.constr * Term.constr + | Rnot of constr + | Ror of constr * constr + | Rand of constr * constr + | Rimp of constr * constr + | Riff of constr * constr | Rother let parse_logic_rel c = match destructurate c with @@ -209,29 +211,29 @@ let rec mk_positive n = if Bigint.equal n Bigint.one then Lazy.force coq_xH else let (q,r) = Bigint.euclid n Bigint.two in - Term.mkApp + mkApp ((if Bigint.equal r Bigint.zero then Lazy.force coq_xO else Lazy.force coq_xI), [| mk_positive q |]) let mk_N = function | 0 -> Lazy.force coq_N0 - | n -> Term.mkApp (Lazy.force coq_Npos, + | n -> mkApp (Lazy.force coq_Npos, [| mk_positive (Bigint.of_int n) |]) module type Int = sig - val typ : Term.constr Lazy.t - val is_int_typ : [ `NF ] Proofview.Goal.t -> Term.constr -> bool - val plus : Term.constr Lazy.t - val mult : Term.constr Lazy.t - val opp : Term.constr Lazy.t - val minus : Term.constr Lazy.t - - val mk : Bigint.bigint -> Term.constr - val parse_term : Term.constr -> parse_term - val parse_rel : [ `NF ] Proofview.Goal.t -> Term.constr -> parse_rel + val typ : constr Lazy.t + val is_int_typ : [ `NF ] Proofview.Goal.t -> constr -> bool + val plus : constr Lazy.t + val mult : constr Lazy.t + val opp : constr Lazy.t + val minus : constr Lazy.t + + val mk : Bigint.bigint -> constr + val parse_term : constr -> parse_term + val parse_rel : [ `NF ] Proofview.Goal.t -> constr -> parse_rel (* check whether t is built only with numbers and + * - *) - val get_scalar : Term.constr -> Bigint.bigint option + val get_scalar : constr -> Bigint.bigint option end module Z : Int = struct @@ -266,9 +268,9 @@ let recognize_Z t = let mk_Z n = if Bigint.equal n Bigint.zero then Lazy.force coq_Z0 else if Bigint.is_strictly_pos n then - Term.mkApp (Lazy.force coq_Zpos, [| mk_positive n |]) + mkApp (Lazy.force coq_Zpos, [| mk_positive n |]) else - Term.mkApp (Lazy.force coq_Zneg, [| mk_positive (Bigint.neg n) |]) + mkApp (Lazy.force coq_Zneg, [| mk_positive (Bigint.neg n) |]) let mk = mk_Z diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli index 80e00e4e14..5ba063d9d0 100644 --- a/plugins/romega/const_omega.mli +++ b/plugins/romega/const_omega.mli @@ -8,116 +8,117 @@ (** Coq objects used in romega *) +open Constr (* from Logic *) -val coq_refl_equal : Term.constr lazy_t -val coq_and : Term.constr lazy_t -val coq_not : Term.constr lazy_t -val coq_or : Term.constr lazy_t -val coq_True : Term.constr lazy_t -val coq_False : Term.constr lazy_t -val coq_I : Term.constr lazy_t +val coq_refl_equal : constr lazy_t +val coq_and : constr lazy_t +val coq_not : constr lazy_t +val coq_or : constr lazy_t +val coq_True : constr lazy_t +val coq_False : constr lazy_t +val coq_I : constr lazy_t (* from ReflOmegaCore/ZOmega *) -val coq_t_int : Term.constr lazy_t -val coq_t_plus : Term.constr lazy_t -val coq_t_mult : Term.constr lazy_t -val coq_t_opp : Term.constr lazy_t -val coq_t_minus : Term.constr lazy_t -val coq_t_var : Term.constr lazy_t - -val coq_proposition : Term.constr lazy_t -val coq_p_eq : Term.constr lazy_t -val coq_p_leq : Term.constr lazy_t -val coq_p_geq : Term.constr lazy_t -val coq_p_lt : Term.constr lazy_t -val coq_p_gt : Term.constr lazy_t -val coq_p_neq : Term.constr lazy_t -val coq_p_true : Term.constr lazy_t -val coq_p_false : Term.constr lazy_t -val coq_p_not : Term.constr lazy_t -val coq_p_or : Term.constr lazy_t -val coq_p_and : Term.constr lazy_t -val coq_p_imp : Term.constr lazy_t -val coq_p_prop : Term.constr lazy_t - -val coq_s_bad_constant : Term.constr lazy_t -val coq_s_divide : Term.constr lazy_t -val coq_s_not_exact_divide : Term.constr lazy_t -val coq_s_sum : Term.constr lazy_t -val coq_s_merge_eq : Term.constr lazy_t -val coq_s_split_ineq : Term.constr lazy_t - -val coq_direction : Term.constr lazy_t -val coq_d_left : Term.constr lazy_t -val coq_d_right : Term.constr lazy_t - -val coq_e_split : Term.constr lazy_t -val coq_e_extract : Term.constr lazy_t -val coq_e_solve : Term.constr lazy_t - -val coq_interp_sequent : Term.constr lazy_t -val coq_do_omega : Term.constr lazy_t - -val mk_nat : int -> Term.constr -val mk_N : int -> Term.constr +val coq_t_int : constr lazy_t +val coq_t_plus : constr lazy_t +val coq_t_mult : constr lazy_t +val coq_t_opp : constr lazy_t +val coq_t_minus : constr lazy_t +val coq_t_var : constr lazy_t + +val coq_proposition : constr lazy_t +val coq_p_eq : constr lazy_t +val coq_p_leq : constr lazy_t +val coq_p_geq : constr lazy_t +val coq_p_lt : constr lazy_t +val coq_p_gt : constr lazy_t +val coq_p_neq : constr lazy_t +val coq_p_true : constr lazy_t +val coq_p_false : constr lazy_t +val coq_p_not : constr lazy_t +val coq_p_or : constr lazy_t +val coq_p_and : constr lazy_t +val coq_p_imp : constr lazy_t +val coq_p_prop : constr lazy_t + +val coq_s_bad_constant : constr lazy_t +val coq_s_divide : constr lazy_t +val coq_s_not_exact_divide : constr lazy_t +val coq_s_sum : constr lazy_t +val coq_s_merge_eq : constr lazy_t +val coq_s_split_ineq : constr lazy_t + +val coq_direction : constr lazy_t +val coq_d_left : constr lazy_t +val coq_d_right : constr lazy_t + +val coq_e_split : constr lazy_t +val coq_e_extract : constr lazy_t +val coq_e_solve : constr lazy_t + +val coq_interp_sequent : constr lazy_t +val coq_do_omega : constr lazy_t + +val mk_nat : int -> constr +val mk_N : int -> constr (** Precondition: the type of the list is in Set *) -val mk_list : Term.constr -> Term.constr list -> Term.constr -val mk_plist : Term.types list -> Term.types +val mk_list : constr -> constr list -> constr +val mk_plist : types list -> types (** Analyzing a coq term *) (* The generic result shape of the analysis of a term. One-level depth, except when a number is found *) type parse_term = - Tplus of Term.constr * Term.constr - | Tmult of Term.constr * Term.constr - | Tminus of Term.constr * Term.constr - | Topp of Term.constr - | Tsucc of Term.constr + Tplus of constr * constr + | Tmult of constr * constr + | Tminus of constr * constr + | Topp of constr + | Tsucc of constr | Tnum of Bigint.bigint | Tother (* The generic result shape of the analysis of a relation. One-level depth. *) type parse_rel = - Req of Term.constr * Term.constr - | Rne of Term.constr * Term.constr - | Rlt of Term.constr * Term.constr - | Rle of Term.constr * Term.constr - | Rgt of Term.constr * Term.constr - | Rge of Term.constr * Term.constr + Req of constr * constr + | Rne of constr * constr + | Rlt of constr * constr + | Rle of constr * constr + | Rgt of constr * constr + | Rge of constr * constr | Rtrue | Rfalse - | Rnot of Term.constr - | Ror of Term.constr * Term.constr - | Rand of Term.constr * Term.constr - | Rimp of Term.constr * Term.constr - | Riff of Term.constr * Term.constr + | Rnot of constr + | Ror of constr * constr + | Rand of constr * constr + | Rimp of constr * constr + | Riff of constr * constr | Rother (* A module factorizing what we should now about the number representation *) module type Int = sig (* the coq type of the numbers *) - val typ : Term.constr Lazy.t + val typ : constr Lazy.t (* Is a constr expands to the type of these numbers *) - val is_int_typ : [ `NF ] Proofview.Goal.t -> Term.constr -> bool + val is_int_typ : [ `NF ] Proofview.Goal.t -> constr -> bool (* the operations on the numbers *) - val plus : Term.constr Lazy.t - val mult : Term.constr Lazy.t - val opp : Term.constr Lazy.t - val minus : Term.constr Lazy.t + val plus : constr Lazy.t + val mult : constr Lazy.t + val opp : constr Lazy.t + val minus : constr Lazy.t (* building a coq number *) - val mk : Bigint.bigint -> Term.constr + val mk : Bigint.bigint -> constr (* parsing a term (one level, except if a number is found) *) - val parse_term : Term.constr -> parse_term + val parse_term : constr -> parse_term (* parsing a relation expression, including = < <= >= > *) - val parse_rel : [ `NF ] Proofview.Goal.t -> Term.constr -> parse_rel + val parse_rel : [ `NF ] Proofview.Goal.t -> constr -> parse_rel (* Is a particular term only made of numbers and + * - ? *) - val get_scalar : Term.constr -> Bigint.bigint option + val get_scalar : constr -> Bigint.bigint option end (* Currently, we only use Z numbers *) diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 661485aeeb..430b608f4c 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 @@ -27,8 +28,6 @@ let pp i = print_int i; print_newline (); flush stdout (* More readable than the prefix notation *) let (>>) = Tacticals.New.tclTHEN -let mkApp = Term.mkApp - (* \section{Types} \subsection{How to walk in a term} To represent how to get to a proposition. Only choice points are @@ -68,14 +67,14 @@ type comparaison = Eq | Leq | Geq | Gt | Lt | Neq (it could contains some [Term.Var] but no [Term.Rel]). So no need to lift when breaking or creating arrows. *) type oproposition = - Pequa of Term.constr * oequation (* constr = copy of the Coq formula *) + Pequa of constr * oequation (* constr = copy of the Coq formula *) | Ptrue | Pfalse | Pnot of oproposition | Por of int * oproposition * oproposition | Pand of int * oproposition * oproposition | Pimp of int * oproposition * oproposition - | Pprop of Term.constr + | Pprop of constr (* The equations *) and oequation = { @@ -102,9 +101,9 @@ and oequation = { type environment = { (* La liste des termes non reifies constituant l'environnement global *) - mutable terms : Term.constr list; + mutable terms : constr list; (* La meme chose pour les propositions *) - mutable props : Term.constr list; + mutable props : constr list; (* Traduction des indices utilisés ici en les indices finaux utilisés par * la tactique Omega après dénombrement des variables utiles *) real_indices : int IntHtbl.t; @@ -219,7 +218,7 @@ let display_omega_var i = Printf.sprintf "OV%d" i calcul des variables utiles. *) let add_reified_atom t env = - try List.index0 Term.eq_constr t env.terms + try List.index0 Constr.equal t env.terms with Not_found -> let i = List.length env.terms in env.terms <- env.terms @ [t]; i @@ -237,7 +236,7 @@ let set_reified_atom v t env = (* \subsection{Gestion de l'environnement de proposition pour Omega} *) (* ajout d'une proposition *) let add_prop env t = - try List.index0 Term.eq_constr t env.props + try List.index0 Constr.equal t env.props with Not_found -> let i = List.length env.props in env.props <- env.props @ [t]; i @@ -560,7 +559,7 @@ let reify_hyp env gl i = | LocalDef (_,d,t) when Z.is_int_typ gl (EConstr.Unsafe.to_constr t) -> let d = EConstr.Unsafe.to_constr d in let dummy = Lazy.force coq_True in - let p = mk_equation env ctxt dummy Eq (Term.mkVar i) d in + let p = mk_equation env ctxt dummy Eq (mkVar i) d in i,Defined,p | LocalDef (_,_,t) | LocalAssum (_,t) -> let t = EConstr.Unsafe.to_constr t in @@ -1012,7 +1011,7 @@ let resolution unsafe env (reified_concl,reified_hyps) systems_list = (fun id -> match Id.Map.find id reified_hyps with | Defined,p -> - reified_of_proposition env p, mk_refl (Term.mkVar id) + reified_of_proposition env p, mk_refl (mkVar id) | Assumed,p -> reified_of_proposition env (maximize_prop useful_equa_ids p), EConstr.mkVar id diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 9f02388c39..150c253a7a 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -13,6 +13,7 @@ open Ltac_plugin open CErrors open Util open Term +open Constr open Tacmach open Proof_search open Context.Named.Declaration @@ -82,7 +83,7 @@ let make_atom atom_env term= let term = EConstr.Unsafe.to_constr term in try let (_,i)= - List.find (fun (t,_)-> eq_constr term t) atom_env.env + List.find (fun (t,_)-> Constr.equal term t) atom_env.env in Atom i with Not_found -> let i=atom_env.next in diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli index bec18f6df8..b2285a4a11 100644 --- a/plugins/rtauto/refl_tauto.mli +++ b/plugins/rtauto/refl_tauto.mli @@ -10,7 +10,7 @@ type atom_env= {mutable next:int; - mutable env:(Term.constr*int) list} + mutable env:(Constr.t*int) list} val make_form : atom_env -> Goal.goal Evd.sigma -> EConstr.types -> Proof_search.form diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index b8fae2494f..9e4b896f8e 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -10,7 +10,7 @@ open Ltac_plugin open Pp open Util open Names -open Term +open Constr open EConstr open Vars open CClosure @@ -58,13 +58,13 @@ let rec mk_clos_but f_map subs t = match f_map (global_of_constr_nofail t) with | Some map -> tag_arg (mk_clos_but f_map subs) map subs (-1) t | None -> - (match kind_of_term t with + (match Constr.kind t with App(f,args) -> mk_clos_app_but f_map subs f args 0 | Prod _ -> mk_clos_deep (mk_clos_but f_map) subs t | _ -> mk_atom t) and mk_clos_app_but f_map subs f args n = - let open Term in + let open Constr in if n >= Array.length args then mk_atom(mkApp(f, args)) else let fargs, args' = Array.chop n args in @@ -151,7 +151,7 @@ let ic_unsafe c = (*FIXME remove *) EConstr.of_constr (fst (Constrintern.interp_constr env sigma c)) let decl_constant na ctx c = - let open Term in + let open Constr in let vars = Univops.universes_of_constr c in let ctx = Univops.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in mkConst(declare_constant (Id.of_string na) @@ -346,11 +346,7 @@ let _ = add_map "ring" let pr_constr c = pr_econstr c -module M = struct - type t = Term.constr - let compare = Term.compare -end -module Cmap = Map.Make(M) +module Cmap = Map.Make(Constr) let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table" let from_name = Summary.ref Spmap.empty ~name:"ring-tac-name-table" @@ -395,7 +391,7 @@ let subst_th (subst,th) = let posttac'= Tacsubst.subst_tactic subst th.ring_post_tac in if c' == th.ring_carrier && eq' == th.ring_req && - Term.eq_constr set' th.ring_setoid && + Constr.equal set' th.ring_setoid && ext' == th.ring_ext && morph' == th.ring_morph && th' == th.ring_th && @@ -933,7 +929,7 @@ let field_equality evd r inv req = inv_m_lem let add_field_theory0 name fth eqth morphth cst_tac inj (pre,post) power sign odiv = - let open Term in + let open Constr in check_required_library (cdir@["Field_tac"]); let (sigma,fth) = ic fth in let env = Global.env() in diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli index d37582bd79..c26fcc8d1f 100644 --- a/plugins/setoid_ring/newring_ast.mli +++ b/plugins/setoid_ring/newring_ast.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term +open Constr open Libnames open Constrexpr open Tacexpr diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index d37c676e38..c1d7e62785 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -12,6 +12,7 @@ open Util open Names open Evd open Term +open Constr open Termops open Printer open Locusops @@ -227,7 +228,7 @@ let isAppInd gl c = let interp_refine ist gl rc = let constrvars = Tacinterp.extract_ltac_constr_values ist (pf_env gl) in let vars = { Glob_ops.empty_lvar with - Glob_term.ltac_constrs = constrvars; ltac_genargs = ist.Tacinterp.lfun + Ltac_pretype.ltac_constrs = constrvars; ltac_genargs = ist.Tacinterp.lfun } in let kind = Pretyping.OfType (pf_concl gl) in let flags = { @@ -465,7 +466,6 @@ let ssrevaltac ist gtac = (* but stripping global ones. We use the variable names to encode the *) (* the number of dependencies, so that the transformation is reversible. *) -open Term let env_size env = List.length (Environ.named_context env) let pf_concl gl = EConstr.Unsafe.to_constr (pf_concl gl) @@ -491,23 +491,23 @@ let pf_abs_evars2 gl rigid (sigma, c0) = | NamedDecl.LocalAssum (x,t) -> mkNamedProd x t c in let t = Context.Named.fold_inside abs_dc ~init:evi.evar_concl dc in nf_evar sigma t in - let rec put evlist c = match kind_of_term c with + let rec put evlist c = match Constr.kind c with | Evar (k, a) -> if List.mem_assoc k evlist || Evd.mem sigma0 k || List.mem k rigid then evlist else let n = max 0 (Array.length a - nenv) in let t = abs_evar n k in (k, (n, t)) :: put evlist t - | _ -> fold_constr put evlist c in + | _ -> Constr.fold put evlist c in let evlist = put [] c0 in if evlist = [] then 0, EConstr.of_constr c0,[], ucst else let rec lookup k i = function | [] -> 0, 0 | (k', (n, _)) :: evl -> if k = k' then i, n else lookup k (i + 1) evl in - let rec get i c = match kind_of_term c with + let rec get i c = match Constr.kind c with | Evar (ev, a) -> let j, n = lookup ev i evlist in - if j = 0 then map_constr (get i) c else if n = 0 then mkRel j else + if j = 0 then Constr.map (get i) c else if n = 0 then mkRel j else mkApp (mkRel j, Array.init n (fun k -> get i a.(n - 1 - k))) - | _ -> map_constr_with_binders ((+) 1) get i c in + | _ -> Constr.map_with_binders ((+) 1) get i c in let rec loop c i = function | (_, (n, t)) :: evl -> loop (mkLambda (mk_evar_name n, get (i - 1) t, c)) (i - 1) evl @@ -551,7 +551,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) = | NamedDecl.LocalAssum (x,t) -> mkNamedProd x t c in let t = Context.Named.fold_inside abs_dc ~init:evi.evar_concl dc in nf_evar sigma0 (nf_evar sigma t) in - let rec put evlist c = match kind_of_term c with + let rec put evlist c = match Constr.kind c with | Evar (k, a) -> if List.mem_assoc k evlist || Evd.mem sigma0 k then evlist else let n = max 0 (Array.length a - nenv) in @@ -560,7 +560,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) = (pf_env gl) sigma (EConstr.of_constr (Evd.evar_concl (Evd.find sigma k))) in let is_prop = k_ty = InProp in let t = abs_evar n k in (k, (n, t, is_prop)) :: put evlist t - | _ -> fold_constr put evlist c in + | _ -> Constr.fold put evlist c in let evlist = put [] c0 in if evlist = [] then 0, c0 else let pr_constr t = Printer.pr_econstr (Reductionops.nf_beta (project gl) (EConstr.of_constr t)) in @@ -588,17 +588,17 @@ let pf_abs_evars_pirrel gl (sigma, c0) = let rec lookup k i = function | [] -> 0, 0 | (k', (n,_,_)) :: evl -> if k = k' then i,n else lookup k (i + 1) evl in - let rec get evlist i c = match kind_of_term c with + let rec get evlist i c = match Constr.kind c with | Evar (ev, a) -> let j, n = lookup ev i evlist in - if j = 0 then map_constr (get evlist i) c else if n = 0 then mkRel j else + if j = 0 then Constr.map (get evlist i) c else if n = 0 then mkRel j else mkApp (mkRel j, Array.init n (fun k -> get evlist i a.(n - 1 - k))) - | _ -> map_constr_with_binders ((+) 1) (get evlist) i c in + | _ -> Constr.map_with_binders ((+) 1) (get evlist) i c in let rec app extra_args i c = match decompose_app c with | hd, args when isRel hd && destRel hd = i -> let j = destRel hd in mkApp (mkRel j, Array.of_list (List.map (Vars.lift (i-1)) extra_args @ args)) - | _ -> map_constr_with_binders ((+) 1) (app extra_args) i c in + | _ -> Constr.map_with_binders ((+) 1) (app extra_args) i c in let rec loopP evlist c i = function | (_, (n, t, _)) :: evl -> let t = get evlist (i - 1) t in @@ -645,7 +645,7 @@ let pf_abs_cterm gl n c0 = let c0 = EConstr.Unsafe.to_constr c0 in let noargs = [|0|] in let eva = Array.make n noargs in - let rec strip i c = match kind_of_term c with + let rec strip i c = match Constr.kind c with | App (f, a) when isRel f -> let j = i - destRel f in if j >= n || eva.(j) = noargs then mkApp (f, Array.map (strip i) a) else @@ -653,8 +653,8 @@ let pf_abs_cterm gl n c0 = let nd = Array.length dp - 1 in let mkarg k = strip i a.(if k < nd then dp.(k + 1) - j else k + dp.(0)) in mkApp (f, Array.init (Array.length a - dp.(0)) mkarg) - | _ -> map_constr_with_binders ((+) 1) strip i c in - let rec strip_ndeps j i c = match kind_of_term c with + | _ -> Constr.map_with_binders ((+) 1) strip i c in + let rec strip_ndeps j i c = match Constr.kind c with | Prod (x, t, c1) when i < j -> let dl, c2 = strip_ndeps j (i + 1) c1 in if Vars.noccurn 1 c2 then dl, Vars.lift (-1) c2 else @@ -665,7 +665,7 @@ let pf_abs_cterm gl n c0 = if Vars.noccurn 1 c2 then dl, Vars.lift (-1) c2 else i :: dl, mkLetIn (x, strip i b, strip i t, c2) | _ -> [], strip i c in - let rec strip_evars i c = match kind_of_term c with + let rec strip_evars i c = match Constr.kind c with | Lambda (x, t1, c1) when i < n -> let na = nb_evar_deps x in let dl, t2 = strip_ndeps (i + na) i t1 in @@ -760,7 +760,7 @@ let clear_with_wilds wilds clr0 gl = let id = NamedDecl.get_id nd in if List.mem id clr || not (List.mem id wilds) then clr else let vars = Termops.global_vars_set_of_decl (pf_env gl) (project gl) nd in - let occurs id' = Idset.mem id' vars in + let occurs id' = Id.Set.mem id' vars in if List.exists occurs clr then id :: clr else clr in Proofview.V82.of_tactic (Tactics.clear (Context.Named.fold_inside extend_clr ~init:clr0 (Tacmach.pf_hyps gl))) gl diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 2eadd5f26c..c399451941 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -190,7 +190,7 @@ val pf_merge_uc_of : val constr_name : evar_map -> EConstr.t -> Name.t val pf_type_of : Goal.goal Evd.sigma -> - Term.constr -> Goal.goal Evd.sigma * Term.types + Constr.constr -> Goal.goal Evd.sigma * Constr.types val pfe_type_of : Goal.goal Evd.sigma -> EConstr.t -> Goal.goal Evd.sigma * EConstr.types @@ -220,7 +220,7 @@ val new_wild_id : tac_ctx -> Names.Id.t * tac_ctx val pf_fresh_global : Globnames.global_reference -> Goal.goal Evd.sigma -> - Term.constr * Goal.goal Evd.sigma + Constr.constr * Goal.goal Evd.sigma val is_discharged_id : Id.t -> bool val mk_discharged_id : Id.t -> Id.t @@ -232,7 +232,7 @@ val new_tmp_id : val mk_anon_id : string -> Goal.goal Evd.sigma -> Id.t val pf_abs_evars_pirrel : Goal.goal Evd.sigma -> - evar_map * Term.constr -> int * Term.constr + evar_map * Constr.constr -> int * Constr.constr val pf_nbargs : Goal.goal Evd.sigma -> EConstr.t -> int val gen_tmp_ids : ?ist:Geninterp.interp_sign -> diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 832044909c..26b5c57675 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -396,7 +396,7 @@ let revtoptac n0 gl = let equality_inj l b id c gl = let msg = ref "" in - try Proofview.V82.of_tactic (Equality.inj l b None c) gl + try Proofview.V82.of_tactic (Equality.inj None l b None c) gl with | Ploc.Exc(_,CErrors.UserError (_,s)) | CErrors.UserError (_,s) diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 95ca6f49ad..e82f222b9c 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -11,13 +11,14 @@ open Ltac_plugin open Util open Names +open Term +open Constr open Vars open Locus open Printer open Globnames open Termops open Tacinterp -open Term open Ssrmatching_plugin open Ssrmatching @@ -316,7 +317,7 @@ let rw_progress rhs lhs ise = not (EConstr.eq_constr ise lhs (Evarutil.nf_evar i (* such a generic Leibnitz equation -- short of inspecting the type *) (* of the elimination lemmas. *) -let rec strip_prod_assum c = match Term.kind_of_term c with +let rec strip_prod_assum c = match Constr.kind c with | Prod (_, _, c') -> strip_prod_assum c' | LetIn (_, v, _, c') -> strip_prod_assum (subst1 v c) | Cast (c', _, _) -> strip_prod_assum c' diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index d01bdc1b9e..29e96ec59f 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -32,6 +32,7 @@ let ssrposetac ist (id, (_, t)) gl = open Pp open Term +open Constr let ssrsettac ist id ((_, (pat, pty)), (_, occ)) gl = let pat = interp_cpattern ist gl pat (Option.map snd pty) in @@ -59,10 +60,10 @@ let rec is_Evar_or_CastedMeta sigma x = (EConstr.isCast sigma x && is_Evar_or_CastedMeta sigma (pi1 (EConstr.destCast sigma x))) let occur_existential_or_casted_meta c = - let rec occrec c = match kind_of_term c with + let rec occrec c = match Constr.kind c with | Evar _ -> raise Not_found | Cast (m,_,_) when isMeta m -> raise Not_found - | _ -> iter_constr occrec c + | _ -> Constr.iter occrec c in try occrec c; false with Not_found -> true open Printer @@ -84,12 +85,12 @@ let pf_find_abstract_proof check_lock gl abstract_n = let fire gl t = EConstr.Unsafe.to_constr (Reductionops.nf_evar (project gl) (EConstr.of_constr t)) in let abstract, gl = pf_mkSsrConst "abstract" gl in let l = Evd.fold_undefined (fun e ei l -> - match kind_of_term ei.Evd.evar_concl with + match Constr.kind ei.Evd.evar_concl with | App(hd, [|ty; n; lock|]) when (not check_lock || (occur_existential_or_casted_meta (fire gl ty) && is_Evar_or_CastedMeta (project gl) (EConstr.of_constr @@ fire gl lock))) && - Term.eq_constr hd (EConstr.Unsafe.to_constr abstract) && Term.eq_constr n abstract_n -> e::l + Constr.equal hd (EConstr.Unsafe.to_constr abstract) && Constr.equal n abstract_n -> e::l | _ -> l) (project gl) [] in match l with | [e] -> e @@ -286,7 +287,7 @@ let ssrabstract ist gens (*last*) gl = let p = mkApp (proj2,[|ty;concl;p|]) in let concl = mkApp(prod,[|ty; concl|]) in pf_unify_HO gl concl t, p - | App(hd, [|left; right|]) when Term.eq_constr hd prod -> + | App(hd, [|left; right|]) when Term.Constr.equal hd prod -> find_hole (mkApp (proj1,[|left;right;p|])) left *) | _ -> errorstrm(strbrk"abstract constant "++pr_econstr abstract_n++ diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 507b4631b0..36dce37aea 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -9,7 +9,8 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) open Names -open Term +module CoqConstr = Constr +open CoqConstr open Termops open Constrexpr open Constrexpr_ops @@ -364,7 +365,7 @@ let coerce_search_pattern_to_sort hpat = let interp_head_pat hpat = let filter_head, p = coerce_search_pattern_to_sort hpat in - let rec loop c = match kind_of_term c with + let rec loop c = match CoqConstr.kind c with | Cast (c', _, _) -> loop c' | Prod (_, _, c') -> loop c' | LetIn (_, _, _, c') -> loop c' diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index e3e34616bf..d5c9e4988e 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -18,10 +18,13 @@ let frozen_lexer = CLexer.get_keyword_state () ;; open Ltac_plugin open Names open Pp -open Pcoq open Genarg open Stdarg open Term +module CoqConstr = Constr +open CoqConstr +open Pcoq +open Pcoq.Constr open Vars open Libnames open Tactics @@ -35,10 +38,8 @@ open Evd open Tacexpr open Tacinterp open Pretyping -open Constr open Ppconstr open Printer - open Globnames open Misctypes open Decl_kinds @@ -73,7 +74,7 @@ let pp s = !pp_ref s (** Utils {{{ *****************************************************************) let env_size env = List.length (Environ.named_context env) let safeDestApp c = - match kind_of_term c with App (f, a) -> f, a | _ -> c, [| |] + match kind c with App (f, a) -> f, a | _ -> c, [| |] (* Toplevel constr must be globalized twice ! *) let glob_constr ist genv = function | _, Some ce -> @@ -325,7 +326,7 @@ let unif_FO env ise p c = let nf_open_term sigma0 ise c = let c = EConstr.Unsafe.to_constr c in let s = ise and s' = ref sigma0 in - let rec nf c' = match kind_of_term c' with + let rec nf c' = match kind c' with | Evar ex -> begin try nf (existential_value s ex) with _ -> let k, a = ex in let a' = Array.map nf a in @@ -333,7 +334,7 @@ let nf_open_term sigma0 ise c = s' := Evd.add !s' k (Evarutil.nf_evar_info s (Evd.find s k)); mkEvar (k, a') end - | _ -> map_constr nf c' in + | _ -> map nf c' in let copy_def k evi () = if evar_body evi != Evd.Evar_empty then () else match Evd.evar_body (Evd.find s k) with @@ -365,7 +366,7 @@ let pf_unify_HO gl t1 t2 = re_sig si sigma (* This is what the definition of iter_constr should be... *) -let iter_constr_LR f c = match kind_of_term c with +let iter_constr_LR f c = match kind c with | Evar (k, a) -> Array.iter f a | Cast (cc, _, t) -> f cc; f t | Prod (_, t, b) | Lambda (_, t, b) -> f t; f b @@ -418,14 +419,14 @@ let all_ok _ _ = true let proj_nparams c = try 1 + Recordops.find_projection_nparams (ConstRef c) with _ -> 0 -let isRigid c = match kind_of_term c with +let isRigid c = match kind c with | Prod _ | Sort _ | Lambda _ | Case _ | Fix _ | CoFix _ -> true | _ -> false let hole_var = mkVar (Id.of_string "_") let pr_constr_pat c0 = let rec wipe_evar c = - if isEvar c then hole_var else map_constr wipe_evar c in + if isEvar c then hole_var else map wipe_evar c in pr_constr (wipe_evar c0) (* Turn (new) evars into metas *) @@ -433,11 +434,11 @@ let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 = let ise = ref ise0 in let sigma = ref ise0 in let nenv = env_size env + if hack then 1 else 0 in - let rec put c = match kind_of_term c with + let rec put c = match kind c with | Evar (k, a as ex) -> begin try put (existential_value !sigma ex) with NotInstantiatedEvar -> - if Evd.mem sigma0 k then map_constr put c else + if Evd.mem sigma0 k then map put c else let evi = Evd.find !sigma k in let dc = List.firstn (max 0 (Array.length a - nenv)) (evar_filtered_context evi) in let abs_dc (d, c) = function @@ -452,7 +453,7 @@ let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 = sigma := Evd.define k (applistc (mkMeta m) a) !sigma; put (existential_value !sigma ex) end - | _ -> map_constr put c in + | _ -> map put c in let c1 = put c0 in !ise, c1 (* Compile a match pattern from a term; t is the term to fill. *) @@ -462,7 +463,7 @@ let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p = let f, a = Reductionops.whd_betaiota_stack ise (EConstr.of_constr p) in let f = EConstr.Unsafe.to_constr f in let a = List.map EConstr.Unsafe.to_constr a in - match kind_of_term f with + match kind f with | Const (p,_) -> let np = proj_nparams p in if np = 0 || np > List.length a then KpatConst, f, a else @@ -490,7 +491,7 @@ let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p = (* kind and arity for Proj and Flex patterns. *) let ungen_upat lhs (sigma, uc, t) u = let f, a = safeDestApp lhs in - let k = match kind_of_term f with + let k = match kind f with | Var _ | Ind _ | Construct _ -> KpatFixed | Const _ -> KpatConst | Evar (k, _) -> if is_defined sigma k then raise NoMatch else KpatEvar k @@ -502,14 +503,14 @@ let ungen_upat lhs (sigma, uc, t) u = let nb_cs_proj_args pc f u = let na k = List.length (snd (lookup_canonical_conversion (ConstRef pc, k))).o_TCOMPS in - let nargs_of_proj t = match kind_of_term t with + let nargs_of_proj t = match kind t with | App(_,args) -> Array.length args | Proj _ -> 0 (* if splay_app calls expand_projection, this has to be the number of arguments including the projected *) | _ -> assert false in - try match kind_of_term f with + try match kind f with | Prod _ -> na Prod_cs - | Sort s -> na (Sort_cs (family_of_sort s)) + | Sort s -> na (Sort_cs (Sorts.family s)) | Const (c',_) when Constant.equal c' pc -> nargs_of_proj u.up_f | Proj (c',_) when Constant.equal (Projection.constant c') pc -> nargs_of_proj u.up_f | Var _ | Ind _ | Construct _ | Const _ -> na (Const_cs (global_of_constr f)) @@ -517,22 +518,22 @@ let nb_cs_proj_args pc f u = with Not_found -> -1 let isEvar_k k f = - match kind_of_term f with Evar (k', _) -> k = k' | _ -> false + match kind f with Evar (k', _) -> k = k' | _ -> false let nb_args c = - match kind_of_term c with App (_, a) -> Array.length a | _ -> 0 + match kind c with App (_, a) -> Array.length a | _ -> 0 let mkSubArg i a = if i = Array.length a then a else Array.sub a 0 i let mkSubApp f i a = if i = 0 then f else mkApp (f, mkSubArg i a) let splay_app ise = - let rec loop c a = match kind_of_term c with + let rec loop c a = match kind c with | App (f, a') -> loop f (Array.append a' a) | Cast (c', _, _) -> loop c' a | Evar ex -> (try loop (existential_value ise ex) a with _ -> c, a) | _ -> c, a in - fun c -> match kind_of_term c with + fun c -> match kind c with | App (f, a) -> loop f a | Cast _ | Evar _ -> loop c [| |] | _ -> c, [| |] @@ -541,8 +542,8 @@ let filter_upat i0 f n u fpats = let na = Array.length u.up_a in if n < na then fpats else let np = match u.up_k with - | KpatConst when Term.eq_constr u.up_f f -> na - | KpatFixed when Term.eq_constr u.up_f f -> na + | KpatConst when equal u.up_f f -> na + | KpatFixed when equal u.up_f f -> na | KpatEvar k when isEvar_k k f -> na | KpatLet when isLetIn f -> na | KpatLam when isLambda f -> na @@ -554,7 +555,7 @@ let filter_upat i0 f n u fpats = if np < na then fpats else let () = if !i0 < np then i0 := n in (u, np) :: fpats -let eq_prim_proj c t = match kind_of_term t with +let eq_prim_proj c t = match kind t with | Proj(p,_) -> Constant.equal (Projection.constant p) c | _ -> false @@ -562,13 +563,13 @@ let filter_upat_FO i0 f n u fpats = let np = nb_args u.up_FO in if n < np then fpats else let ok = match u.up_k with - | KpatConst -> Term.eq_constr u.up_f f - | KpatFixed -> Term.eq_constr u.up_f f + | KpatConst -> equal u.up_f f + | KpatFixed -> equal u.up_f f | KpatEvar k -> isEvar_k k f | KpatLet -> isLetIn f | KpatLam -> isLambda f | KpatRigid -> isRigid f - | KpatProj pc -> Term.eq_constr f (mkConst pc) || eq_prim_proj pc f + | KpatProj pc -> equal f (mkConst pc) || eq_prim_proj pc f | KpatFlex -> i0 := n; true in if ok then begin if !i0 < np then i0 := np; (u, np) :: fpats end else fpats @@ -741,13 +742,13 @@ let mk_tpattern_matcher ?(all_instances=false) let x, pv, t, pb = destLetIn u.up_f in let env' = Environ.push_rel (Context.Rel.Declaration.LocalAssum(x, t)) env in - let match_let f = match kind_of_term f with + let match_let f = match kind f with | LetIn (_, v, _, b) -> unif_EQ env sigma pv v && unif_EQ env' sigma pb b | _ -> false in match_let - | KpatFixed -> Term.eq_constr u.up_f - | KpatConst -> Term.eq_constr u.up_f + | KpatFixed -> equal u.up_f + | KpatConst -> equal u.up_f | KpatLam -> fun c -> - (match kind_of_term c with + (match kind c with | Lambda _ -> unif_EQ env sigma u.up_f c | _ -> false) | _ -> unif_EQ env sigma u.up_f in @@ -778,8 +779,8 @@ let rec uniquize = function let t1 = nf_evar sigma1 t1 in let f1 = nf_evar sigma1 f1 in let a1 = Array.map (nf_evar sigma1) a1 in - not (Term.eq_constr t t1 && - Term.eq_constr f f1 && CArray.for_all2 Term.eq_constr a a1) in + not (equal t t1 && + equal f f1 && CArray.for_all2 equal a a1) in x :: uniquize (List.filter neq xs) in ((fun env c h ~k -> @@ -1018,7 +1019,7 @@ let input_ssrtermkind strm = match stream_nth 0 strm with | Tok.KEYWORD "(" -> '(' | Tok.KEYWORD "@" -> '@' | _ -> ' ' -let ssrtermkind = Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind +let ssrtermkind = Pcoq.Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind let interp_ssrterm _ gl t = Tacmach.project gl, t @@ -1100,7 +1101,7 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = let decodeG t f g = decode ist (mkG t) f g in let bad_enc id _ = CErrors.anomaly (str"bad encoding for pattern "++str id++str".") in let cleanup_XinE h x rp sigma = - let h_k = match kind_of_term h with Evar (k,_) -> k | _ -> assert false in + let h_k = match kind h with Evar (k,_) -> k | _ -> assert false in let to_clean, update = (* handle rename if x is already used *) let ctx = pf_hyps gl in let len = Context.Named.length ctx in @@ -1115,11 +1116,11 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = with Not_found -> ref (Some x), fun _ -> () in let sigma0 = project gl in let new_evars = - let rec aux acc t = match kind_of_term t with + let rec aux acc t = match kind t with | Evar (k,_) -> if k = h_k || List.mem k acc || Evd.mem sigma0 k then acc else (update k; k::acc) - | _ -> fold_constr aux acc t in + | _ -> CoqConstr.fold aux acc t in aux [] (nf_evar sigma rp) in let sigma = List.fold_left (fun sigma e -> @@ -1202,7 +1203,7 @@ let interp_cpattern ist gl red redty = interp_pattern ist gl (T red) redty;; let interp_rpattern ~wit_ssrpatternarg ist gl red = interp_pattern ~wit_ssrpatternarg ist gl red None;; let id_of_pattern = function - | _, T t -> (match kind_of_term t with Var id -> Some id | _ -> None) + | _, T t -> (match kind t with Var id -> Some id | _ -> None) | _ -> None (* The full occurrence set *) @@ -1222,7 +1223,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = Evd.add (Evd.remove sigma e) e {e_def with Evd.evar_body = Evar_empty} in sigma, e_body in let ex_value hole = - match kind_of_term hole with Evar (e,_) -> e | _ -> assert false in + match kind hole with Evar (e,_) -> e | _ -> assert false in let mk_upat_for ?hack env sigma0 (sigma, t) ?(p=t) ok = let sigma,pat= mk_tpattern ?hack env sigma0 (sigma,p) ok L2R (fs sigma t) in sigma, [pat] in @@ -1407,7 +1408,7 @@ let () = let ssrinstancesof ist arg gl = let ok rhs lhs ise = true in -(* not (Term.eq_constr lhs (Evarutil.nf_evar ise rhs)) in *) +(* not (equal lhs (Evarutil.nf_evar ise rhs)) in *) let env, sigma, concl = pf_env gl, project gl, pf_concl gl in let concl = EConstr.Unsafe.to_constr concl in let sigma0, cpat = interp_cpattern ist gl arg None in diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 8e2a1a7176..8ab666f7ea 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -6,7 +6,7 @@ open Genarg open Tacexpr open Environ open Evd -open Term +open Constr (** ******** Small Scale Reflection pattern matching facilities ************* *) |