diff options
Diffstat (limited to 'plugins')
67 files changed, 384 insertions, 358 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 361981c5b..04ff11fc4 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -443,7 +443,7 @@ let cc_tactic depth additionnal_terms = let open Glob_term in let env = Proofview.Goal.env gl in let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in - let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in + let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) in let pr_missing (c, missing) = let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in let holes = List.init missing (fun _ -> hole) in diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index bebd27e11..4ede11b5c 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -596,19 +596,18 @@ let warns () = let rec locate_ref = function | [] -> [],[] - | r::l -> - let q = qualid_of_reference r in - let mpo = try Some (Nametab.locate_module q.CAst.v) with Not_found -> None + | qid::l -> + let mpo = try Some (Nametab.locate_module qid) with Not_found -> None and ro = - try Some (Smartlocate.global_with_alias r) + try Some (Smartlocate.global_with_alias qid) with Nametab.GlobalizationError _ | UserError _ -> None in match mpo, ro with - | None, None -> Nametab.error_global_not_found q + | None, None -> Nametab.error_global_not_found qid | None, Some r -> let refs,mps = locate_ref l in r::refs,mps | Some mp, None -> let refs,mps = locate_ref l in refs,mp::mps | Some mp, Some r -> - warning_ambiguous_name (q.CAst.v,mp,r); + warning_ambiguous_name (qid,mp,r); let refs,mps = locate_ref l in refs,mp::mps (*s Recursive extraction in the Coq toplevel. The vernacular command is @@ -646,7 +645,7 @@ let separate_extraction lr = is \verb!Extraction! [qualid]. *) let simple_extraction r = - Vernacentries.dump_global CAst.(make (Misctypes.AN r)); + Vernacentries.dump_global CAst.(make (Constrexpr.AN r)); match locate_ref [r] with | ([], [mp]) as p -> full_extr None p | [r],[] -> diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 77f1fb5ef..54fde2ca4 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -13,14 +13,14 @@ open Names open Libnames -val simple_extraction : reference -> unit -val full_extraction : string option -> reference list -> unit -val separate_extraction : reference list -> unit +val simple_extraction : qualid -> unit +val full_extraction : string option -> qualid list -> unit +val separate_extraction : qualid list -> unit val extraction_library : bool -> Id.t -> unit (* For the test-suite : extraction to a temporary file + ocamlc on it *) -val extract_and_compile : reference list -> unit +val extract_and_compile : qualid list -> unit (* For debug / external output via coqtop.byte + Drop : *) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 5aee70194..3a61c7747 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -1065,11 +1065,15 @@ let extract_constant env kn cb = (match cb.const_body with | Undef _ -> warn_info (); mk_typ_ax () | Def c -> - (match cb.const_proj with + (match Environ.is_projection kn env with | false -> mk_typ (get_body c) | true -> let pb = lookup_projection (Projection.make kn false) env in - mk_typ (EConstr.of_constr pb.proj_body)) + (** FIXME: handle mutual records *) + let ind = (pb.Declarations.proj_ind, 0) in + let bodies = Inductiveops.legacy_match_projection env ind in + let body = bodies.(pb.Declarations.proj_arg) in + mk_typ (EConstr.of_constr body)) | OpaqueDef c -> add_opaque r; if access_opaque () then mk_typ (get_opaque env c) @@ -1078,11 +1082,15 @@ let extract_constant env kn cb = (match cb.const_body with | Undef _ -> warn_info (); mk_ax () | Def c -> - (match cb.const_proj with + (match Environ.is_projection kn env with | false -> mk_def (get_body c) | true -> let pb = lookup_projection (Projection.make kn false) env in - mk_def (EConstr.of_constr pb.proj_body)) + (** FIXME: handle mutual records *) + let ind = (pb.Declarations.proj_ind, 0) in + let bodies = Inductiveops.legacy_match_projection env ind in + let body = bodies.(pb.Declarations.proj_arg) in + mk_def (EConstr.of_constr body)) | OpaqueDef c -> add_opaque r; if access_opaque () then mk_def (get_opaque env c) diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 5bf944434..a8baeaf1b 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -194,17 +194,17 @@ val find_custom_match : ml_branch array -> string (*s Extraction commands. *) val extraction_language : lang -> unit -val extraction_inline : bool -> reference list -> unit +val extraction_inline : bool -> qualid list -> unit val print_extraction_inline : unit -> Pp.t val reset_extraction_inline : unit -> unit val extract_constant_inline : - bool -> reference -> string list -> string -> unit + bool -> qualid -> string list -> string -> unit val extract_inductive : - reference -> string -> string list -> string option -> unit + qualid -> string -> string list -> string option -> unit type int_or_id = ArgInt of int | ArgId of Id.t -val extraction_implicit : reference -> int_or_id list -> unit +val extraction_implicit : qualid -> int_or_id list -> unit (*s Table of blacklisted filenames *) diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 30deb6f49..7e54bc8ad 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -17,7 +17,6 @@ open Goptions open Tacmach.New open Tacticals.New open Tacinterp -open Libnames open Stdarg open Tacarg open Pcoq.Prim @@ -127,7 +126,7 @@ let normalize_evaluables= open Genarg open Ppconstr open Printer -let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_reference +let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_qualid let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (pr_or_var (fun x -> pr_global (snd x))) let pr_firstorder_using_typed _ _ _ = Pptactic.pr_auto_using pr_global diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 22a3e1f67..85f493956 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -22,7 +22,6 @@ open Reductionops open Formula open Sequent open Names -open Misctypes open Context.Rel.Declaration let compare_instance inst1 inst2= @@ -184,12 +183,12 @@ let right_instance_tac inst continue seq= [introf; Proofview.Goal.enter begin fun gl -> let id0 = List.nth (pf_ids_of_hyps gl) 0 in - split (ImplicitBindings [mkVar id0]) + split (Tactypes.ImplicitBindings [mkVar id0]) end; tclSOLVE [wrap 0 true continue (deepen seq)]]; tclTRY assumption] | Real ((0,t),_) -> - (tclTHEN (split (ImplicitBindings [t])) + (tclTHEN (split (Tactypes.ImplicitBindings [t])) (tclSOLVE [wrap 0 true continue (deepen seq)])) | Real ((m,t),_) -> tclFAIL 0 (Pp.str "not implemented ... yet") diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index a158fc8ff..31496513a 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -627,7 +627,7 @@ let build_scheme fas = Smartlocate.global_with_alias f with Not_found -> user_err ~hdr:"FunInd.build_scheme" - (str "Cannot find " ++ Libnames.pr_reference f) + (str "Cannot find " ++ Libnames.pr_qualid f) in let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in let _ = evd := evd' in @@ -668,7 +668,7 @@ let build_case_scheme fa = try fst (Global.constr_of_global_in_context (Global.env ()) (Smartlocate.global_with_alias f)) with Not_found -> user_err ~hdr:"FunInd.build_case_scheme" - (str "Cannot find " ++ Libnames.pr_reference f) in + (str "Cannot find " ++ Libnames.pr_qualid f) in let first_fun,u = destConst funs in let funs_mp,funs_dp,_ = Constant.repr3 first_fun in let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index 33aeafef8..97f9acdb3 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -36,5 +36,5 @@ exception No_graph_found val make_scheme : Evd.evar_map ref -> (pconstant*Sorts.family) list -> Safe_typing.private_constants Entries.definition_entry list -val build_scheme : (Id.t*Libnames.reference*Sorts.family) list -> unit -val build_case_scheme : (Id.t*Libnames.reference*Sorts.family) -> unit +val build_scheme : (Id.t*Libnames.qualid*Sorts.family) list -> unit +val build_case_scheme : (Id.t*Libnames.qualid*Sorts.family) -> unit diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 0a2741ad1..a2d31780d 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -15,7 +15,8 @@ open Indfun_common open Indfun open Genarg open Stdarg -open Misctypes +open Tacarg +open Tactypes open Pcoq open Pcoq.Prim open Pcoq.Constr @@ -167,7 +168,7 @@ END let pr_fun_scheme_arg (princ_name,fun_name,s) = Names.Id.print princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++ - Libnames.pr_reference fun_name ++ spc() ++ str "Sort " ++ + Libnames.pr_qualid fun_name ++ spc() ++ str "Sort " ++ Termops.pr_sort_family s VERNAC ARGUMENT EXTEND fun_scheme_arg @@ -180,11 +181,11 @@ let warning_error names e = let (e, _) = ExplainErr.process_vernac_interp_error (e, Exninfo.null) in match e with | Building_graph e -> - let names = pr_enum Libnames.pr_reference names in + let names = pr_enum Libnames.pr_qualid names in let error = if do_observe () then (spc () ++ CErrors.print e) else mt () in warn_cannot_define_graph (names,error) | Defining_principle e -> - let names = pr_enum Libnames.pr_reference names in + let names = pr_enum Libnames.pr_qualid names in let error = if do_observe () then CErrors.print e else mt () in warn_cannot_define_principle (names,error) | _ -> raise e diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 3ba3bafa4..6b9b10312 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -10,7 +10,6 @@ open Indfun_common open CErrors open Util open Glob_termops -open Misctypes module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index bb1587507..954fc3bab 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -5,7 +5,6 @@ open CErrors open Util open Names open Decl_kinds -open Misctypes (* Some basic functions to rebuild glob_constr @@ -18,7 +17,7 @@ let mkGLambda(n,t,b) = DAst.make @@ GLambda(n,Explicit,t,b) let mkGProd(n,t,b) = DAst.make @@ GProd(n,Explicit,t,b) let mkGLetIn(n,b,t,c) = DAst.make @@ GLetIn(n,b,t,c) let mkGCases(rto,l,brl) = DAst.make @@ GCases(RegularStyle,rto,l,brl) -let mkGHole () = DAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None) +let mkGHole () = DAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Namegen.IntroAnonymous,None) (* Some basic functions to decompose glob_constrs @@ -109,7 +108,7 @@ let change_vars = | GHole _ as x -> x | GCast(b,c) -> GCast(change_vars mapping b, - Miscops.map_cast_type (change_vars mapping) c) + Glob_ops.map_cast_type (change_vars mapping) c) | GProj(p,c) -> GProj(p, change_vars mapping c) ) rt and change_vars_br mapping ({CAst.loc;v=(idl,patl,res)} as br) = @@ -290,7 +289,7 @@ let rec alpha_rt excluded rt = | GHole _ as rt -> rt | GCast (b,c) -> GCast(alpha_rt excluded b, - Miscops.map_cast_type (alpha_rt excluded) c) + Glob_ops.map_cast_type (alpha_rt excluded) c) | GApp(f,args) -> GApp(alpha_rt excluded f, List.map (alpha_rt excluded) args @@ -440,7 +439,7 @@ let replace_var_by_term x_id term = | GHole _ as rt -> rt | GCast(b,c) -> GCast(replace_var_by_pattern b, - Miscops.map_cast_type replace_var_by_pattern c) + Glob_ops.map_cast_type replace_var_by_pattern c) | GProj(p,c) -> GProj(p,replace_var_by_pattern c) ) x @@ -542,7 +541,7 @@ let expand_as = | GRec _ -> user_err Pp.(str "Not handled GRec") | GCast(b,c) -> GCast(expand_as map b, - Miscops.map_cast_type (expand_as map) c) + Glob_ops.map_cast_type (expand_as map) c) | GCases(sty,po,el,brl) -> GCases(sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, List.map (expand_as_br map) brl) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index efbd029e4..489a40ed0 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -10,7 +10,7 @@ open Libnames open Globnames open Glob_term open Declarations -open Misctypes +open Tactypes open Decl_kinds module RelDecl = Context.Rel.Declaration @@ -362,17 +362,17 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error (*i The next call to mk_rel_id is valid since we have just construct the graph Ensures by : do_built i*) - let f_R_mut = CAst.make @@ Ident (mk_rel_id (List.nth names 0)) in + let f_R_mut = qualid_of_ident @@ mk_rel_id (List.nth names 0) in let ind_kn = fst (locate_with_msg - (pr_reference f_R_mut++str ": Not an inductive type!") + (pr_qualid f_R_mut++str ": Not an inductive type!") locate_ind f_R_mut) in let fname_kn (((fname,_),_,_,_,_),_) = - let f_ref = CAst.map (fun n -> Ident n) fname in - locate_with_msg - (pr_reference f_ref++str ": Not an inductive type!") + let f_ref = qualid_of_ident ?loc:fname.CAst.loc fname.CAst.v in + locate_with_msg + (pr_qualid f_ref++str ": Not an inductive type!") locate_constant f_ref in @@ -477,7 +477,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas let unbounded_eq = let f_app_args = CAst.make @@ Constrexpr.CAppExpl( - (None,CAst.make @@ Ident fname,None) , + (None,qualid_of_ident fname,None) , (List.map (function | {CAst.v=Anonymous} -> assert false @@ -487,7 +487,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas ) ) in - CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (CAst.make @@ Qualid (qualid_of_string "Logic.eq"))), + CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (qualid_of_string "Logic.eq")), [(f_app_args,None);(body,None)]) in let eq = Constrexpr_ops.mkCProdN args unbounded_eq in @@ -544,9 +544,9 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas | None -> let ltof = let make_dir l = DirPath.make (List.rev_map Id.of_string l) in - CAst.make @@ Libnames.Qualid (Libnames.qualid_of_path - (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof"))) - in + Libnames.qualid_of_path + (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof")) + in let fun_from_mes = let applied_mes = Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC wf_arg]) in @@ -727,12 +727,10 @@ let do_generate_principle pconstants on_error register_built interactive_proof () let rec add_args id new_args = CAst.map (function - | CRef (r,_) as b -> - begin match r with - | {CAst.v=Libnames.Ident fname} when Id.equal fname id -> - CAppExpl((None,r,None),new_args) - | _ -> b - end + | CRef (qid,_) as b -> + if qualid_is_ident qid && Id.equal (qualid_basename qid) id then + CAppExpl((None,qid,None),new_args) + else b | CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo.") | CProdN(nal,b1) -> CProdN(List.map (function CLocalAssum (nal,k,b2) -> CLocalAssum (nal,k,add_args id new_args b2) @@ -746,13 +744,10 @@ let rec add_args id new_args = CAst.map (function add_args id new_args b1) | CLetIn(na,b1,t,b2) -> CLetIn(na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2) - | CAppExpl((pf,r,us),exprl) -> - begin - match r with - | {CAst.v=Libnames.Ident fname} when Id.equal fname id -> - CAppExpl((pf,r,us),new_args@(List.map (add_args id new_args) exprl)) - | _ -> CAppExpl((pf,r,us),List.map (add_args id new_args) exprl) - end + | CAppExpl((pf,qid,us),exprl) -> + if qualid_is_ident qid && Id.equal (qualid_basename qid) id then + CAppExpl((pf,qid,us),new_args@(List.map (add_args id new_args) exprl)) + else CAppExpl((pf,qid,us),List.map (add_args id new_args) exprl) | CApp((pf,b),bl) -> CApp((pf,add_args id new_args b), List.map (fun (e,o) -> add_args id new_args e,o) bl) @@ -782,7 +777,7 @@ let rec add_args id new_args = CAst.map (function | CSort _ as b -> b | CCast(b1,b2) -> CCast(add_args id new_args b1, - Miscops.map_cast_type (add_args id new_args) b2) + Glob_ops.map_cast_type (add_args id new_args) b2) | CRecord pars -> CRecord (List.map (fun (e,o) -> e, add_args id new_args o) pars) | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.") @@ -888,7 +883,7 @@ let make_graph (f_ref : GlobRef.t) = | Constrexpr.CLocalAssum (nal,_,_) -> List.map (fun {CAst.loc;v=n} -> CAst.make ?loc @@ - CRef(CAst.make ?loc @@ Libnames.Ident(Nameops.Name.get_id n),None)) + CRef(Libnames.qualid_of_ident ?loc @@ Nameops.Name.get_id n,None)) nal | Constrexpr.CLocalPattern _ -> assert false ) diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index 24304e361..f209fb19f 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -1,5 +1,5 @@ open Names -open Misctypes +open Tactypes val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index c6faa142a..4eee2c7a4 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -31,9 +31,7 @@ let id_of_name = function Name id -> id | _ -> raise Not_found -let locate ref = - let {CAst.v=qid} = qualid_of_reference ref in - Nametab.locate qid +let locate qid = Nametab.locate qid let locate_ind ref = match locate ref with diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 346b21ef2..7e52ee224 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -20,11 +20,11 @@ val array_get_start : 'a array -> 'a array val id_of_name : Name.t -> Id.t -val locate_ind : Libnames.reference -> inductive -val locate_constant : Libnames.reference -> Constant.t +val locate_ind : Libnames.qualid -> inductive +val locate_constant : Libnames.qualid -> Constant.t val locate_with_msg : - Pp.t -> (Libnames.reference -> 'a) -> - Libnames.reference -> 'a + Pp.t -> (Libnames.qualid -> 'a) -> + Libnames.qualid -> 'a val filter_map : ('a -> bool) -> ('a -> 'b) -> 'a list -> 'b list val list_union_eq : diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index cc92a73f0..439274240 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -23,7 +23,7 @@ open Tacticals open Tactics open Indfun_common open Tacmach -open Misctypes +open Tactypes open Termops open Context.Rel.Declaration @@ -239,7 +239,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i List.map (fun decl -> List.map - (fun id -> CAst.make @@ IntroNaming (IntroIdentifier id)) + (fun id -> CAst.make @@ IntroNaming (Namegen.IntroIdentifier id)) (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (RelDecl.get_type decl))))) ) branches @@ -257,7 +257,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i List.fold_right (fun {CAst.v=pat} acc -> match pat with - | IntroNaming (IntroIdentifier id) -> id::acc + | IntroNaming (Namegen.IntroIdentifier id) -> id::acc | _ -> anomaly (Pp.str "Not an identifier.") ) (List.nth intro_pats (pred i)) diff --git a/plugins/funind/invfun.mli b/plugins/funind/invfun.mli index 9151fd0e2..3ddc60920 100644 --- a/plugins/funind/invfun.mli +++ b/plugins/funind/invfun.mli @@ -9,7 +9,7 @@ (************************************************************************) val invfun : - Misctypes.quantified_hypothesis -> + Tactypes.quantified_hypothesis -> Names.GlobRef.t option -> Evar.t Evd.sigma -> Evar.t list Evd.sigma val derive_correctness : diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 72bb8253d..7298342e1 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -37,7 +37,7 @@ open Glob_term open Pretyping open Termops open Constrintern -open Misctypes +open Tactypes open Genredexpr open Equality @@ -1325,7 +1325,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials"); let hook _ _ = let opacity = - let na_ref = CAst.make @@ Libnames.Ident na in + let na_ref = qualid_of_ident na in let na_global = Smartlocate.global_with_alias na_ref in match na_global with ConstRef c -> is_opaque_constant c @@ -1577,7 +1577,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let hook _ _ = let term_ref = Nametab.locate (qualid_of_ident term_id) in let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in - let _ = Extraction_plugin.Table.extraction_inline true [CAst.make @@ Ident term_id] in + let _ = Extraction_plugin.Table.extraction_inline true [qualid_of_ident term_id] in (* message "start second proof"; *) let stop = try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type); diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index faa9e413b..61525cb49 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.ml4 @@ -10,11 +10,13 @@ open Util open Locus -open Misctypes +open Tactypes open Genredexpr open Stdarg open Extraargs +open Tacarg open Names +open Logic DECLARE PLUGIN "ltac_plugin" diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index ea8dcf57d..84f13d213 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -92,7 +92,7 @@ let let_evar name typ = Namegen.next_ident_away_in_goal id (Termops.vars_of_env env) | Name.Name id -> id in - let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in + let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Namegen.IntroFresh id) typ in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Tactics.letin_tac None (Name.Name id) evar None Locusops.nowhere) end diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index 4e7c8b754..dae2582bd 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -19,7 +19,6 @@ open Tacmach open Tacexpr open Taccoerce open Tacinterp -open Misctypes open Locus (** Adding scopes for generic arguments not defined through ARGUMENT EXTEND *) @@ -35,7 +34,7 @@ let () = create_generic_quotation "ident" Pcoq.Prim.ident Stdarg.wit_ident let () = create_generic_quotation "reference" Pcoq.Prim.reference Stdarg.wit_ref let () = create_generic_quotation "uconstr" Pcoq.Constr.lconstr Stdarg.wit_uconstr let () = create_generic_quotation "constr" Pcoq.Constr.lconstr Stdarg.wit_constr -let () = create_generic_quotation "ipattern" Pltac.simple_intropattern Stdarg.wit_intro_pattern +let () = create_generic_quotation "ipattern" Pltac.simple_intropattern wit_intro_pattern let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Stdarg.wit_open_constr let () = let inject (loc, v) = Tacexpr.Tacexp v in diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index ff697e3c7..737147884 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -12,7 +12,6 @@ open Tacexpr open Names open Constrexpr open Glob_term -open Misctypes val wit_orient : bool Genarg.uniform_genarg_type val orient : bool Pcoq.Gram.entry @@ -20,9 +19,9 @@ val pr_orient : bool -> Pp.t val wit_rename : (Id.t * Id.t) Genarg.uniform_genarg_type -val occurrences : (int list or_var) Pcoq.Gram.entry -val wit_occurrences : (int list or_var, int list or_var, int list) Genarg.genarg_type -val pr_occurrences : int list or_var -> Pp.t +val occurrences : (int list Locus.or_var) Pcoq.Gram.entry +val wit_occurrences : (int list Locus.or_var, int list Locus.or_var, int list) Genarg.genarg_type +val pr_occurrences : int list Locus.or_var -> Pp.t val occurrences_of : int list -> Locus.occurrences val wit_natural : int Genarg.uniform_genarg_type diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index cb7183638..660e29ca8 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -24,7 +24,8 @@ open CErrors open Util open Termops open Equality -open Misctypes +open Namegen +open Tactypes open Proofview.Notations open Vernacinterp @@ -604,7 +605,7 @@ let subst_var_with_hole occ tid t = (incr locref; DAst.make ~loc:(Loc.make_loc (!locref,0)) @@ GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous), - Misctypes.IntroAnonymous, None))) + IntroAnonymous, None))) else x | _ -> map_glob_constr_left_to_right substrec x in let t' = substrec t @@ -615,13 +616,13 @@ let subst_hole_with_term occ tc t = let locref = ref 0 in let occref = ref occ in let rec substrec c = match DAst.get c with - | GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s) -> + | GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),IntroAnonymous,s) -> decr occref; if Int.equal !occref 0 then tc else (incr locref; DAst.make ~loc:(Loc.make_loc (!locref,0)) @@ - GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s)) + GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),IntroAnonymous,s)) | _ -> map_glob_constr_left_to_right substrec c in substrec t @@ -792,17 +793,12 @@ END (* ********************************************************************* *) -let eq_constr x y = - Proofview.Goal.enter begin fun gl -> - let env = Tacmach.New.pf_env gl in - let evd = Tacmach.New.project gl in - match EConstr.eq_constr_universes env evd x y with - | Some _ -> Proofview.tclUNIT () - | None -> Tacticals.New.tclFAIL 0 (str "Not equal") - end - TACTIC EXTEND constr_eq -| [ "constr_eq" constr(x) constr(y) ] -> [ eq_constr x y ] +| [ "constr_eq" constr(x) constr(y) ] -> [ Tactics.constr_eq ~strict:false x y ] +END + +TACTIC EXTEND constr_eq_strict +| [ "constr_eq_strict" constr(x) constr(y) ] -> [ Tactics.constr_eq ~strict:true x y ] END TACTIC EXTEND constr_eq_nounivs diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 642e52155..35ed14fc1 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -173,7 +173,7 @@ TACTIC EXTEND convert_concl_no_check | ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x DEFAULTcast ] END -let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_reference +let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_qualid let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Printer.pr_global let glob_hints_path_atom ist = Hints.glob_hints_path_atom @@ -189,7 +189,7 @@ ARGUMENT EXTEND hints_path_atom END let pr_hints_path prc prx pry c = Hints.pp_hints_path c -let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_reference c +let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_qualid c let glob_hints_path ist = Hints.glob_hints_path ARGUMENT EXTEND hints_path diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index ed54320a5..620f14707 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -12,9 +12,10 @@ DECLARE PLUGIN "ltac_plugin" open Util open Pp +open Glob_term open Constrexpr open Tacexpr -open Misctypes +open Namegen open Genarg open Genredexpr open Tok (* necessary for camlp5 *) @@ -26,7 +27,7 @@ open Pcoq.Constr open Pvernac.Vernac_ open Pltac -let fail_default_value = ArgArg 0 +let fail_default_value = Locus.ArgArg 0 let arg_of_expr = function TacArg (loc,a) -> a @@ -34,15 +35,16 @@ let arg_of_expr = function let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) () let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n -let genarg_of_ipattern pat = in_gen (rawwit Stdarg.wit_intro_pattern) pat +let genarg_of_ipattern pat = in_gen (rawwit Tacarg.wit_intro_pattern) pat let genarg_of_uconstr c = in_gen (rawwit Stdarg.wit_uconstr) c let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac -let reference_to_id = CAst.map_with_loc (fun ?loc -> function - | Libnames.Ident id -> id - | Libnames.Qualid _ -> - CErrors.user_err ?loc - (str "This expression should be a simple identifier.")) +let reference_to_id qid = + if Libnames.qualid_is_ident qid then + CAst.make ?loc:qid.CAst.loc @@ Libnames.qualid_basename qid + else + CErrors.user_err ?loc:qid.CAst.loc + (str "This expression should be a simple identifier.") let tactic_mode = Gram.entry_create "vernac:tactic_command" @@ -197,9 +199,8 @@ GEXTEND Gram non ambiguous name where dots are replaced by "_"? Probably too verbose most of the time. *) fresh_id: - [ [ s = STRING -> ArgArg s (*| id = ident -> ArgVar (!@loc,id)*) - | qid = qualid -> let (_pth,id) = Libnames.repr_qualid qid.CAst.v in - ArgVar (CAst.make ~loc:!@loc id) ] ] + [ [ s = STRING -> Locus.ArgArg s (*| id = ident -> Locus.ArgVar (!@loc,id)*) + | qid = qualid -> Locus.ArgVar (CAst.make ~loc:!@loc @@ Libnames.qualid_basename qid) ] ] ; constr_eval: [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> @@ -474,7 +475,7 @@ END VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY | [ "Print" "Ltac" reference(r) ] -> - [ Feedback.msg_notice (Tacintern.print_ltac (Libnames.qualid_of_reference r).CAst.v) ] + [ Feedback.msg_notice (Tacintern.print_ltac r) ] END VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY @@ -482,7 +483,7 @@ VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY [ Tacentries.print_located_tactic r ] END -let pr_ltac_ref = Libnames.pr_reference +let pr_ltac_ref = Libnames.pr_qualid let pr_tacdef_body tacdef_body = let id, redef, body = @@ -509,8 +510,7 @@ VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition | [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => [ VtSideff (List.map (function | TacticDefinition ({CAst.v=r},_) -> r - | TacticRedefinition ({CAst.v=Ident r},_) -> r - | TacticRedefinition ({CAst.v=Qualid q},_) -> snd(repr_qualid q)) l), VtLater + | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater ] -> [ fun ~atts ~st -> let open Vernacinterp in Tacentries.register_ltac (Locality.make_module_locality atts.locality) l; st diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index 352e92c2a..1f56244c7 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -12,7 +12,6 @@ Syntax for the subtac terms and types. Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *) -open Libnames open Constrexpr open Constrexpr_ops open Stdarg @@ -49,7 +48,7 @@ module Tactic = Pltac open Pcoq -let sigref = mkRefC (CAst.make @@ Qualid (Libnames.qualid_of_string "Coq.Init.Specif.sig")) +let sigref loc = mkRefC (Libnames.qualid_of_string ~loc "Coq.Init.Specif.sig") type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type @@ -68,7 +67,7 @@ GEXTEND Gram Constr.closed_binder: [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> - let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in + let typ = mkAppC (sigref !@loc, [mkLambdaC ([id], default_binder_kind, t, c)]) in [CLocalAssum ([id], default_binder_kind, typ)] ] ]; diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index 079001ee4..f1634f156 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -11,7 +11,6 @@ (* Syntax for rewriting with strategies *) open Names -open Misctypes open Locus open Constrexpr open Glob_term @@ -20,6 +19,7 @@ open Extraargs open Tacmach open Rewrite open Stdarg +open Tactypes open Pcoq.Prim open Pcoq.Constr open Pvernac.Vernac_ @@ -67,13 +67,13 @@ let subst_strategy s str = str let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>" let pr_raw_strategy prc prlc _ (s : raw_strategy) = - let prr = Pptactic.pr_red_expr (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_reference, prc) in + let prr = Pptactic.pr_red_expr (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_qualid, prc) in Rewrite.pr_strategy prc prr s let pr_glob_strategy prc prlc _ (s : glob_strategy) = let prr = Pptactic.pr_red_expr (Ppconstr.pr_constr_expr, Ppconstr.pr_lconstr_expr, - Pputils.pr_or_by_notation Libnames.pr_reference, + Pputils.pr_or_by_notation Libnames.pr_qualid, Ppconstr.pr_constr_expr) in Rewrite.pr_strategy prc prr s diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index dc9f607cf..31bc34a32 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -11,12 +11,14 @@ open Pp open CErrors open Util +open Names +open Namegen open Tacexpr open Genredexpr open Constrexpr open Libnames open Tok -open Misctypes +open Tactypes open Locus open Decl_kinds @@ -154,7 +156,7 @@ let mkTacCase with_evar = function (* Reinterpret ident as notations for variables in the context *) (* because we don't know if they are quantified or not *) | [(clear,ElimOnIdent id),(None,None),None],None -> - TacCase (with_evar,(clear,(CAst.make @@ CRef (CAst.make ?loc:id.CAst.loc @@ Ident id.CAst.v,None),NoBindings))) + TacCase (with_evar,(clear,(CAst.make @@ CRef (qualid_of_ident ?loc:id.CAst.loc id.CAst.v,None),NoBindings))) | ic -> if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic) then @@ -383,19 +385,19 @@ GEXTEND Gram ; hypident: [ [ id = id_or_meta -> - let id : Misctypes.lident = id in + let id : lident = id in id,InHyp | "("; IDENT "type"; IDENT "of"; id = id_or_meta; ")" -> - let id : Misctypes.lident = id in + let id : lident = id in id,InHypTypeOnly | "("; IDENT "value"; IDENT "of"; id = id_or_meta; ")" -> - let id : Misctypes.lident = id in + let id : lident = id in id,InHypValueOnly ] ] ; hypident_occ: [ [ (id,l)=hypident; occs=occs -> - let id : Misctypes.lident = id in + let id : lident = id in ((occs,id),l) ] ] ; in_clause: @@ -494,12 +496,12 @@ GEXTEND Gram | -> None ] ] ; rewriter : - [ [ "!"; c = constr_with_bindings_arg -> (RepeatPlus,c) - | ["?"| LEFTQMARK]; c = constr_with_bindings_arg -> (RepeatStar,c) - | n = natural; "!"; c = constr_with_bindings_arg -> (Precisely n,c) - | n = natural; ["?" | LEFTQMARK]; c = constr_with_bindings_arg -> (UpTo n,c) - | n = natural; c = constr_with_bindings_arg -> (Precisely n,c) - | c = constr_with_bindings_arg -> (Precisely 1, c) + [ [ "!"; c = constr_with_bindings_arg -> (Equality.RepeatPlus,c) + | ["?"| LEFTQMARK]; c = constr_with_bindings_arg -> (Equality.RepeatStar,c) + | n = natural; "!"; c = constr_with_bindings_arg -> (Equality.Precisely n,c) + | n = natural; ["?" | LEFTQMARK]; c = constr_with_bindings_arg -> (Equality.UpTo n,c) + | n = natural; c = constr_with_bindings_arg -> (Equality.Precisely n,c) + | c = constr_with_bindings_arg -> (Equality.Precisely 1, c) ] ] ; oriented_rewriter : diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index 434feba95..c5aa542fd 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -15,22 +15,22 @@ open Libnames open Constrexpr open Tacexpr open Genredexpr -open Misctypes +open Tactypes val open_constr : constr_expr Gram.entry val constr_with_bindings : constr_expr with_bindings Gram.entry val bindings : constr_expr bindings Gram.entry -val hypident : (lident * Locus.hyp_location_flag) Gram.entry -val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry -val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry +val hypident : (Names.lident * Locus.hyp_location_flag) Gram.entry +val constr_may_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Gram.entry +val constr_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Gram.entry val uconstr : constr_expr Gram.entry val quantified_hypothesis : quantified_hypothesis Gram.entry val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Gram.entry -val int_or_var : int or_var Gram.entry +val int_or_var : int Locus.or_var Gram.entry val simple_tactic : raw_tactic_expr Gram.entry val simple_intropattern : constr_expr intro_pattern_expr CAst.t Gram.entry -val in_clause : lident Locus.clause_expr Gram.entry -val clause_dft_concl : lident Locus.clause_expr Gram.entry +val in_clause : Names.lident Locus.clause_expr Gram.entry +val clause_dft_concl : Names.lident Locus.clause_expr Gram.entry val tactic_arg : raw_tactic_arg Gram.entry val tactic_expr : raw_tactic_expr Gram.entry val binder_tactic : raw_tactic_expr Gram.entry diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index b29af6680..09179dad3 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -17,9 +17,8 @@ open Constrexpr open Genarg open Geninterp open Stdarg -open Libnames open Notation_gram -open Misctypes +open Tactypes open Locus open Decl_kinds open Genredexpr @@ -493,7 +492,7 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_orient b = if b then mt () else str "<- " - let pr_multi = function + let pr_multi = let open Equality in function | Precisely 1 -> mt () | Precisely n -> int n ++ str "!" | UpTo n -> int n ++ str "?" @@ -749,7 +748,7 @@ let pr_goal_selector ~toplevel s = | TacIntroPattern (ev,(_::_ as p)) -> hov 1 (primitive (if ev then "eintros" else "intros") ++ (match p with - | [{CAst.v=Misctypes.IntroForthcoming false}] -> mt () + | [{CAst.v=IntroForthcoming false}] -> mt () | _ -> spc () ++ prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)) | TacApply (a,ev,cb,inhyp) -> hov 1 ( @@ -1109,8 +1108,8 @@ let pr_goal_selector ~toplevel s = pr_lconstr = pr_lconstr_expr; pr_pattern = pr_constr_pattern_expr; pr_lpattern = pr_lconstr_pattern_expr; - pr_constant = pr_or_by_notation pr_reference; - pr_reference = pr_reference; + pr_constant = pr_or_by_notation pr_qualid; + pr_reference = pr_qualid; pr_name = pr_lident; pr_generic = (fun arg -> Pputils.pr_raw_generic (Global.env ()) arg); pr_extend = pr_raw_extend_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr; @@ -1323,7 +1322,7 @@ let () = let open Genprint in register_basic_print0 wit_int_or_var (pr_or_var int) (pr_or_var int) int; register_basic_print0 wit_ref - pr_reference (pr_or_var (pr_located pr_global)) pr_global; + pr_qualid (pr_or_var (pr_located pr_global)) pr_global; register_basic_print0 wit_ident pr_id pr_id pr_id; register_basic_print0 wit_var pr_lident pr_lident pr_id; register_print0 @@ -1357,7 +1356,7 @@ let () = ; Genprint.register_print0 wit_red_expr - (lift (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr))) + (lift (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_qualid, pr_constr_pattern_expr))) (lift (pr_red_expr (pr_and_constr_expr pr_glob_constr_pptac, pr_and_constr_expr pr_lglob_constr_pptac, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr_pptac))) pr_red_expr_env ; diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 5d2a99618..6c09e447a 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -14,11 +14,11 @@ open Genarg open Geninterp open Names -open Misctypes open Environ open Constrexpr open Notation_gram open Tacexpr +open Tactypes type 'a grammar_tactic_prod_item_expr = | TacTerm of string @@ -97,7 +97,7 @@ val pr_may_eval : ('a -> Pp.t) -> ('a -> Pp.t) -> ('b -> Pp.t) -> ('c -> Pp.t) -> ('a,'b,'c) Genredexpr.may_eval -> Pp.t -val pr_and_short_name : ('a -> Pp.t) -> 'a and_short_name -> Pp.t +val pr_and_short_name : ('a -> Pp.t) -> 'a Stdarg.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 diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index b91315aca..01c52c413 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -26,7 +26,7 @@ open Classes open Constrexpr open Globnames open Evd -open Misctypes +open Tactypes open Locus open Locusops open Decl_kinds @@ -1773,11 +1773,11 @@ let rec strategy_of_ast = function (* By default the strategy for "rewrite_db" is top-down *) -let mkappc s l = CAst.make @@ CAppExpl ((None,CAst.make @@ Libnames.Ident (Id.of_string s),None),l) +let mkappc s l = CAst.make @@ CAppExpl ((None,qualid_of_ident (Id.of_string s),None),l) let declare_an_instance n s args = (((CAst.make @@ Name n),None), Explicit, - CAst.make @@ CAppExpl ((None, CAst.make @@ Qualid (qualid_of_string s),None), args)) + CAst.make @@ CAppExpl ((None, qualid_of_string s,None), args)) let declare_instance a aeq n s = declare_an_instance n s [a;aeq] @@ -1791,17 +1791,17 @@ let anew_instance global binders instance fields = let declare_instance_refl global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" in anew_instance global binders instance - [(CAst.make @@ Ident (Id.of_string "reflexivity"),lemma)] + [(qualid_of_ident (Id.of_string "reflexivity"),lemma)] let declare_instance_sym global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Symmetric") "Coq.Classes.RelationClasses.Symmetric" in anew_instance global binders instance - [(CAst.make @@ Ident (Id.of_string "symmetry"),lemma)] + [(qualid_of_ident (Id.of_string "symmetry"),lemma)] let declare_instance_trans global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive" in anew_instance global binders instance - [(CAst.make @@ Ident (Id.of_string "transitivity"),lemma)] + [(qualid_of_ident (Id.of_string "transitivity"),lemma)] let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans = init_setoid (); @@ -1825,16 +1825,16 @@ let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in ignore( anew_instance global binders instance - [(CAst.make @@ Ident (Id.of_string "PreOrder_Reflexive"), lemma1); - (CAst.make @@ Ident (Id.of_string "PreOrder_Transitive"),lemma3)]) + [(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1); + (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)]) | (None, Some lemma2, Some lemma3) -> let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in ignore( anew_instance global binders instance - [(CAst.make @@ Ident (Id.of_string "PER_Symmetric"), lemma2); - (CAst.make @@ Ident (Id.of_string "PER_Transitive"),lemma3)]) + [(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2); + (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)]) | (Some lemma1, Some lemma2, Some lemma3) -> let _lemma_refl = declare_instance_refl global binders a aeq n lemma1 in let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in @@ -1842,11 +1842,11 @@ let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in ignore( anew_instance global binders instance - [(CAst.make @@ Ident (Id.of_string "Equivalence_Reflexive"), lemma1); - (CAst.make @@ Ident (Id.of_string "Equivalence_Symmetric"), lemma2); - (CAst.make @@ Ident (Id.of_string "Equivalence_Transitive"), lemma3)]) + [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1); + (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2); + (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)]) -let cHole = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None) +let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) let proper_projection sigma r ty = let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) in @@ -1949,16 +1949,15 @@ let add_setoid global binders a aeq t n = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in ignore( anew_instance global binders instance - [(CAst.make @@ Ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]); - (CAst.make @@ Ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); - (CAst.make @@ Ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]) + [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]); + (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); + (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]) let make_tactic name = let open Tacexpr in - let tacpath = Libnames.qualid_of_string name in - let tacname = CAst.make @@ Qualid tacpath in - TacArg (Loc.tag @@ (TacCall (Loc.tag (tacname, [])))) + let tacqid = Libnames.qualid_of_string name in + TacArg (Loc.tag @@ (TacCall (Loc.tag (tacqid, [])))) let warn_add_morphism_deprecated = CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () -> @@ -2008,7 +2007,7 @@ let add_morphism glob binders m s n = let instance = (((CAst.make @@ Name instance_id),None), Explicit, CAst.make @@ CAppExpl ( - (None, CAst.make @@ Qualid (Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None), + (None, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper",None), [cHole; s; m])) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 1e3d4733b..0d014a0bf 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -12,9 +12,9 @@ open Names open Environ open EConstr open Constrexpr -open Tacexpr -open Misctypes open Evd +open Tactypes +open Tacexpr open Tacinterp (** TODO: document and clean me! *) diff --git a/plugins/ltac/tacarg.ml b/plugins/ltac/tacarg.ml index 6eb482b1c..8a25d4851 100644 --- a/plugins/ltac/tacarg.ml +++ b/plugins/ltac/tacarg.ml @@ -19,6 +19,14 @@ let make0 ?dyn name = let () = Geninterp.register_val0 wit dyn in wit +let wit_intro_pattern = make0 "intropattern" +let wit_quant_hyp = make0 "quant_hyp" +let wit_constr_with_bindings = make0 "constr_with_bindings" +let wit_open_constr_with_bindings = make0 "open_constr_with_bindings" +let wit_bindings = make0 "bindings" +let wit_quantified_hypothesis = wit_quant_hyp +let wit_intropattern = wit_intro_pattern + let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type = make0 "tactic" diff --git a/plugins/ltac/tacarg.mli b/plugins/ltac/tacarg.mli index 59473a5e5..bdb0be03c 100644 --- a/plugins/ltac/tacarg.mli +++ b/plugins/ltac/tacarg.mli @@ -9,9 +9,33 @@ (************************************************************************) open Genarg -open Tacexpr +open EConstr open Constrexpr -open Misctypes +open Tactypes +open Tacexpr + +(** Tactic related witnesses, could also live in tactics/ if other users *) +val wit_intro_pattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type + +val wit_quant_hyp : quantified_hypothesis uniform_genarg_type + +val wit_constr_with_bindings : + (constr_expr with_bindings, + glob_constr_and_expr with_bindings, + constr with_bindings delayed_open) genarg_type + +val wit_open_constr_with_bindings : + (constr_expr with_bindings, + glob_constr_and_expr with_bindings, + constr with_bindings delayed_open) genarg_type + +val wit_bindings : + (constr_expr bindings, + glob_constr_and_expr bindings, + constr bindings delayed_open) genarg_type + +val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type +val wit_intropattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type (** Generic arguments based on Ltac. *) diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 3812a2ba2..cc9c2046d 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -12,9 +12,11 @@ open Util open Names open Constr open EConstr -open Misctypes +open Namegen +open Tactypes open Genarg open Stdarg +open Tacarg open Geninterp open Pp @@ -365,7 +367,7 @@ let coerce_to_int_or_var_list v = match Value.to_list v with | None -> raise (CannotCoerceTo "an int list") | Some l -> - let map n = ArgArg (coerce_to_int n) in + let map n = Locus.ArgArg (coerce_to_int n) in List.map map l (** Abstract application, to print ltac functions *) diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index 5185217cd..56f881684 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -11,9 +11,9 @@ open Util open Names open EConstr -open Misctypes open Genarg open Geninterp +open Tactypes (** Coercions from highest level generic arguments to actual data used by Ltac interpretation. Those functions examinate dynamic types and try to return @@ -56,7 +56,7 @@ val coerce_to_ident_not_fresh : Environ.env -> Evd.evar_map -> Value.t -> Id.t val coerce_to_intro_pattern : Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr val coerce_to_intro_pattern_naming : - Environ.env -> Evd.evar_map -> Value.t -> intro_pattern_naming_expr + Environ.env -> Evd.evar_map -> Value.t -> Namegen.intro_pattern_naming_expr val coerce_to_hint_base : Value.t -> string @@ -86,7 +86,7 @@ val coerce_to_quantified_hypothesis : Evd.evar_map -> Value.t -> quantified_hypo val coerce_to_decl_or_quant_hyp : Environ.env -> Evd.evar_map -> Value.t -> quantified_hypothesis -val coerce_to_int_or_var_list : Value.t -> int or_var list +val coerce_to_int_or_var_list : Value.t -> int Locus.or_var list (** {5 Missing generic arguments} *) diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index e510b9f59..98d451536 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -376,7 +376,7 @@ let add_ml_tactic_notation name ~level prods = in let ids = List.map_filter get_id prods in let entry = { mltac_name = name; mltac_index = len - i - 1 } in - let map id = Reference (Misctypes.ArgVar (CAst.make id)) in + let map id = Reference (Locus.ArgVar (CAst.make id)) in let tac = TacML (Loc.tag (entry, List.map map ids)) in add_glob_tactic_notation false ~level prods true ids tac in @@ -449,12 +449,12 @@ let register_ltac local tacl = in let () = if is_shadowed then warn_unusable_identifier id in NewTac id, body - | Tacexpr.TacticRedefinition (ident, body) -> + | Tacexpr.TacticRedefinition (qid, body) -> let kn = - try Tacenv.locate_tactic (qualid_of_reference ident).CAst.v + try Tacenv.locate_tactic qid with Not_found -> - CErrors.user_err ?loc:ident.CAst.loc - (str "There is no Ltac named " ++ pr_reference ident ++ str ".") + CErrors.user_err ?loc:qid.CAst.loc + (str "There is no Ltac named " ++ pr_qualid qid ++ str ".") in UpdateTac kn, body in diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 3f804ee8d..2bfbbe2e1 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -65,7 +65,7 @@ val create_ltac_quotation : string -> val print_ltacs : unit -> unit (** Display the list of ltac definitions currently available. *) -val print_located_tactic : Libnames.reference -> unit +val print_located_tactic : Libnames.qualid -> unit (** Display the absolute name of a tactic. *) type _ ty_sig = diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 17f5e5d41..06d2711ad 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -15,7 +15,7 @@ open Libnames open Genredexpr open Genarg open Pattern -open Misctypes +open Tactypes open Locus type ltac_constant = KerName.t @@ -75,7 +75,7 @@ type 'id message_token = type ('dconstr,'id) induction_clause = 'dconstr with_bindings Tactics.destruction_arg * - (intro_pattern_naming_expr CAst.t option (* eqn:... *) + (Namegen.intro_pattern_naming_expr CAst.t option (* eqn:... *) * 'dconstr or_and_intro_pattern_expr CAst.t or_var option) (* as ... *) * 'id clause_expr option (* in ... *) @@ -117,7 +117,7 @@ type ml_tactic_entry = { (** Composite types *) -type glob_constr_and_expr = Tactypes.glob_constr_and_expr +type glob_constr_and_expr = Genintern.glob_constr_and_expr type open_constr_expr = unit * constr_expr type open_glob_constr = unit * glob_constr_and_expr @@ -134,7 +134,7 @@ type delayed_open_constr = EConstr.constr delayed_open type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t -type intro_pattern_naming = intro_pattern_naming_expr CAst.t +type intro_pattern_naming = Namegen.intro_pattern_naming_expr CAst.t (** Generic expressions for atomic tactics *) @@ -152,7 +152,7 @@ type 'a gen_atomic_tactic_expr = 'dtrm intro_pattern_expr CAst.t option * 'trm | TacGeneralize of ('trm with_occurrences * Name.t) list | TacLetTac of evars_flag * Name.t * 'trm * 'nam clause_expr * letin_flag * - intro_pattern_naming_expr CAst.t option + Namegen.intro_pattern_naming_expr CAst.t option (* Derived basic tactics *) | TacInductionDestruct of @@ -164,7 +164,7 @@ type 'a gen_atomic_tactic_expr = (* Equality and inversion *) | TacRewrite of evars_flag * - (bool * multi * 'dtrm with_bindings_arg) list * 'nam clause_expr * + (bool * Equality.multi * 'dtrm with_bindings_arg) list * 'nam clause_expr * (* spiwack: using ['dtrm] here is a small hack, may not be stable by a change in the representation of delayed terms. Because, in fact, it is the whole "with_bindings" @@ -305,7 +305,7 @@ constraint 'a = < type g_trm = glob_constr_and_expr type g_pat = glob_constr_pattern_and_expr -type g_cst = evaluable_global_reference and_short_name or_var +type g_cst = evaluable_global_reference Stdarg.and_short_name or_var type g_ref = ltac_constant located or_var type g_nam = lident @@ -333,8 +333,8 @@ type glob_tactic_arg = type r_trm = constr_expr type r_pat = constr_pattern_expr -type r_cst = reference or_by_notation -type r_ref = reference +type r_cst = qualid or_by_notation +type r_ref = qualid type r_nam = lident type r_lev = rlevel @@ -399,4 +399,4 @@ type ltac_trace = ltac_call_kind Loc.located list type tacdef_body = | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) - | TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) + | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 17f5e5d41..71e1edfd7 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -15,8 +15,8 @@ open Libnames open Genredexpr open Genarg open Pattern -open Misctypes open Locus +open Tactypes type ltac_constant = KerName.t @@ -75,7 +75,7 @@ type 'id message_token = type ('dconstr,'id) induction_clause = 'dconstr with_bindings Tactics.destruction_arg * - (intro_pattern_naming_expr CAst.t option (* eqn:... *) + (Namegen.intro_pattern_naming_expr CAst.t option (* eqn:... *) * 'dconstr or_and_intro_pattern_expr CAst.t or_var option) (* as ... *) * 'id clause_expr option (* in ... *) @@ -117,7 +117,7 @@ type ml_tactic_entry = { (** Composite types *) -type glob_constr_and_expr = Tactypes.glob_constr_and_expr +type glob_constr_and_expr = Genintern.glob_constr_and_expr type open_constr_expr = unit * constr_expr type open_glob_constr = unit * glob_constr_and_expr @@ -134,7 +134,7 @@ type delayed_open_constr = EConstr.constr delayed_open type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t -type intro_pattern_naming = intro_pattern_naming_expr CAst.t +type intro_pattern_naming = Namegen.intro_pattern_naming_expr CAst.t (** Generic expressions for atomic tactics *) @@ -152,7 +152,7 @@ type 'a gen_atomic_tactic_expr = 'dtrm intro_pattern_expr CAst.t option * 'trm | TacGeneralize of ('trm with_occurrences * Name.t) list | TacLetTac of evars_flag * Name.t * 'trm * 'nam clause_expr * letin_flag * - intro_pattern_naming_expr CAst.t option + Namegen.intro_pattern_naming_expr CAst.t option (* Derived basic tactics *) | TacInductionDestruct of @@ -164,7 +164,7 @@ type 'a gen_atomic_tactic_expr = (* Equality and inversion *) | TacRewrite of evars_flag * - (bool * multi * 'dtrm with_bindings_arg) list * 'nam clause_expr * + (bool * Equality.multi * 'dtrm with_bindings_arg) list * 'nam clause_expr * (* spiwack: using ['dtrm] here is a small hack, may not be stable by a change in the representation of delayed terms. Because, in fact, it is the whole "with_bindings" @@ -305,7 +305,7 @@ constraint 'a = < type g_trm = glob_constr_and_expr type g_pat = glob_constr_pattern_and_expr -type g_cst = evaluable_global_reference and_short_name or_var +type g_cst = evaluable_global_reference Stdarg.and_short_name or_var type g_ref = ltac_constant located or_var type g_nam = lident @@ -333,8 +333,8 @@ type glob_tactic_arg = type r_trm = constr_expr type r_pat = constr_pattern_expr -type r_cst = reference or_by_notation -type r_ref = reference +type r_cst = qualid or_by_notation +type r_ref = qualid type r_nam = lident type r_lev = rlevel @@ -399,4 +399,4 @@ type ltac_trace = ltac_call_kind Loc.located list type tacdef_body = | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) - | TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) + | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 9ad9e1520..481fc30df 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -27,7 +27,8 @@ open Tacexpr open Genarg open Stdarg open Tacarg -open Misctypes +open Namegen +open Tactypes open Locus (** Globalization of tactic expressions : @@ -91,88 +92,83 @@ let intern_or_var f ist = function let intern_int_or_var = intern_or_var (fun (n : int) -> n) let intern_string_or_var = intern_or_var (fun (s : string) -> s) -let intern_global_reference ist = function - | {CAst.loc;v=Ident id} when find_var id ist -> - ArgVar (make ?loc id) - | r -> - let {CAst.loc} as lqid = qualid_of_reference r in - try ArgArg (loc,locate_global_with_alias lqid) - with Not_found -> error_global_not_found lqid - -let intern_ltac_variable ist = function - | {loc;v=Ident id} -> - if find_var id ist then - (* A local variable of any type *) - ArgVar (make ?loc id) - else raise Not_found - | _ -> - raise Not_found - -let intern_constr_reference strict ist = function - | {v=Ident id} as r when not strict && find_hyp id ist -> - (DAst.make @@ GVar id), Some (make @@ CRef (r,None)) - | {v=Ident id} as r when find_var id ist -> - (DAst.make @@ GVar id), if strict then None else Some (make @@ CRef (r,None)) - | r -> - let {loc} as lqid = qualid_of_reference r in - DAst.make @@ GRef (locate_global_with_alias lqid,None), - if strict then None else Some (make @@ CRef (r,None)) +let intern_global_reference ist qid = + if qualid_is_ident qid && find_var (qualid_basename qid) ist then + ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid) + else + try ArgArg (qid.CAst.loc,locate_global_with_alias qid) + with Not_found -> error_global_not_found qid + +let intern_ltac_variable ist qid = + if qualid_is_ident qid && find_var (qualid_basename qid) ist then + (* A local variable of any type *) + ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid) + else raise Not_found + +let intern_constr_reference strict ist qid = + let id = qualid_basename qid in + if qualid_is_ident qid && not strict && find_hyp (qualid_basename qid) ist then + (DAst.make @@ GVar id), Some (make @@ CRef (qid,None)) + else if qualid_is_ident qid && find_var (qualid_basename qid) ist then + (DAst.make @@ GVar id), if strict then None else Some (make @@ CRef (qid,None)) + else + DAst.make @@ GRef (locate_global_with_alias qid,None), + if strict then None else Some (make @@ CRef (qid,None)) (* Internalize an isolated reference in position of tactic *) -let intern_isolated_global_tactic_reference r = - let {loc;v=qid} = qualid_of_reference r in +let intern_isolated_global_tactic_reference qid = + let loc = qid.CAst.loc in TacCall (Loc.tag ?loc (ArgArg (loc,Tacenv.locate_tactic qid),[])) -let intern_isolated_tactic_reference strict ist r = +let intern_isolated_tactic_reference strict ist qid = (* An ltac reference *) - try Reference (intern_ltac_variable ist r) + try Reference (intern_ltac_variable ist qid) with Not_found -> (* A global tactic *) - try intern_isolated_global_tactic_reference r + try intern_isolated_global_tactic_reference qid with Not_found -> (* Tolerance for compatibility, allow not to use "constr:" *) - try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r)) + try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist qid)) with Not_found -> (* Reference not found *) - error_global_not_found (qualid_of_reference r) + error_global_not_found qid (* Internalize an applied tactic reference *) -let intern_applied_global_tactic_reference r = - let {loc;v=qid} = qualid_of_reference r in - ArgArg (loc,Tacenv.locate_tactic qid) +let intern_applied_global_tactic_reference qid = + ArgArg (qid.CAst.loc,Tacenv.locate_tactic qid) -let intern_applied_tactic_reference ist r = +let intern_applied_tactic_reference ist qid = (* An ltac reference *) - try intern_ltac_variable ist r + try intern_ltac_variable ist qid with Not_found -> (* A global tactic *) - try intern_applied_global_tactic_reference r + try intern_applied_global_tactic_reference qid with Not_found -> (* Reference not found *) - error_global_not_found (qualid_of_reference r) + error_global_not_found qid (* Intern a reference parsed in a non-tactic entry *) -let intern_non_tactic_reference strict ist r = +let intern_non_tactic_reference strict ist qid = (* An ltac reference *) - try Reference (intern_ltac_variable ist r) + try Reference (intern_ltac_variable ist qid) with Not_found -> (* A constr reference *) - try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r)) + try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist qid)) with Not_found -> (* Tolerance for compatibility, allow not to use "ltac:" *) - try intern_isolated_global_tactic_reference r + try intern_isolated_global_tactic_reference qid with Not_found -> (* By convention, use IntroIdentifier for unbound ident, when not in a def *) - match r with - | {loc;v=Ident id} when not strict -> - let ipat = in_gen (glbwit wit_intro_pattern) (make ?loc @@ IntroNaming (IntroIdentifier id)) in + if qualid_is_ident qid && not strict then + let id = qualid_basename qid in + let ipat = in_gen (glbwit wit_intro_pattern) (make ?loc:qid.CAst.loc @@ IntroNaming (IntroIdentifier id)) in TacGeneric ipat - | _ -> - (* Reference not found *) - error_global_not_found (qualid_of_reference r) + else + (* Reference not found *) + error_global_not_found qid let intern_message_token ist = function | (MsgString _ | MsgInt _ as x) -> x @@ -268,7 +264,7 @@ let intern_destruction_arg ist = function | clear,ElimOnIdent {loc;v=id} -> if !strict_check then (* If in a defined tactic, no intros-until *) - let c, p = intern_constr ist (make @@ CRef (make @@ Ident id, None)) in + let c, p = intern_constr ist (make @@ CRef (qualid_of_ident id, None)) in match DAst.get c with | GVar id -> clear,ElimOnIdent (make ?loc:c.loc id) | _ -> clear,ElimOnConstr ((c, p), NoBindings) @@ -276,16 +272,15 @@ let intern_destruction_arg ist = function clear,ElimOnIdent (make ?loc id) let short_name = function - | {v=AN {loc;v=Ident id}} when not !strict_check -> Some (make ?loc id) + | {v=AN qid} when qualid_is_ident qid && not !strict_check -> + Some (make ?loc:qid.CAst.loc @@ qualid_basename qid) | _ -> None -let intern_evaluable_global_reference ist r = - let lqid = qualid_of_reference r in - try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true lqid) +let intern_evaluable_global_reference ist qid = + try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true qid) with Not_found -> - match r with - | {loc;v=Ident id} when not !strict_check -> EvalVarRef id - | _ -> error_global_not_found lqid + if qualid_is_ident qid && not !strict_check then EvalVarRef (qualid_basename qid) + else error_global_not_found qid let intern_evaluable_reference_or_by_notation ist = function | {v=AN r} -> intern_evaluable_global_reference ist r @@ -295,14 +290,19 @@ let intern_evaluable_reference_or_by_notation ist = function (function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc) (* Globalize a reduction expression *) -let intern_evaluable ist = function - | {loc;v=AN {v=Ident id}} when find_var id ist -> ArgVar (make ?loc id) - | {loc;v=AN {v=Ident id}} when not !strict_check && find_hyp id ist -> - ArgArg (EvalVarRef id, Some (make ?loc id)) - | r -> - let e = intern_evaluable_reference_or_by_notation ist r in - let na = short_name r in - ArgArg (e,na) +let intern_evaluable ist r = + let f ist r = + let e = intern_evaluable_reference_or_by_notation ist r in + let na = short_name r in + ArgArg (e,na) + in + match r with + | {v=AN qid} when qualid_is_ident qid && find_var (qualid_basename qid) ist -> + ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid) + | {v=AN qid} when qualid_is_ident qid && not !strict_check && find_hyp (qualid_basename qid) ist -> + let id = qualid_basename qid in + ArgArg (EvalVarRef id, Some (make ?loc:qid.CAst.loc id)) + | _ -> f ist r let intern_unfold ist (l,qid) = (l,intern_evaluable ist qid) @@ -355,7 +355,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = subterm matched when a pattern *) let r = match r with | {v=AN r} -> r - | {loc} -> make ?loc @@ Qualid (qualid_of_path (path_of_global (smart_global r))) in + | {loc} -> (qualid_of_path ?loc (path_of_global (smart_global r))) in let sign = { Constrintern.ltac_vars = ist.ltacvars; ltac_bound = Id.Set.empty; diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index fb32508cc..9146fced2 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -12,7 +12,7 @@ open Names open Tacexpr open Genarg open Constrexpr -open Misctypes +open Tactypes (** Globalization of tactic expressions : Conversion from [raw_tactic_expr] to [glob_tactic_expr] *) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index a93cf5ae7..9d1cc1643 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -12,6 +12,7 @@ open Constrintern open Patternops open Pp open CAst +open Namegen open Genredexpr open Glob_term open Glob_ops @@ -35,7 +36,7 @@ open Stdarg open Tacarg open Printer open Pretyping -open Misctypes +open Tactypes open Locus open Tacintern open Taccoerce @@ -360,7 +361,7 @@ let interp_reference ist env sigma = function with Not_found -> try VarRef (get_id (Environ.lookup_named id env)) - with Not_found -> error_global_not_found (make ?loc @@ qualid_of_ident id) + with Not_found -> error_global_not_found (qualid_of_ident ?loc id) let try_interp_evaluable env (loc, id) = let v = Environ.lookup_named id env in @@ -376,14 +377,14 @@ let interp_evaluable ist env sigma = function with Not_found -> match r with | EvalConstRef _ -> r - | _ -> error_global_not_found (make ?loc @@ qualid_of_ident id) + | _ -> error_global_not_found (qualid_of_ident ?loc id) end | ArgArg (r,None) -> r | ArgVar {loc;v=id} -> try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> try try_interp_evaluable env (loc, id) - with Not_found -> error_global_not_found (make ?loc @@ qualid_of_ident id) + with Not_found -> error_global_not_found (qualid_of_ident ?loc id) (* Interprets an hypothesis name *) let interp_occurrences ist occs = @@ -642,7 +643,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (make ?loc id) with Not_found -> - error_global_not_found (make ?loc @@ qualid_of_ident id)) + error_global_not_found (qualid_of_ident ?loc id)) | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b) | Inr c -> Inr (interp_typed_pattern ist env sigma c) in interp_occurrences ist occs, p @@ -924,7 +925,7 @@ let interp_destruction_arg ist gl arg = if Tactics.is_quantified_hypothesis id gl then keep,ElimOnIdent (make ?loc id) else - let c = (DAst.make ?loc @@ GVar id,Some (make @@ CRef (make ?loc @@ Ident id,None))) in + let c = (DAst.make ?loc @@ GVar id,Some (make @@ CRef (qualid_of_ident ?loc id,None))) in let f env sigma = let (sigma,c) = interp_open_constr ist env sigma c in (sigma, (c,NoBindings)) @@ -1048,8 +1049,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with push_trace(loc,call) ist >>= fun trace -> Profile_ltac.do_profile "eval_tactic:2" trace (catch_error_tac trace (interp_atomic ist t)) - | TacFun _ | TacLetIn _ -> assert false - | TacMatchGoal _ | TacMatch _ -> assert false + | TacFun _ | TacLetIn _ | TacMatchGoal _ | TacMatch _ -> interp_tactic ist tac | TacId [] -> Proofview.tclLIFT (db_breakpoint (curr_debug ist) []) | TacId s -> let msgnl = diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index bd44bdbea..fd2d96bd6 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -14,7 +14,7 @@ open EConstr open Tacexpr open Genarg open Redexpr -open Misctypes +open Tactypes val ltac_trace_info : ltac_trace Exninfo.t @@ -131,7 +131,7 @@ val interp_ltac_var : (value -> 'a) -> interp_sign -> val interp_int : interp_sign -> lident -> int -val interp_int_or_var : interp_sign -> int or_var -> int +val interp_int_or_var : interp_sign -> int Locus.or_var -> int val default_ist : unit -> Geninterp.interp_sign (** Empty ist with debug set on the current value. *) diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 50bf687b1..dd799dc13 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -14,7 +14,7 @@ open Mod_subst open Genarg open Stdarg open Tacarg -open Misctypes +open Tactypes open Globnames open Genredexpr open Patternops @@ -75,7 +75,7 @@ let subst_and_short_name f (c,n) = (* assert (n=None); *)(* since tacdef are strictly globalized *) (f c,None) -let subst_or_var f = function +let subst_or_var f = let open Locus in function | ArgVar _ as x -> x | ArgArg x -> ArgArg (f x) diff --git a/plugins/ltac/tacsubst.mli b/plugins/ltac/tacsubst.mli index 0a894791b..d406686c5 100644 --- a/plugins/ltac/tacsubst.mli +++ b/plugins/ltac/tacsubst.mli @@ -11,7 +11,7 @@ open Tacexpr open Mod_subst open Genarg -open Misctypes +open Tactypes (** Substitution of tactics at module closing time *) diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli index 734e76b56..175341df0 100644 --- a/plugins/ltac/tactic_debug.mli +++ b/plugins/ltac/tactic_debug.mli @@ -76,7 +76,7 @@ val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t (** Prints a logic failure message for a rule *) val db_breakpoint : debug_info -> - Misctypes.lident message_token list -> unit Proofview.NonLogical.t + lident message_token list -> unit Proofview.NonLogical.t val extract_ltac_trace : ?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.t option Loc.located diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 8eeb8903e..299bc7ea4 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -13,7 +13,6 @@ open EConstr open Hipattern open Names open Geninterp -open Misctypes open Ltac_plugin open Tacexpr open Tacinterp @@ -94,7 +93,7 @@ let clear id = Tactics.clear [id] let assumption = Tactics.assumption -let split = Tactics.split_with_bindings false [Misctypes.NoBindings] +let split = Tactics.split_with_bindings false [Tactypes.NoBindings] (** Test *) @@ -175,7 +174,7 @@ let flatten_contravariant_disj _ ist = | Some (_,args) -> let map i arg = let typ = mkArrow arg c in - let ci = Tactics.constructor_tac false None (succ i) Misctypes.NoBindings in + let ci = Tactics.constructor_tac false None (succ i) Tactypes.NoBindings in let by = tclTHENLIST [intro; apply hyp; ci; assumption] in assert_ ~by typ in @@ -187,7 +186,7 @@ let flatten_contravariant_disj _ ist = let make_unfold name = let dir = DirPath.make (List.map Id.of_string ["Logic"; "Init"; "Coq"]) in let const = Constant.make2 (ModPath.MPfile dir) (Label.make name) in - (Locus.AllOccurrences, ArgArg (EvalConstRef const, None)) + Locus.(AllOccurrences, ArgArg (EvalConstRef const, None)) let u_not = make_unfold "not" @@ -245,7 +244,7 @@ let with_flags flags _ ist = let x = CAst.make @@ Id.of_string "x" in let arg = Val.Dyn (tag_tauto_flags, flags) in let ist = { ist with lfun = Id.Map.add x.CAst.v arg ist.lfun } in - eval_tactic_ist ist (TacArg (Loc.tag @@ TacCall (Loc.tag (ArgVar f, [Reference (ArgVar x)])))) + eval_tactic_ist ist (TacArg (Loc.tag @@ TacCall (Loc.tag (Locus.ArgVar f, [Reference (Locus.ArgVar x)])))) let register_tauto_tactic tac name0 args = let ids = List.map (fun id -> Id.of_string id) args in diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 68620dbfc..f22147f8b 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -23,6 +23,7 @@ open Names open Goptions open Mutils open Constr +open Tactypes (** * Debug flag @@ -1727,7 +1728,7 @@ let micromega_gen let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in - let ipat_of_name id = Some (CAst.make @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in + let ipat_of_name id = Some (CAst.make @@ IntroNaming (Namegen.IntroIdentifier id)) in let goal_name = fresh_id Id.Set.empty (Names.Id.of_string "__arith") gl in let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in @@ -1842,7 +1843,7 @@ let micromega_genr prover tac = let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in - let ipat_of_name id = Some (CAst.make @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in + let ipat_of_name id = Some (CAst.make @@ IntroNaming (Namegen.IntroIdentifier id)) in let goal_name = fresh_id Id.Set.empty (Names.Id.of_string "__arith") gl in let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index c615cf278..6f4138828 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -29,7 +29,7 @@ open Libnames open Globnames open Nametab open Contradiction -open Misctypes +open Tactypes open Context.Named.Declaration module NamedDecl = Context.Named.Declaration diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index c35e0fe12..09209dc22 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -10,7 +10,6 @@ open Ltac_plugin open Names -open Misctypes open Tacexpr open Geninterp open Quote @@ -24,7 +23,7 @@ let x = Id.of_string "x" let make_cont (k : Val.t) (c : EConstr.t) = let c = Tacinterp.Value.of_constr c in - let tac = TacCall (Loc.tag (ArgVar CAst.(make cont), [Reference (ArgVar CAst.(make x))])) in + let tac = TacCall (Loc.tag (Locus.ArgVar CAst.(make cont), [Reference (Locus.ArgVar CAst.(make x))])) in let ist = { lfun = Id.Map.add cont k (Id.Map.singleton x c); extra = TacStore.empty; } in Tacinterp.eval_tactic_ist ist (TacArg (Loc.tag tac)) diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index 5e4c9214a..e9ce306e8 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -42,11 +42,11 @@ let pr_ring_mod = function | Ring_kind Abstract -> str "abstract" | Ring_kind (Morphism morph) -> str "morphism" ++ pr_arg pr_constr_expr morph | Const_tac (CstTac cst_tac) -> str "constants" ++ spc () ++ str "[" ++ pr_raw_tactic cst_tac ++ str "]" - | Const_tac (Closed l) -> str "closed" ++ spc () ++ str "[" ++ prlist_with_sep spc pr_reference l ++ str "]" + | Const_tac (Closed l) -> str "closed" ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]" | Pre_tac t -> str "preprocess" ++ spc () ++ str "[" ++ pr_raw_tactic t ++ str "]" | Post_tac t -> str "postprocess" ++ spc () ++ str "[" ++ pr_raw_tactic t ++ str "]" | Setoid(sth,ext) -> str "setoid" ++ pr_arg pr_constr_expr sth ++ pr_arg pr_constr_expr ext - | Pow_spec(Closed l,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ prlist_with_sep spc pr_reference l ++ str "]" + | Pow_spec(Closed l,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]" | Pow_spec(CstTac cst_tac,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ pr_raw_tactic cst_tac ++ str "]" | Sign_spec t -> str "sign" ++ pr_arg pr_constr_expr t | Div_spec t -> str "div" ++ pr_arg pr_constr_expr t diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index b9d0d2e25..84b29a0bf 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -20,6 +20,7 @@ open Environ open Libnames open Globnames open Glob_term +open Locus open Tacexpr open Coqlib open Mod_subst @@ -29,7 +30,6 @@ open Printer open Declare open Decl_kinds open Entries -open Misctypes open Newring_ast open Proofview.Notations diff --git a/plugins/setoid_ring/newring_ast.ml b/plugins/setoid_ring/newring_ast.ml index 3eb68b518..a83c79d11 100644 --- a/plugins/setoid_ring/newring_ast.ml +++ b/plugins/setoid_ring/newring_ast.ml @@ -22,7 +22,7 @@ type 'constr coeff_spec = type cst_tac_spec = CstTac of raw_tactic_expr - | Closed of reference list + | Closed of qualid list type 'constr ring_mod = Ring_kind of 'constr coeff_spec diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli index 3eb68b518..a83c79d11 100644 --- a/plugins/setoid_ring/newring_ast.mli +++ b/plugins/setoid_ring/newring_ast.mli @@ -22,7 +22,7 @@ type 'constr coeff_spec = type cst_tac_spec = CstTac of raw_tactic_expr - | Closed of reference list + | Closed of qualid list type 'constr ring_mod = Ring_kind of 'constr coeff_spec diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index 7f5f2f63d..5571c5420 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -37,7 +37,7 @@ type ssrmult = int * ssrmmod type ssrocc = (bool * int list) option (* index MAYBE REMOVE ONLY INTERNAL stuff between {} *) -type ssrindex = int Misctypes.or_var +type ssrindex = int Locus.or_var (* clear switch {H G} *) type ssrclear = ssrhyps diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 3f6503e73..54f3f9c71 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -181,10 +181,9 @@ let option_assert_get o msg = (** Constructors for rawconstr *) open Glob_term open Globnames -open Misctypes open Decl_kinds -let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None) +let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) let rec mkRHoles n = if n > 0 then mkRHole :: mkRHoles (n - 1) else [] let rec isRHoles cl = match cl with @@ -254,7 +253,7 @@ let interp_refine ist gl rc = let interp_open_constr ist gl gc = - let (sigma, (c, _)) = Tacinterp.interp_open_constr_with_bindings ist (pf_env gl) (project gl) (gc, Misctypes.NoBindings) in + let (sigma, (c, _)) = Tacinterp.interp_open_constr_with_bindings ist (pf_env gl) (project gl) (gc, Tactypes.NoBindings) in (project gl, (sigma, c)) let interp_term ist gl (_, c) = snd (interp_open_constr ist gl c) @@ -859,10 +858,10 @@ open Util (** Constructors for constr_expr *) let mkCProp loc = CAst.make ?loc @@ CSort GProp let mkCType loc = CAst.make ?loc @@ CSort (GType []) -let mkCVar ?loc id = CAst.make ?loc @@ CRef (CAst.make ?loc @@ Ident id, None) +let mkCVar ?loc id = CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None) let rec mkCHoles ?loc n = - if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) :: mkCHoles ?loc (n - 1) -let mkCHole loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None) + if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None)) :: mkCHoles ?loc (n - 1) +let mkCHole loc = CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None) let mkCLambda ?loc name ty t = CAst.make ?loc @@ CLambdaN ([CLocalAssum([CAst.make ?loc name], Default Explicit, ty)], t) let mkCArrow ?loc ty t = CAst.make ?loc @@ diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 83b4d6562..fbe3b000f 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -17,7 +17,7 @@ open Term open Constr open Termops open Globnames -open Misctypes +open Tactypes open Tacmach open Ssrmatching_plugin diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index c6beb08c5..2c046190f 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -86,7 +86,6 @@ let _ = open Constrexpr open Glob_term -open Misctypes let combineCG t1 t2 f g = match t1, t2 with | (x, (t1, None)), (_, (t2, None)) -> x, (g t1 t2, None) diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index fbfbdb110..7a1d06fdc 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -22,13 +22,15 @@ open Libnames open Tactics open Tacmach open Util +open Locus open Tacexpr open Tacinterp open Pltac open Extraargs open Ppconstr -open Misctypes +open Namegen +open Tactypes open Decl_kinds open Constrexpr open Constrexpr_ops @@ -301,24 +303,24 @@ END let pr_index = function - | Misctypes.ArgVar {CAst.v=id} -> pr_id id - | Misctypes.ArgArg n when n > 0 -> int n + | ArgVar {CAst.v=id} -> pr_id id + | ArgArg n when n > 0 -> int n | _ -> mt () let pr_ssrindex _ _ _ = pr_index -let noindex = Misctypes.ArgArg 0 +let noindex = ArgArg 0 let check_index ?loc i = if i > 0 then i else CErrors.user_err ?loc (str"Index not positive") let mk_index ?loc = function - | Misctypes.ArgArg i -> Misctypes.ArgArg (check_index ?loc i) + | ArgArg i -> ArgArg (check_index ?loc i) | iv -> iv let interp_index ist gl idx = Tacmach.project gl, match idx with - | Misctypes.ArgArg _ -> idx - | Misctypes.ArgVar id -> + | ArgArg _ -> idx + | ArgVar id -> let i = try let v = Id.Map.find id.CAst.v ist.Tacinterp.lfun in @@ -336,7 +338,7 @@ let interp_index ist gl idx = | None -> raise Not_found end end with _ -> CErrors.user_err ?loc:id.CAst.loc (str"Index not a number") in - Misctypes.ArgArg (check_index ?loc:id.CAst.loc i) + ArgArg (check_index ?loc:id.CAst.loc i) open Pltac @@ -543,7 +545,7 @@ END let remove_loc x = x.CAst.v -let ipat_of_intro_pattern p = Misctypes.( +let ipat_of_intro_pattern p = Tactypes.( let rec ipat_of_intro_pattern = function | IntroNaming (IntroIdentifier id) -> IPatId id | IntroAction IntroWildcard -> IPatAnon Drop @@ -595,16 +597,15 @@ let intern_ipats ist = List.map (intern_ipat ist) let interp_intro_pattern = interp_wit wit_intro_pattern -let interp_introid ist gl id = Misctypes.( +let interp_introid ist gl id = try IntroNaming (IntroIdentifier (hyp_id (snd (interp_hyp ist gl (SsrHyp (Loc.tag id)))))) with _ -> (snd (interp_intro_pattern ist gl (CAst.make @@ IntroNaming (IntroIdentifier id)))).CAst.v -) let get_intro_id = function | IntroNaming (IntroIdentifier id) -> id | _ -> assert false -let rec add_intro_pattern_hyps ipat hyps = Misctypes.( +let rec add_intro_pattern_hyps ipat hyps = let {CAst.loc=loc;v=ipat} = ipat in match ipat with | IntroNaming (IntroIdentifier id) -> @@ -623,7 +624,6 @@ let rec add_intro_pattern_hyps ipat hyps = Misctypes.( | IntroForthcoming _ -> (* As in ipat_of_intro_pattern, was unable to determine which kind of ipat interp_introid could return [HH] *) assert false -) (* We interp the ipat using the standard ltac machinery for ids, since * we have no clue what a name could be bound to (maybe another ipat) *) @@ -1064,7 +1064,7 @@ let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with | BFdef :: h, { v = CLetIn({CAst.v=x}, v, oty, c) } -> let bs, c' = format_constr_expr h c in Bdef (x, oty, v) :: bs, c' - | [BFcast], { v = CCast (c, CastConv t) } -> + | [BFcast], { v = CCast (c, Glob_term.CastConv t) } -> [Bcast t], c | BFrec (has_str, has_cast) :: h, { v = CFix ( _, [_, (Some locn, CStructRec), bl, t, c]) } -> @@ -1093,7 +1093,7 @@ let wit_ssrfwdfmt = add_genarg "ssrfwdfmt" pr_fwdfmt let mkFwdVal fk c = ((fk, []), c) let mkssrFwdVal fk c = ((fk, []), (c,None)) -let dC t = CastConv t +let dC t = Glob_term.CastConv t let same_ist { interp_env = x } { interp_env = y } = match x,y with @@ -1154,7 +1154,8 @@ ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY pr_ssrbvar END let bvar_lname = let open CAst in function - | { v = CRef ({loc;v=Ident id}, _) } -> CAst.make ?loc @@ Name id + | { v = CRef (qid, _) } when qualid_is_ident qid -> + CAst.make ?loc:qid.CAst.loc @@ Name (qualid_basename qid) | { loc = loc } -> CAst.make ?loc Anonymous let pr_ssrbinder prc _ _ (_, c) = prc c @@ -1210,8 +1211,8 @@ let push_binders c2 bs = | [] -> c | _ -> anomaly "binder not a lambda nor a let in" in match c2 with - | { loc; v = CCast (ct, CastConv cty) } -> - CAst.make ?loc @@ (CCast (loop false ct bs, CastConv (loop true cty bs))) + | { loc; v = CCast (ct, Glob_term.CastConv cty) } -> + CAst.make ?loc @@ (CCast (loop false ct bs, Glob_term.CastConv (loop true cty bs))) | ct -> loop false ct bs let rec fix_binders = let open CAst in function @@ -1246,7 +1247,8 @@ END let pr_ssrfixfwd _ _ _ (id, fwd) = str " fix " ++ pr_id id ++ pr_fwd fwd let bvar_locid = function - | { CAst.v = CRef ({CAst.loc=loc;v=Ident id}, _) } -> CAst.make ?loc id + | { CAst.v = CRef (qid, _) } when qualid_is_ident qid -> + CAst.make ?loc:qid.CAst.loc (qualid_basename qid) | _ -> CErrors.user_err (Pp.str "Missing identifier after \"(co)fix\"") diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index 372ae86bd..83581f341 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -14,7 +14,6 @@ open Names open Constr open Termops open Tacmach -open Misctypes open Locusops open Ssrast @@ -25,7 +24,7 @@ module NamedDecl = Context.Named.Declaration (** Tacticals (+, -, *, done, by, do, =>, first, and last). *) -let get_index = function ArgArg i -> i | _ -> +let get_index = function Locus.ArgArg i -> i | _ -> anomaly "Uninterpreted index" (* Toplevel constr must be globalized twice ! *) diff --git a/plugins/ssr/ssrtacticals.mli b/plugins/ssr/ssrtacticals.mli index a5636ad0f..684e00235 100644 --- a/plugins/ssr/ssrtacticals.mli +++ b/plugins/ssr/ssrtacticals.mli @@ -17,7 +17,7 @@ val tclSEQAT : Tacinterp.interp_sign -> Tacinterp.Value.t -> Ssrast.ssrdir -> - int Misctypes.or_var * + int Locus.or_var * (('a * Tacinterp.Value.t option list) * Tacinterp.Value.t option) -> Tacmach.tactic @@ -37,7 +37,7 @@ val hinttac : val ssrdotac : Tacinterp.interp_sign -> - ((int Misctypes.or_var * Ssrast.ssrmmod) * + ((int Locus.or_var * Ssrast.ssrmmod) * (bool * Tacinterp.Value.t option list)) * ((Ssrast.ssrhyps * ((Ssrast.ssrhyp_or_id * string) * diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 750461a1b..7ce2dd64a 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -27,9 +27,7 @@ open Glob_term open Globnames open Stdarg open Genarg -open Misctypes open Decl_kinds -open Libnames open Pp open Ppconstr open Printer @@ -144,21 +142,21 @@ END let declare_one_prenex_implicit locality f = let fref = try Smartlocate.global_with_alias f - with _ -> errorstrm (pr_reference f ++ str " is not declared") in + with _ -> errorstrm (pr_qualid f ++ str " is not declared") in let rec loop = function | a :: args' when Impargs.is_status_implicit a -> (ExplByName (Impargs.name_of_implicit a), (true, true, true)) :: loop args' | args' when List.exists Impargs.is_status_implicit args' -> - errorstrm (str "Expected prenex implicits for " ++ pr_reference f) + errorstrm (str "Expected prenex implicits for " ++ pr_qualid f) | _ -> [] in let impls = match Impargs.implicits_of_global fref with | [cond,impls] -> impls - | [] -> errorstrm (str "Expected some implicits for " ++ pr_reference f) + | [] -> errorstrm (str "Expected some implicits for " ++ pr_qualid f) | _ -> errorstrm (str "Multiple implicits not supported") in match loop impls with | [] -> - errorstrm (str "Expected some implicits for " ++ pr_reference f) + errorstrm (str "Expected some implicits for " ++ pr_qualid f) | impls -> Impargs.declare_manual_implicits locality fref ~enriching:false [impls] @@ -416,7 +414,7 @@ let interp_search_arg arg = (* Module path postfilter *) -let pr_modloc (b, m) = if b then str "-" ++ pr_reference m else pr_reference m +let pr_modloc (b, m) = if b then str "-" ++ pr_qualid m else pr_qualid m let wit_ssrmodloc = add_genarg "ssrmodloc" pr_modloc @@ -434,10 +432,9 @@ GEXTEND Gram END let interp_modloc mr = - let interp_mod (_, mr) = - let {CAst.loc=loc; v=qid} = qualid_of_reference mr in + let interp_mod (_, qid) = try Nametab.full_name_module qid with Not_found -> - CErrors.user_err ?loc (str "No Module " ++ pr_qualid qid) in + CErrors.user_err ?loc:qid.CAst.loc (str "No Module " ++ pr_qualid qid) in let mr_out, mr_in = List.partition fst mr in let interp_bmod b = function | [] -> fun _ _ _ -> true diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 29a936381..faebe3179 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -157,7 +157,7 @@ let tclINJ_CONSTR_IST ist p = let mkGHole = DAst.make - (Glob_term.GHole(Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None)) + (Glob_term.GHole(Evar_kinds.InternalHole, Namegen.IntroAnonymous, None)) let rec mkGHoles n = if n > 0 then mkGHole :: mkGHoles (n - 1) else [] let mkGApp f args = if args = [] then f diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index b1c5e131f..c20e415b4 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -40,7 +40,7 @@ open Pretyping open Ppconstr open Printer open Globnames -open Misctypes +open Namegen open Decl_kinds open Evar_kinds open Constrexpr @@ -131,9 +131,12 @@ let add_genarg tag pr = (** Constructors for cast type *) let dC t = CastConv t (** Constructors for constr_expr *) -let isCVar = function { CAst.v = CRef ({CAst.v=Ident _},_) } -> true | _ -> false -let destCVar = function { CAst.v = CRef ({CAst.v=Ident id},_) } -> id | _ -> - CErrors.anomaly (str"not a CRef.") +let isCVar = function { CAst.v = CRef (qid,_) } -> qualid_is_ident qid | _ -> false +let destCVar = function + | { CAst.v = CRef (qid,_) } when qualid_is_ident qid -> + qualid_basename qid + | _ -> + CErrors.anomaly (str"not a CRef.") let isGLambda c = match DAst.get c with GLambda (Name _, _, _, _) -> true | _ -> false let destGLambda c = match DAst.get c with GLambda (Name id, _, _, c) -> (id, c) | _ -> CErrors.anomaly (str "not a GLambda") @@ -1019,8 +1022,10 @@ type pattern = Evd.evar_map * (constr, constr) ssrpattern let id_of_cpattern (_, (c1, c2), _) = let open CAst in match DAst.get c1, c2 with - | _, Some { v = CRef ({CAst.v=Ident x}, _) } -> Some x - | _, Some { v = CAppExpl ((_, {CAst.v=Ident x}, _), []) } -> Some x + | _, Some { v = CRef (qid, _) } when qualid_is_ident qid -> + Some (qualid_basename qid) + | _, Some { v = CAppExpl ((_, qid, _), []) } when qualid_is_ident qid -> + Some (qualid_basename qid) | GRef (VarRef x, _), None -> Some x | _ -> None let id_of_Cterm t = match id_of_cpattern t with |