diff options
Diffstat (limited to 'plugins/ltac')
31 files changed, 213 insertions, 232 deletions
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 931633e1a..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" @@ -273,15 +275,13 @@ END (* Fix *) TACTIC EXTEND fix - [ "fix" natural(n) ] -> [ Tactics.fix None n ] -| [ "fix" ident(id) natural(n) ] -> [ Tactics.fix (Some id) n ] + [ "fix" ident(id) natural(n) ] -> [ Tactics.fix id n ] END (* Cofix *) TACTIC EXTEND cofix - [ "cofix" ] -> [ Tactics.cofix None ] -| [ "cofix" ident(id) ] -> [ Tactics.cofix (Some id) ] + [ "cofix" ident(id) ] -> [ Tactics.cofix id ] END (* Clear *) diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index 9382f567b..84f13d213 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -10,7 +10,7 @@ open Util open Names -open Term +open Constr open CErrors open Evar_refiner open Tacmach @@ -52,7 +52,7 @@ let instantiate_tac n c ido = match ido with ConclLocation () -> evar_list sigma (pf_concl gl) | HypLocation (id,hloc) -> - let decl = Environ.lookup_named_val id (Goal.V82.hyps sigma (sig_it gl)) in + let decl = Environ.lookup_named id (pf_env gl) in match hloc with InHyp -> (match decl with @@ -85,16 +85,14 @@ let let_evar name typ = Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in - let sigma = ref sigma in - let _ = Typing.e_sort_of env sigma typ in - let sigma = !sigma in + let sigma, _ = Typing.sort_of env sigma typ in let id = match name with | Name.Anonymous -> let id = Namegen.id_of_name_using_hdchar env sigma typ name in 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 702b83034..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 @@ -251,7 +250,7 @@ END let pr_by_arg_tac _prc _prlc prtac opt_c = match opt_c with | None -> mt () - | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_term.E) t) + | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_gram.E) t) ARGUMENT EXTEND by_arg_tac TYPED AS tactic_opt diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index e5a4f090e..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 @@ -66,7 +65,7 @@ val wit_by_arg_tac : Geninterp.Val.t option) Genarg.genarg_type val pr_by_arg_tac : - (int * Notation_term.parenRelation -> raw_tactic_expr -> Pp.t) -> + (int * Notation_gram.parenRelation -> raw_tactic_expr -> Pp.t) -> raw_tactic_expr option -> Pp.t val test_lpar_id_colon : unit Pcoq.Gram.entry diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 2e90ce90c..f2899ab63 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -9,6 +9,7 @@ (************************************************************************) open Pp +open Constr open Genarg open Stdarg open Tacarg @@ -23,7 +24,8 @@ open CErrors open Util open Termops open Equality -open Misctypes +open Namegen +open Tactypes open Proofview.Notations open Vernacinterp @@ -284,80 +286,6 @@ VERNAC COMMAND FUNCTIONAL EXTEND HintRewrite CLASSIFIED BY classify_hint END (**********************************************************************) -(* Hint Resolve *) - -open Term -open EConstr -open Vars -open Coqlib - -let project_hint ~poly pri l2r r = - let gr = Smartlocate.global_with_alias r in - let env = Global.env() in - let sigma = Evd.from_env env in - let sigma, c = Evd.fresh_global env sigma gr in - let c = EConstr.of_constr c in - let t = Retyping.get_type_of env sigma c in - let t = - Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) t in - let sign,ccl = decompose_prod_assum sigma t in - let (a,b) = match snd (decompose_app sigma ccl) with - | [a;b] -> (a,b) - | _ -> assert false in - let p = - if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in - let sigma, p = Evd.fresh_global env sigma p in - let p = EConstr.of_constr p in - let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in - let c = it_mkLambda_or_LetIn - (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in - let id = - Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l")) - in - let ctx = Evd.const_univ_entry ~poly sigma in - let c = EConstr.to_constr sigma c in - let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in - let info = {Vernacexpr.hint_priority = pri; hint_pattern = None} in - (info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c)) - -let add_hints_iff ~atts l2r lc n bl = - let open Vernacinterp in - Hints.add_hints (Locality.make_module_locality atts.locality) bl - (Hints.HintsResolveEntry (List.map (project_hint ~poly:atts.polymorphic n l2r) lc)) - -VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF - [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) - ":" preident_list(bl) ] -> - [ fun ~atts ~st -> begin - add_hints_iff ~atts true lc n bl; - st - end - ] -| [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ] -> - [ fun ~atts ~st -> begin - add_hints_iff ~atts true lc n ["core"]; - st - end - ] -END - -VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffRL CLASSIFIED AS SIDEFF - [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) - ":" preident_list(bl) ] -> - [ fun ~atts ~st -> begin - add_hints_iff ~atts false lc n bl; - st - end - ] -| [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) ] -> - [ fun ~atts ~st -> begin - add_hints_iff ~atts false lc n ["core"]; - st - end - ] -END - -(**********************************************************************) (* Refine *) open EConstr @@ -596,10 +524,16 @@ let inImplicitTactic : glob_tactic_expr option -> obj = subst_function = subst_implicit_tactic; classify_function = (fun o -> Dispose)} +let warn_deprecated_implicit_tactic = + CWarnings.create ~name:"deprecated-implicit-tactic" ~category:"deprecated" + (fun () -> strbrk "Implicit tactics are deprecated") + let declare_implicit_tactic tac = + let () = warn_deprecated_implicit_tactic () in Lib.add_anonymous_leaf (inImplicitTactic (Some (Tacintern.glob_tactic tac))) let clear_implicit_tactic () = + let () = warn_deprecated_implicit_tactic () in Lib.add_anonymous_leaf (inImplicitTactic None) VERNAC COMMAND EXTEND ImplicitTactic CLASSIFIED AS SIDEFF @@ -615,10 +549,12 @@ END VERNAC COMMAND EXTEND RetroknowledgeRegister CLASSIFIED AS SIDEFF | [ "Register" constr(c) "as" retroknowledge_field(f) "by" constr(b)] -> - [ let tc,_ctx = Constrintern.interp_constr (Global.env ()) Evd.empty c in - let tb,_ctx(*FIXME*) = Constrintern.interp_constr (Global.env ()) Evd.empty b in - let tc = EConstr.to_constr Evd.empty tc in - let tb = EConstr.to_constr Evd.empty tb in + [ let env = Global.env () in + let evd = Evd.from_env env in + let tc,_ctx = Constrintern.interp_constr env evd c in + let tb,_ctx(*FIXME*) = Constrintern.interp_constr env evd b in + let tc = EConstr.to_constr evd tc in + let tb = EConstr.to_constr evd tb in Global.register f tc tb ] END @@ -669,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 @@ -680,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 @@ -781,7 +717,7 @@ let mkCaseEq a : unit Proofview.tactic = let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in (** FIXME: this looks really wrong. Does anybody really use this tactic? *) - let (_, c) = Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env Evd.empty concl in + let (_, c) = Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env (Evd.from_env env) concl in change_concl c end; simplest_case a] @@ -1108,7 +1044,9 @@ END VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF | [ "Declare" "Equivalent" "Keys" constr(c) constr(c') ] -> [ let get_key c = - let (evd, c) = Constrintern.interp_open_constr (Global.env ()) Evd.empty c in + let env = Global.env () in + let evd = Evd.from_env env in + let (evd, c) = Constrintern.interp_open_constr env evd c in let kind c = EConstr.kind evd c in Keys.constr_key kind c in diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 643f7e99f..642e52155 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -9,6 +9,7 @@ (************************************************************************) open Pp +open Constr open Genarg open Stdarg open Pcoq.Prim @@ -169,7 +170,7 @@ END TACTIC EXTEND convert_concl_no_check -| ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x Term.DEFAULTcast ] +| ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x DEFAULTcast ] END let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_reference @@ -219,7 +220,7 @@ VERNAC COMMAND FUNCTIONAL EXTEND HintCut CLASSIFIED AS SIDEFF fun ~atts ~st -> begin let open Vernacinterp in let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in - Hints.add_hints (Locality.make_section_locality atts.locality) + Hints.add_hints ~local:(Locality.make_section_locality atts.locality) (match dbnames with None -> ["core"] | Some l -> l) entry; st end diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 0c42a8bb2..d7d642e50 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -12,21 +12,22 @@ 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 *) open Names open Pcoq -open Pcoq.Constr -open Pcoq.Vernac_ open Pcoq.Prim +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,7 +35,7 @@ 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 @@ -58,8 +59,8 @@ let tacdef_body = new_entry "tactic:tacdef_body" let _ = let mode = { Proof_global.name = "Classic"; - set = (fun () -> set_command_entry tactic_mode); - reset = (fun () -> set_command_entry Pcoq.Vernac_.noedit_mode); + set = (fun () -> Pvernac.set_command_entry tactic_mode); + reset = (fun () -> Pvernac.(set_command_entry noedit_mode)); } in Proof_global.register_proof_mode mode @@ -197,9 +198,9 @@ 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)*) + [ [ s = STRING -> Locus.ArgArg s (*| id = ident -> Locus.ArgVar (!@loc,id)*) | qid = qualid -> let (_pth,id) = Libnames.repr_qualid qid.CAst.v in - ArgVar (CAst.make ~loc:!@loc id) ] ] + Locus.ArgVar (CAst.make ~loc:!@loc id) ] ] ; constr_eval: [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> @@ -325,6 +326,7 @@ GEXTEND Gram ; toplevel_selector: [ [ sel = selector_body; ":" -> sel + | "!"; ":" -> SelectAlreadyFocused | IDENT "all"; ":" -> SelectAll ] ] ; tactic_mode: @@ -415,7 +417,7 @@ let is_explicit_terminator = function TacSolve _ -> true | _ -> false VERNAC tactic_mode EXTEND VernacSolve | [ - ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => [ classify_as_proofstep ] -> [ - let g = Option.default (Proof_bullet.get_default_goal_selector ()) g in + let g = Option.default (Goal_select.get_default_goal_selector ()) g in vernac_solve g n t def ] | [ - "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index fbaa2e58f..2189e224f 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,9 +19,10 @@ open Extraargs open Tacmach open Rewrite open Stdarg -open Pcoq.Vernac_ +open Tactypes open Pcoq.Prim open Pcoq.Constr +open Pvernac.Vernac_ open Pltac DECLARE PLUGIN "ltac_plugin" diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 7534e2799..05005c733 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 @@ -211,7 +213,7 @@ let warn_deprecated_eqn_syntax = (* Auxiliary grammar rules *) -open Vernac_ +open Pvernac.Vernac_ GEXTEND Gram GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis @@ -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 6637de745..4c075d413 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 hypident : (Names.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 uconstr : constr_expr Gram.entry val quantified_hypothesis : quantified_hypothesis Gram.entry -val destruction_arg : constr_expr with_bindings destruction_arg Gram.entry -val int_or_var : int or_var Gram.entry +val destruction_arg : constr_expr with_bindings Tactics.destruction_arg 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 11bb7a234..e19a95e84 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -18,8 +18,8 @@ open Genarg open Geninterp open Stdarg open Libnames -open Notation_term -open Misctypes +open Notation_gram +open Tactypes open Locus open Decl_kinds open Genredexpr @@ -149,9 +149,12 @@ let string_of_genarg_arg (ArgumentType arg) = let open Genprint in match generic_top_print (in_gen (Topwit wit) x) with | TopPrinterBasic pr -> pr () - | TopPrinterNeedsContext pr -> pr (Global.env()) Evd.empty + | TopPrinterNeedsContext pr -> + let env = Global.env() in + pr env (Evd.from_env env) | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> - printer (Global.env()) Evd.empty default_ensure_surrounded + let env = Global.env() in + printer env (Evd.from_env env) default_ensure_surrounded end | _ -> default @@ -490,7 +493,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 "?" @@ -515,6 +518,7 @@ let string_of_genarg_arg (ArgumentType arg) = else int i ++ str "-" ++ int j let pr_goal_selector toplevel = function + | SelectAlreadyFocused -> str "!:" | SelectNth i -> int i ++ str ":" | SelectList l -> prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ str ":" | SelectId id -> str "[" ++ Id.print id ++ str "]:" @@ -745,7 +749,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 ( diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 5951f2b11..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_term +open Notation_gram open Tacexpr +open Tactypes type 'a grammar_tactic_prod_item_expr = | TacTerm of string @@ -84,7 +84,7 @@ type pp_tactic = { pptac_prods : grammar_terminals; } -val pr_goal_selector : toplevel:bool -> goal_selector -> Pp.t +val pr_goal_selector : toplevel:bool -> Goal_select.t -> Pp.t val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit @@ -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 @@ -153,5 +153,5 @@ 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) -> +val make_constr_printer : (env -> Evd.evar_map -> tolerability -> 'a -> Pp.t) -> 'a Genprint.top_printer diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index d32a2faef..cd04f4ae9 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 @@ -104,9 +104,8 @@ let extends_undefined evars evars' = let app_poly_check env evars f args = let (evars, cstrs), fc = f evars in - let evdref = ref evars in - let t = Typing.e_solve_evars env evdref (mkApp (fc, args)) in - (!evdref, cstrs), t + let evars, t = Typing.solve_evars env evars (mkApp (fc, args)) in + (evars, cstrs), t let app_poly_nocheck env evars f args = let evars, fc = f evars in @@ -428,7 +427,8 @@ 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' && Constr.equal x x' && Constr.equal y y') + let equal x y = Constr.equal (EConstr.Unsafe.to_constr x) (EConstr.Unsafe.to_constr y) in + pb == pb' || (ty == ty' && equal x x' && equal y y') let problem_inclusion x y = List.for_all (fun pb -> List.exists (fun pb' -> eq_pb pb pb') y) x @@ -626,9 +626,9 @@ let solve_remaining_by env sigma holes by = (** Evar should not be defined, but just in case *) | Some evi -> let env = Environ.reset_with_named_context evi.evar_hyps env in - let ty = EConstr.of_constr evi.evar_concl in + let ty = evi.evar_concl in let c, sigma = Pfedit.refine_by_tactic env sigma ty solve_tac in - Evd.define evk c sigma + Evd.define evk (EConstr.of_constr c) sigma in List.fold_left solve sigma indep @@ -1468,8 +1468,8 @@ exception RewriteFailure of Pp.t type result = (evar_map * constr option * types) option option let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : result = + let sigma, sort = Typing.sort_of env sigma concl in let evdref = ref sigma in - let sort = Typing.e_sort_of env evdref concl in let evars = (!evdref, Evar.Set.empty) in let evars, cstr = let prop, (evars, arrow) = @@ -1846,7 +1846,7 @@ let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans = (CAst.make @@ Ident (Id.of_string "Equivalence_Symmetric"), lemma2); (CAst.make @@ 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 @@ -1862,7 +1862,6 @@ let declare_projection n instance_id r = let env = Global.env () in let sigma = Evd.from_env env in let sigma,c = Evd.fresh_global env sigma r in - let c = EConstr.of_constr c in let ty = Retyping.get_type_of env sigma c in let term = proper_projection sigma c ty in let sigma, typ = Typing.type_of env sigma term in @@ -1923,7 +1922,7 @@ let build_morphism_signature env sigma m = let evd = solve_constraints env !evd in let evd = Evd.minimize_universes evd in let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in - Pretyping.check_evars env Evd.empty evd (EConstr.of_constr m); + Pretyping.check_evars env (Evd.from_env env) evd (EConstr.of_constr m); Evd.evar_universe_context evd, m let default_morphism sign m = 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 5347eda7d..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. *) @@ -23,7 +47,7 @@ val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Geninterp.Val.t) genarg_typ val wit_ltac : (raw_tactic_expr, glob_tactic_expr, unit) genarg_type val wit_destruction_arg : - (constr_expr with_bindings Tacexpr.destruction_arg, - glob_constr_and_expr with_bindings Tacexpr.destruction_arg, - delayed_open_constr_with_bindings Tacexpr.destruction_arg) genarg_type + (constr_expr with_bindings Tactics.destruction_arg, + glob_constr_and_expr with_bindings Tactics.destruction_arg, + delayed_open_constr_with_bindings Tactics.destruction_arg) genarg_type 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 1fa5e3c07..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 @@ -80,13 +80,13 @@ val coerce_to_hyp : Environ.env -> Evd.evar_map -> Value.t -> Id.t val coerce_to_hyp_list : Environ.env -> Evd.evar_map -> Value.t -> Id.t list -val coerce_to_reference : Environ.env -> Evd.evar_map -> Value.t -> Globnames.global_reference +val coerce_to_reference : Environ.env -> Evd.evar_map -> Value.t -> GlobRef.t val coerce_to_quantified_hypothesis : Evd.evar_map -> Value.t -> quantified_hypothesis 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..fada7424c 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 diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 8b0c44041..d51de8c65 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 @@ -35,30 +35,35 @@ type advanced_flag = bool (* true = advanced false = basic *) type letin_flag = bool (* true = use local def false = use Leibniz *) type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) -type goal_selector = Vernacexpr.goal_selector = +type goal_selector = Goal_select.t = + | SelectAlreadyFocused | SelectNth of int | SelectList of (int * int) list | SelectId of Id.t | SelectAll +[@@ocaml.deprecated "Use Vernacexpr.goal_selector"] -type 'a core_destruction_arg = 'a Misctypes.core_destruction_arg = +type 'a core_destruction_arg = 'a Tactics.core_destruction_arg = | ElimOnConstr of 'a | ElimOnIdent of lident | ElimOnAnonHyp of int +[@@ocaml.deprecated "Use Tactics.core_destruction_arg"] type 'a destruction_arg = - clear_flag * 'a core_destruction_arg + clear_flag * 'a Tactics.core_destruction_arg +[@@ocaml.deprecated "Use Tactics.destruction_arg"] -type inversion_kind = Misctypes.inversion_kind = +type inversion_kind = Inv.inversion_kind = | SimpleInversion | FullInversion | FullInversionClear +[@@ocaml.deprecated "Use Tactics.inversion_kind"] type ('c,'d,'id) inversion_strength = | NonDepInversion of - inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option + Inv.inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option | DepInversion of - inversion_kind * 'c option * 'd or_and_intro_pattern_expr CAst.t or_var option + Inv.inversion_kind * 'c option * 'd or_and_intro_pattern_expr CAst.t or_var option | InversionUsing of 'c * 'id list type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b @@ -69,8 +74,8 @@ type 'id message_token = | MsgIdent of 'id type ('dconstr,'id) induction_clause = - 'dconstr with_bindings destruction_arg * - (intro_pattern_naming_expr CAst.t option (* eqn:... *) + 'dconstr with_bindings Tactics.destruction_arg * + (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 ... *) @@ -112,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 @@ -129,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 *) @@ -147,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 @@ -159,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" @@ -265,7 +270,7 @@ and 'a gen_tactic_expr = ('p,'a gen_tactic_expr) match_rule list | TacFun of 'a gen_tactic_fun_ast | TacArg of 'a gen_tactic_arg located - | TacSelect of goal_selector * 'a gen_tactic_expr + | TacSelect of Goal_select.t * 'a gen_tactic_expr (* For ML extensions *) | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located (* For syntax extensions *) @@ -300,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 diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 8b0c44041..01eead164 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 @@ -35,30 +35,35 @@ type advanced_flag = bool (* true = advanced false = basic *) type letin_flag = bool (* true = use local def false = use Leibniz *) type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) -type goal_selector = Vernacexpr.goal_selector = +type goal_selector = Goal_select.t = + | SelectAlreadyFocused | SelectNth of int | SelectList of (int * int) list | SelectId of Id.t | SelectAll +[@@ocaml.deprecated "Use Vernacexpr.goal_selector"] -type 'a core_destruction_arg = 'a Misctypes.core_destruction_arg = +type 'a core_destruction_arg = 'a Tactics.core_destruction_arg = | ElimOnConstr of 'a | ElimOnIdent of lident | ElimOnAnonHyp of int +[@@ocaml.deprecated "Use Tactics.core_destruction_arg"] type 'a destruction_arg = - clear_flag * 'a core_destruction_arg + clear_flag * 'a Tactics.core_destruction_arg +[@@ocaml.deprecated "Use Tactics.destruction_arg"] -type inversion_kind = Misctypes.inversion_kind = +type inversion_kind = Inv.inversion_kind = | SimpleInversion | FullInversion | FullInversionClear +[@@ocaml.deprecated "Use Tactics.inversion_kind"] type ('c,'d,'id) inversion_strength = | NonDepInversion of - inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option + Inv.inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option | DepInversion of - inversion_kind * 'c option * 'd or_and_intro_pattern_expr CAst.t or_var option + Inv.inversion_kind * 'c option * 'd or_and_intro_pattern_expr CAst.t or_var option | InversionUsing of 'c * 'id list type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b @@ -69,8 +74,8 @@ type 'id message_token = | MsgIdent of 'id type ('dconstr,'id) induction_clause = - 'dconstr with_bindings destruction_arg * - (intro_pattern_naming_expr CAst.t option (* eqn:... *) + 'dconstr with_bindings Tactics.destruction_arg * + (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 ... *) @@ -112,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 @@ -129,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 *) @@ -147,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 @@ -159,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" @@ -265,7 +270,7 @@ and 'a gen_tactic_expr = ('p,'a gen_tactic_expr) match_rule list | TacFun of 'a gen_tactic_fun_ast | TacArg of 'a gen_tactic_arg located - | TacSelect of goal_selector * 'a gen_tactic_expr + | TacSelect of Goal_select.t * 'a gen_tactic_expr (* For ML extensions *) | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located (* For syntax extensions *) @@ -300,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 diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 9ad9e1520..cef5bb1b8 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 : 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 6a4bf577b..8a8f9e71a 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 @@ -691,11 +692,9 @@ let interp_may_eval f ist env sigma = function let (sigma,ic) = f ist env sigma c in let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in let ctxt = EConstr.Unsafe.to_constr ctxt in - let evdref = ref sigma in - let ic = EConstr.Unsafe.to_constr ic in + let ic = EConstr.Unsafe.to_constr ic in let c = subst_meta [Constr_matching.special_meta,ic] ctxt in - let c = Typing.e_solve_evars env evdref (EConstr.of_constr c) in - !evdref , c + Typing.solve_evars env sigma (EConstr.of_constr c) with | Not_found -> user_err ?loc ~hdr:"interp_may_eval" @@ -2010,7 +2009,8 @@ let interp_redexp env sigma r = let _ = let eval lfun env sigma ty tac = - let ist = { lfun = lfun; extra = TacStore.empty; } in + let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in + let ist = { lfun = lfun; extra; } in let tac = interp_tactic ist tac in let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in (EConstr.of_constr c, sigma) 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 a1d8b087e..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) @@ -112,7 +112,7 @@ let subst_glob_constr_or_pattern subst (bvars,c,p) = (bvars,subst_glob_constr subst c,subst_pattern subst p) let subst_redexp subst = - Miscops.map_red_expr_gen + Redops.map_red_expr_gen (subst_glob_constr subst) (subst_evaluable subst) (subst_glob_constr_or_pattern subst) 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.ml b/plugins/ltac/tactic_debug.ml index e55b49fb4..105b5c59a 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -391,19 +391,14 @@ let explain_ltac_call_trace last trace loc = let skip_extensions trace = let rec aux = function - | (_,Tacexpr.LtacNameCall f as tac) :: _ - when Tacenv.is_ltac_for_ml_tactic f -> [tac] - | (_,Tacexpr.LtacNotationCall _ as tac) :: (_,Tacexpr.LtacMLCall _) :: _ -> + | (_,Tacexpr.LtacNotationCall _ as tac) :: (_,Tacexpr.LtacMLCall _) :: tail -> (* Case of an ML defined tactic with entry of the form <<"foo" args>> *) (* see tacextend.mlp *) - [tac] - | (_,Tacexpr.LtacMLCall _ as tac) :: _ -> [tac] + tac :: aux tail | t :: tail -> t :: aux tail | [] -> [] in List.rev (aux (List.rev trace)) -let finer_loc loc1 loc2 = Loc.merge_opt loc1 loc2 = loc2 - let extract_ltac_trace ?loc trace = let trace = skip_extensions trace in let (tloc,c),tail = List.sep_last trace in @@ -411,7 +406,7 @@ let extract_ltac_trace ?loc trace = (* We entered a user-defined tactic, we display the trace with location of the call *) let msg = hov 0 (explain_ltac_call_trace c tail loc ++ fnl()) in - (if finer_loc loc tloc then loc else tloc), Some msg + (if Loc.finer loc tloc then loc else tloc), Some msg else (* We entered a primitive tactic, we don't display trace but report on the finest location *) @@ -420,7 +415,7 @@ let extract_ltac_trace ?loc trace = let rec aux best_loc = function | (loc,_)::tail -> if Option.is_empty best_loc || - not (Option.is_empty loc) && finer_loc loc best_loc + not (Option.is_empty loc) && Loc.finer loc best_loc then aux loc tail else 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/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index b6462c810..c949589e2 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -46,7 +46,7 @@ let adjust : Constr_matching.bound_ident_map * Ltac_pretype.patvar_map -> (** Adds a binding to a {!Id.Map.t} if the identifier is [Some id] *) let id_map_try_add id x m = match id with - | Some id -> Id.Map.add id x m + | Some id -> Id.Map.add id (Lazy.force x) m | None -> m (** Adds a binding to a {!Id.Map.t} if the name is [Name id] *) diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index a51c09ca4..299bc7ea4 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -8,12 +8,11 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Term +open Constr 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 |