diff options
Diffstat (limited to 'plugins/ltac')
47 files changed, 272 insertions, 301 deletions
diff --git a/plugins/ltac/Ltac.v b/plugins/ltac/Ltac.v deleted file mode 100644 index e69de29bb2..0000000000 --- a/plugins/ltac/Ltac.v +++ /dev/null diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg index 2159c05f80..48b6abf441 100644 --- a/plugins/ltac/coretactics.mlg +++ b/plugins/ltac/coretactics.mlg @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index c87eb7c3c9..17a7121a3f 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -26,9 +26,9 @@ module NamedDecl = Context.Named.Declaration (* The instantiate tactic *) -let instantiate_evar evk (ist,rawc) sigma = +let instantiate_evar evk (ist,rawc) env sigma = let evi = Evd.find sigma evk in - let filtered = Evd.evar_filtered_env evi in + let filtered = Evd.evar_filtered_env env evi in let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in let lvar = { ltac_constrs = constrvars; @@ -36,7 +36,7 @@ let instantiate_evar evk (ist,rawc) sigma = ltac_idents = Names.Id.Map.empty; ltac_genargs = ist.Geninterp.lfun; } in - let sigma' = w_refine (evk,evi) (lvar ,rawc) sigma in + let sigma' = w_refine (evk,evi) (lvar ,rawc) env sigma in tclEVARS sigma' let evar_list sigma c = @@ -48,6 +48,7 @@ let evar_list sigma c = let instantiate_tac n c ido = Proofview.V82.tactic begin fun gl -> + let env = Global.env () in let sigma = gl.sigma in let evl = match ido with @@ -69,16 +70,17 @@ let instantiate_tac n c ido = user_err Pp.(str "Not enough uninstantiated existential variables."); if n <= 0 then user_err Pp.(str "Incorrect existential variable index."); let evk,_ = List.nth evl (n-1) in - instantiate_evar evk c sigma gl + instantiate_evar evk c env sigma gl end let instantiate_tac_by_name id c = Proofview.V82.tactic begin fun gl -> + let env = Global.env () in let sigma = gl.sigma in let evk = try Evd.evar_key id sigma with Not_found -> user_err Pp.(str "Unknown existential variable.") in - instantiate_evar evk c sigma gl + instantiate_evar evk c env sigma gl end let let_evar name typ = diff --git a/plugins/ltac/evar_tactics.mli b/plugins/ltac/evar_tactics.mli index d99c800320..dd7aef71c6 100644 --- a/plugins/ltac/evar_tactics.mli +++ b/plugins/ltac/evar_tactics.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index bab6bfd78e..c4731e5c34 100644 --- a/plugins/ltac/extraargs.mlg +++ b/plugins/ltac/extraargs.mlg @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -298,7 +298,7 @@ END let pr_by_arg_tac env sigma _prc _prlc prtac opt_c = match opt_c with | None -> mt () - | Some t -> hov 2 (str "by" ++ spc () ++ prtac env sigma (3,Notation_gram.E) t) + | Some t -> hov 2 (str "by" ++ spc () ++ prtac env sigma (Constrexpr.LevelLe 3) t) } @@ -330,18 +330,10 @@ END { let local_test_lpar_id_colon = - let err () = raise Stream.Failure in - Pcoq.Entry.of_parser "lpar_id_colon" - (fun _ strm -> - match Util.stream_nth 0 strm with - | Tok.KEYWORD "(" -> - (match Util.stream_nth 1 strm with - | Tok.IDENT _ -> - (match Util.stream_nth 2 strm with - | Tok.KEYWORD ":" -> () - | _ -> err ()) - | _ -> err ()) - | _ -> err ()) + let open Pcoq.Lookahead in + to_entry "lpar_id_colon" begin + lk_kw "(" >> lk_ident >> lk_kw ":" + end let pr_lpar_id_colon _ _ _ _ = mt () diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index 6dd51e4e01..fbdb7c0032 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -67,7 +67,7 @@ val wit_by_arg_tac : val pr_by_arg_tac : Environ.env -> Evd.evar_map -> - (Environ.env -> Evd.evar_map -> int * Notation_gram.parenRelation -> raw_tactic_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> raw_tactic_expr -> Pp.t) -> raw_tactic_expr option -> Pp.t val test_lpar_id_colon : unit Pcoq.Entry.t diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 6c63a891e8..9b80cbd803 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -670,7 +670,7 @@ let hResolve id c occ t = Pretyping.understand env sigma t_hole with | Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) as e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in let loc_begin = Option.cata (fun l -> fst (Loc.unloc l)) 0 (Loc.get_loc info) in resolve_hole (subst_hole_with_term loc_begin c_raw t_hole) in @@ -736,7 +736,7 @@ let refl_equal () = Coqlib.lib_ref "core.eq.type" call it before it is defined. *) let mkCaseEq a : unit Proofview.tactic = Proofview.Goal.enter begin fun gl -> - let type_of_a = Tacmach.New.pf_unsafe_type_of gl a in + let type_of_a = Tacmach.New.pf_get_type_of gl a in Tacticals.New.pf_constr_of_global (delayed_force refl_equal) >>= fun req -> Tacticals.New.tclTHENLIST [Tactics.generalize [(mkApp(req, [| type_of_a; a|]))]; @@ -794,7 +794,7 @@ let destauto t = let destauto_in id = Proofview.Goal.enter begin fun gl -> - let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in + let ctype = Tacmach.New.pf_get_type_of gl (mkVar id) in (* Pp.msgnl (Printer.pr_lconstr (mkVar id)); *) (* Pp.msgnl (Printer.pr_lconstr (ctype)); *) destauto ctype diff --git a/plugins/ltac/extratactics.mli b/plugins/ltac/extratactics.mli index e47226410a..ac9fd198de 100644 --- a/plugins/ltac/extratactics.mli +++ b/plugins/ltac/extratactics.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index 8344f9dae3..3c30c881fb 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -114,7 +114,7 @@ END (** Eauto *) -TACTIC EXTEND prolog +TACTIC EXTEND prolog DEPRECATED { Deprecation.make ~note:"Use eauto instead" () } | [ "prolog" "[" uconstr_list(l) "]" int_or_var(n) ] -> { Eauto.prolog_tac (eval_uconstrs ist l) n } END @@ -249,8 +249,8 @@ END VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF | #[ locality = Attributes.locality; ] [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> { let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in - Hints.add_hints ~local:(Locality.make_section_locality locality) + let locality = if Locality.make_section_locality locality then Goptions.OptLocal else Goptions.OptGlobal in + Hints.add_hints ~locality (match dbnames with None -> ["core"] | Some l -> l) entry; } END - diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg index 0aaf417f33..0f0341f123 100644 --- a/plugins/ltac/g_class.mlg +++ b/plugins/ltac/g_class.mlg @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ltac/g_eqdecide.mlg b/plugins/ltac/g_eqdecide.mlg index d416f08c06..4b4a0e5f3e 100644 --- a/plugins/ltac/g_eqdecide.mlg +++ b/plugins/ltac/g_eqdecide.mlg @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 81a6651745..50c3ed1248 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -20,7 +20,6 @@ open Tacexpr open Namegen open Genarg open Genredexpr -open Tok (* necessary for camlp5 *) open Names open Attributes @@ -63,14 +62,10 @@ let classic_proof_mode = Pvernac.register_proof_mode "Classic" tactic_mode (* Hack to parse "[ id" without dropping [ *) let test_bracket_ident = - Pcoq.Entry.of_parser "test_bracket_ident" - (fun _ strm -> - match stream_nth 0 strm with - | KEYWORD "[" -> - (match stream_nth 1 strm with - | IDENT _ -> () - | _ -> raise Stream.Failure) - | _ -> raise Stream.Failure) + let open Pcoq.Lookahead in + to_entry "test_bracket_ident" begin + lk_kw "[" >> lk_ident + end (* Tactics grammar rules *) @@ -368,7 +363,6 @@ let print_info_trace = ref None let () = declare_int_option { optdepr = false; - optname = "print info trace"; optkey = ["Info" ; "Level"]; optread = (fun () -> !print_info_trace); optwrite = fun n -> print_info_trace := n; diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index 5a7a634ed0..498b33d1a8 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 2209edcbb4..09cdc997ab 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index f0d6258cd1..6a158bde17 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -38,45 +38,24 @@ let err () = raise Stream.Failure (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *) (* admissible notation "(x t)" *) let test_lpar_id_coloneq = - Pcoq.Entry.of_parser "lpar_id_coloneq" - (fun _ strm -> - match stream_nth 0 strm with - | KEYWORD "(" -> - (match stream_nth 1 strm with - | IDENT _ -> - (match stream_nth 2 strm with - | KEYWORD ":=" -> () - | _ -> err ()) - | _ -> err ()) - | _ -> err ()) + let open Pcoq.Lookahead in + to_entry "lpar_id_coloneq" begin + lk_kw "(" >> lk_ident >> lk_kw ":=" + end (* Hack to recognize "(x)" *) let test_lpar_id_rpar = - Pcoq.Entry.of_parser "lpar_id_coloneq" - (fun _ strm -> - match stream_nth 0 strm with - | KEYWORD "(" -> - (match stream_nth 1 strm with - | IDENT _ -> - (match stream_nth 2 strm with - | KEYWORD ")" -> () - | _ -> err ()) - | _ -> err ()) - | _ -> err ()) + let open Pcoq.Lookahead in + to_entry "lpar_id_coloneq" begin + lk_kw "(" >> lk_ident >> lk_kw ")" + end (* idem for (x:=t) and (1:=t) *) let test_lpar_idnum_coloneq = - Pcoq.Entry.of_parser "test_lpar_idnum_coloneq" - (fun _ strm -> - match stream_nth 0 strm with - | KEYWORD "(" -> - (match stream_nth 1 strm with - | IDENT _ | NUMERAL _ -> - (match stream_nth 2 strm with - | KEYWORD ":=" -> () - | _ -> err ()) - | _ -> err ()) - | _ -> err ()) + let open Pcoq.Lookahead in + to_entry "test_lpar_idnum_coloneq" begin + lk_kw "(" >> (lk_ident <+> lk_nat) >> lk_kw ":=" + end (* idem for (x:t) *) open Extraargs @@ -107,11 +86,10 @@ let check_for_coloneq = | _ -> err ()) let lookup_at_as_comma = - Pcoq.Entry.of_parser "lookup_at_as_comma" - (fun _ strm -> - match stream_nth 0 strm with - | KEYWORD (","|"at"|"as") -> () - | _ -> err ()) + let open Pcoq.Lookahead in + to_entry "lookup_at_as_comma" begin + lk_kws [",";"at";"as"] + end open Constr open Prim @@ -147,7 +125,7 @@ let destruction_arg_of_constr (c,lbind as clbind) = match lbind with | _ -> ElimOnConstr clbind let mkNumeral n = - Numeral ((if 0<=n then SPlus else SMinus),NumTok.int (string_of_int (abs n))) + Numeral (NumTok.Signed.of_int_string (string_of_int n)) let mkTacCase with_evar = function | [(clear,ElimOnConstr cl),(None,None),None],None -> @@ -207,10 +185,6 @@ let merge_occurrences loc cl = function in (Some p, ans) -let warn_deprecated_eqn_syntax = - CWarnings.create ~name:"deprecated-eqn-syntax" ~category:"deprecated" - (fun arg -> strbrk (Printf.sprintf "Syntax \"_eqn:%s\" is deprecated. Please use \"eqn:%s\" instead." arg arg)) - (* Auxiliary grammar rules *) open Pvernac.Vernac_ @@ -483,10 +457,6 @@ GRAMMAR EXTEND Gram ; eqn_ipat: [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> { Some (CAst.make ~loc pat) } - | IDENT "_eqn"; ":"; pat = naming_intropattern -> - { warn_deprecated_eqn_syntax ~loc "H"; Some (CAst.make ~loc pat) } - | IDENT "_eqn" -> - { warn_deprecated_eqn_syntax ~loc "?"; Some (CAst.make ~loc IntroAnonymous) } | -> { None } ] ] ; as_name: @@ -611,6 +581,16 @@ GRAMMAR EXTEND Gram { TacAtom (CAst.make ~loc @@ TacAssert (false,true,Some tac,ipat,c)) } | IDENT "eassert"; c = constr; ipat = as_ipat; tac = by_tactic -> { TacAtom (CAst.make ~loc @@ TacAssert (true,true,Some tac,ipat,c)) } + + (* Alternative syntax for "pose proof c as id by tac" *) + | IDENT "pose"; IDENT "proof"; test_lpar_id_coloneq; "("; lid = identref; ":="; + c = lconstr; ")" -> + { let { CAst.loc = loc; v = id } = lid in + TacAtom (CAst.make ?loc @@ TacAssert (false,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } + | IDENT "epose"; IDENT "proof"; test_lpar_id_coloneq; "("; lid = identref; ":="; + c = lconstr; ")" -> + { let { CAst.loc = loc; v = id } = lid in + TacAtom (CAst.make ?loc @@ TacAssert (true,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat -> { TacAtom (CAst.make ~loc @@ TacAssert (false,true,None,ipat,c)) } | IDENT "epose"; IDENT "proof"; c = lconstr; ipat = as_ipat -> diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml index 0e21115474..5b5ee64a56 100644 --- a/plugins/ltac/pltac.ml +++ b/plugins/ltac/pltac.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index aa2631ae41..8565c4b4d6 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 7843faaef3..09f1fc371a 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -17,7 +17,6 @@ open Constrexpr open Genarg open Geninterp open Stdarg -open Notation_gram open Tactypes open Locus open Genredexpr @@ -73,43 +72,43 @@ type 'a raw_extra_genarg_printer = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t) -> 'a -> Pp.t type 'a glob_extra_genarg_printer = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> entry_relative_level -> glob_tactic_expr -> Pp.t) -> 'a -> Pp.t type 'a extra_genarg_printer = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) -> + (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) -> 'a -> Pp.t type 'a raw_extra_genarg_printer_with_level = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) -> - tolerability -> 'a -> Pp.t + (Environ.env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t) -> + entry_relative_level -> 'a -> Pp.t type 'a glob_extra_genarg_printer_with_level = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) -> - tolerability -> 'a -> Pp.t + (Environ.env -> Evd.evar_map -> entry_relative_level -> glob_tactic_expr -> Pp.t) -> + entry_relative_level -> 'a -> Pp.t type 'a extra_genarg_printer_with_level = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) -> - tolerability -> 'a -> Pp.t + (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) -> + entry_relative_level -> 'a -> Pp.t let string_of_genarg_arg (ArgumentType arg) = let rec aux : type a b c. (a, b, c) genarg_type -> string = function @@ -294,7 +293,7 @@ let string_of_genarg_arg (ArgumentType arg) = let pr _ = str "_" in KerName.print key ++ spc() ++ pr_sequence pr l ++ str" (* Generic printer *)" - let pr_farg prtac arg = prtac (1, Any) (TacArg (CAst.make arg)) + let pr_farg prtac arg = prtac LevelSome (TacArg (CAst.make arg)) let is_genarg tag wit = let ArgT.Any tag = tag in @@ -314,35 +313,35 @@ let string_of_genarg_arg (ArgumentType arg) = let rec pr_any_arg : type l. (_ -> l generic_argument -> Pp.t) -> _ -> l generic_argument -> Pp.t = fun prtac symb arg -> match symb with - | Extend.Uentry tag when is_genarg tag (genarg_tag arg) -> prtac (1, Any) arg + | Extend.Uentry tag when is_genarg tag (genarg_tag arg) -> prtac LevelSome arg | Extend.Ulist1 s | Extend.Ulist0 s -> begin match get_list arg with - | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + | None -> str "ltac:(" ++ prtac LevelSome arg ++ str ")" | Some l -> pr_sequence (pr_any_arg prtac s) l end | Extend.Ulist1sep (s, sep) | Extend.Ulist0sep (s, sep) -> begin match get_list arg with - | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + | None -> str "ltac:(" ++ prtac LevelSome arg ++ str ")" | Some l -> prlist_with_sep (fun () -> str sep) (pr_any_arg prtac s) l end | Extend.Uopt s -> begin match get_opt arg with - | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + | None -> str "ltac:(" ++ prtac LevelSome arg ++ str ")" | Some l -> pr_opt (pr_any_arg prtac s) l end | Extend.Uentry _ | Extend.Uentryl _ -> - str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + str "ltac:(" ++ prtac LevelSome arg ++ str ")" let pr_targ prtac symb arg = match symb with | Extend.Uentry tag when is_genarg tag (ArgumentType wit_tactic) -> - prtac (1, Any) arg - | Extend.Uentryl (_, l) -> prtac (l, Any) arg + prtac LevelSome arg + | Extend.Uentryl (_, l) -> prtac LevelSome arg | _ -> match arg with | TacGeneric arg -> let pr l arg = prtac l (TacGeneric arg) in pr_any_arg pr symb arg - | _ -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + | _ -> str "ltac:(" ++ prtac LevelSome arg ++ str ")" let pr_raw_extend_rec prtac = pr_extend_gen (pr_farg prtac) @@ -630,7 +629,7 @@ let pr_goal_selector ~toplevel s = let pr_then () = str ";" - let ltop = (5,E) + let ltop = LevelLe 5 let lseq = 4 let ltactical = 3 let lorelse = 2 @@ -645,13 +644,13 @@ let pr_goal_selector ~toplevel s = let ltatom = 1 let linfo = 5 - let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq + let level_of p = match p with LevelLe n -> n | LevelLt n -> n-1 | LevelSome -> lseq (** A printer for tactics that polymorphically works on the three "raw", "glob" and "typed" levels *) type 'a printer = { - pr_tactic : tolerability -> 'tacexpr -> Pp.t; + pr_tactic : entry_relative_level -> 'tacexpr -> Pp.t; pr_constr : Environ.env -> Evd.evar_map -> 'trm -> Pp.t; pr_lconstr : Environ.env -> Evd.evar_map -> 'trm -> Pp.t; pr_dconstr : Environ.env -> Evd.evar_map -> 'dtrm -> Pp.t; @@ -780,7 +779,7 @@ let pr_goal_selector ~toplevel s = hov 1 ( primitive (if b then if ev then "eassert" else "assert" else if ev then "eenough" else "enough") ++ pr_assumption (pr.pr_constr env sigma) (pr.pr_dconstr env sigma) (pr.pr_lconstr env sigma) ipat c ++ - pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac + pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (LevelLe ltactical))) tac ) | TacAssert (ev,_,None,ipat,c) -> hov 1 ( @@ -857,7 +856,7 @@ let pr_goal_selector ~toplevel s = pr_with_bindings_arg_full (pr.pr_dconstr env sigma) (pr.pr_dconstr env sigma) c) l ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) cl - ++ pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac + ++ pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (LevelLe ltactical))) tac ) | TacInversion (DepInversion (k,c,ids),hyp) -> hov 1 ( @@ -893,11 +892,11 @@ let pr_goal_selector ~toplevel s = let return (doc, l) = (tag tac doc, l) in let (strm, prec) = return (match tac with | TacAbstract (t,None) -> - keyword "abstract " ++ pr_tac (labstract,L) t, labstract + keyword "abstract " ++ pr_tac (LevelLt labstract) t, labstract | TacAbstract (t,Some s) -> hov 0 ( keyword "abstract" - ++ str" (" ++ pr_tac (labstract,L) t ++ str")" ++ spc () + ++ str" (" ++ pr_tac (LevelLt labstract) t ++ str")" ++ spc () ++ keyword "using" ++ spc () ++ pr_id s), labstract | TacLetIn (recflag,llc,u) -> @@ -906,7 +905,7 @@ let pr_goal_selector ~toplevel s = (hv 0 ( pr_let_clauses recflag (pr.pr_generic env sigma) (pr_tac ltop) llc ++ spc () ++ keyword "in" - ) ++ fnl () ++ pr_tac (llet,E) u), + ) ++ fnl () ++ pr_tac (LevelLe llet) u), llet | TacMatch (lz,t,lrul) -> hov 0 ( @@ -931,17 +930,17 @@ let pr_goal_selector ~toplevel s = hov 2 ( keyword "fun" ++ prlist pr_funvar lvar ++ str " =>" ++ spc () - ++ pr_tac (lfun,E) body), + ++ pr_tac (LevelLe lfun) body), lfun | TacThens (t,tl) -> hov 1 ( - pr_tac (lseq,E) t ++ pr_then () ++ spc () + pr_tac (LevelLe lseq) t ++ pr_then () ++ spc () ++ pr_seq_body (pr_opt_tactic (pr_tac ltop)) tl), lseq | TacThen (t1,t2) -> hov 1 ( - pr_tac (lseq,E) t1 ++ pr_then () ++ spc () - ++ pr_tac (lseq,L) t2), + pr_tac (LevelLe lseq) t1 ++ pr_then () ++ spc () + ++ pr_tac (LevelLt lseq) t2), lseq | TacDispatch tl -> pr_dispatch (pr_tac ltop) tl, lseq @@ -949,78 +948,78 @@ let pr_goal_selector ~toplevel s = pr_tac_extend (pr_tac ltop) tf t tr , lseq | TacThens3parts (t1,tf,t2,tl) -> hov 1 ( - pr_tac (lseq,E) t1 ++ pr_then () ++ spc () + pr_tac (LevelLe lseq) t1 ++ pr_then () ++ spc () ++ pr_then_gen (pr_tac ltop) tf t2 tl), lseq | TacTry t -> hov 1 ( - keyword "try" ++ spc () ++ pr_tac (ltactical,E) t), + keyword "try" ++ spc () ++ pr_tac (LevelLe ltactical) t), ltactical | TacDo (n,t) -> hov 1 ( str "do" ++ spc () ++ pr_or_var int n ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacTimeout (n,t) -> hov 1 ( keyword "timeout " ++ pr_or_var int n ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacTime (s,t) -> hov 1 ( keyword "time" ++ pr_opt qstring s ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacRepeat t -> hov 1 ( keyword "repeat" ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacProgress t -> hov 1 ( keyword "progress" ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacShowHyps t -> hov 1 ( keyword "infoH" ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacInfo t -> hov 1 ( keyword "info" ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), linfo | TacOr (t1,t2) -> hov 1 ( - pr_tac (lorelse,L) t1 ++ spc () + pr_tac (LevelLt lorelse) t1 ++ spc () ++ str "+" ++ brk (1,1) - ++ pr_tac (lorelse,E) t2), + ++ pr_tac (LevelLe lorelse) t2), lorelse | TacOnce t -> hov 1 ( keyword "once" ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacExactlyOnce t -> hov 1 ( keyword "exactly_once" ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacIfThenCatch (t,tt,te) -> hov 1 ( - str"tryif" ++ spc() ++ pr_tac (ltactical,E) t ++ brk(1,1) ++ - str"then" ++ spc() ++ pr_tac (ltactical,E) tt ++ brk(1,1) ++ - str"else" ++ spc() ++ pr_tac (ltactical,E) te ++ brk(1,1)), + str"tryif" ++ spc() ++ pr_tac (LevelLe ltactical) t ++ brk(1,1) ++ + str"then" ++ spc() ++ pr_tac (LevelLe ltactical) tt ++ brk(1,1) ++ + str"else" ++ spc() ++ pr_tac (LevelLe ltactical) te ++ brk(1,1)), ltactical | TacOrelse (t1,t2) -> hov 1 ( - pr_tac (lorelse,L) t1 ++ spc () + pr_tac (LevelLt lorelse) t1 ++ spc () ++ str "||" ++ brk (1,1) - ++ pr_tac (lorelse,E) t2), + ++ pr_tac (LevelLe lorelse) t2), lorelse | TacFail (g,n,l) -> let arg = @@ -1042,7 +1041,7 @@ let pr_goal_selector ~toplevel s = | TacSolve tl -> keyword "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet | TacComplete t -> - pr_tac (lcomplete,E) t, lcomplete + pr_tac (LevelLe lcomplete) t, lcomplete | TacSelect (s, tac) -> pr_goal_selector ~toplevel:false s ++ spc () ++ pr_tac ltop tac, latom | TacId l -> keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom @@ -1398,10 +1397,10 @@ let () = let () = let printer env sigma _ _ prtac = prtac env sigma in declare_extra_genarg_pprule_with_level wit_tactic printer printer printer - ltop (0,E) + ltop (LevelLe 0) let () = let pr_unit _env _sigma _ _ _ _ () = str "()" in let printer env sigma _ _ prtac = prtac env sigma in declare_extra_genarg_pprule_with_level wit_ltac printer printer pr_unit - ltop (0,E) + ltop (LevelLe 0) diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 9cff3ea1eb..6a9fb5c2ea 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -16,7 +16,6 @@ open Geninterp open Names open Environ open Constrexpr -open Notation_gram open Genintern open Tacexpr open Tactypes @@ -29,43 +28,43 @@ type 'a raw_extra_genarg_printer = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t) -> 'a -> Pp.t type 'a glob_extra_genarg_printer = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> entry_relative_level -> glob_tactic_expr -> Pp.t) -> 'a -> Pp.t type 'a extra_genarg_printer = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) -> + (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) -> 'a -> Pp.t type 'a raw_extra_genarg_printer_with_level = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) -> - tolerability -> 'a -> Pp.t + (Environ.env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t) -> + entry_relative_level -> 'a -> Pp.t type 'a glob_extra_genarg_printer_with_level = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) -> - tolerability -> 'a -> Pp.t + (Environ.env -> Evd.evar_map -> entry_relative_level -> glob_tactic_expr -> Pp.t) -> + entry_relative_level -> 'a -> Pp.t type 'a extra_genarg_printer_with_level = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) -> - tolerability -> 'a -> Pp.t + (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) -> + entry_relative_level -> 'a -> Pp.t val declare_extra_genarg_pprule : ('a, 'b, 'c) genarg_type -> @@ -78,7 +77,7 @@ val declare_extra_genarg_pprule_with_level : 'a raw_extra_genarg_printer_with_level -> 'b glob_extra_genarg_printer_with_level -> 'c extra_genarg_printer_with_level -> - (* surroounded *) tolerability -> (* non-surroounded *) tolerability -> unit + (* surroounded *) entry_relative_level -> (* non-surroounded *) entry_relative_level -> unit val declare_extra_vernac_genarg_pprule : ('a, 'b, 'c) genarg_type -> @@ -140,7 +139,7 @@ val pr_ltac_constant : ltac_constant -> Pp.t val pr_raw_tactic : env -> Evd.evar_map -> raw_tactic_expr -> Pp.t -val pr_raw_tactic_level : env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t +val pr_raw_tactic_level : env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t val pr_glob_tactic : env -> glob_tactic_expr -> Pp.t @@ -155,10 +154,10 @@ val pr_match_pattern : ('a -> Pp.t) -> 'a match_pattern -> Pp.t val pr_match_rule : bool -> ('a -> Pp.t) -> ('b -> Pp.t) -> ('b, 'a) match_rule -> Pp.t -val pr_value : tolerability -> Val.t -> Pp.t +val pr_value : entry_relative_level -> Val.t -> Pp.t -val ltop : tolerability +val ltop : entry_relative_level -val make_constr_printer : (env -> Evd.evar_map -> tolerability -> 'a -> Pp.t) -> +val make_constr_printer : (env -> Evd.evar_map -> entry_relative_level -> 'a -> Pp.t) -> 'a Genprint.top_printer diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index fe5ebf1172..14fab251d0 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -450,7 +450,6 @@ let () = let open Goptions in declare_bool_option { optdepr = false; - optname = "Ltac Profiling"; optkey = ["Ltac"; "Profiling"]; optread = get_profiling; optwrite = set_profiling } diff --git a/plugins/ltac/profile_ltac.mli b/plugins/ltac/profile_ltac.mli index 7595f53fd7..6118a62933 100644 --- a/plugins/ltac/profile_ltac.mli +++ b/plugins/ltac/profile_ltac.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ltac/profile_ltac_tactics.mlg b/plugins/ltac/profile_ltac_tactics.mlg index 9dd71505c8..eb9d9cbdce 100644 --- a/plugins/ltac/profile_ltac_tactics.mlg +++ b/plugins/ltac/profile_ltac_tactics.mlg @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 98d14f3d33..321b05b97c 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -129,7 +129,7 @@ let find_class_proof proof_type proof_method env evars carrier relation = let evars', c = Typeclasses.resolve_one_typeclass env (goalevars evars) goal in if extends_undefined (goalevars evars) evars' then raise Not_found else app_poly_check env (evars',cstrevars evars) proof_method [| carrier; relation; c |] - with e when Logic.catchable_exception e -> raise Not_found + with e when CErrors.noncritical e -> raise Not_found (** Utility functions *) @@ -289,18 +289,18 @@ end) = struct if Int.equal n 0 then c else match EConstr.kind sigma c with - | App (f, [| a; b; relb |]) when Termops.is_global sigma (pointwise_relation_ref ()) f -> + | App (f, [| a; b; relb |]) when isRefX sigma (pointwise_relation_ref ()) f -> decomp_pointwise sigma (pred n) relb - | App (f, [| a; b; arelb |]) when Termops.is_global sigma (forall_relation_ref ()) f -> + | App (f, [| a; b; arelb |]) when isRefX sigma (forall_relation_ref ()) f -> decomp_pointwise sigma (pred n) (Reductionops.beta_applist sigma (arelb, [mkRel 1])) | _ -> invalid_arg "decomp_pointwise" let rec apply_pointwise sigma rel = function | arg :: args -> (match EConstr.kind sigma rel with - | App (f, [| a; b; relb |]) when Termops.is_global sigma (pointwise_relation_ref ()) f -> + | App (f, [| a; b; relb |]) when isRefX sigma (pointwise_relation_ref ()) f -> apply_pointwise sigma relb args - | App (f, [| a; b; arelb |]) when Termops.is_global sigma (forall_relation_ref ()) f -> + | App (f, [| a; b; arelb |]) when isRefX sigma (forall_relation_ref ()) f -> apply_pointwise sigma (Reductionops.beta_applist sigma (arelb, [arg])) args | _ -> invalid_arg "apply_pointwise") | [] -> rel @@ -357,7 +357,7 @@ end) = struct match EConstr.kind sigma t with | App (c, args) when Array.length args >= 2 -> let head = if isApp sigma c then fst (destApp sigma c) else c in - if Termops.is_global sigma (coq_eq_ref ()) head then None + if isRefX sigma (coq_eq_ref ()) head then None else (try let params, args = Array.chop (Array.length args - 2) args in @@ -483,7 +483,7 @@ let rec decompose_app_rel env evd t = | App (f, [||]) -> assert false | App (f, [|arg|]) -> let (f', argl, argr) = decompose_app_rel env evd arg in - let ty = Typing.unsafe_type_of env evd argl in + let ty = Retyping.get_type_of env evd argl in let r = Retyping.relevance_of_type env evd ty in let f'' = mkLambda (make_annot (Name default_dependent_ident) r, ty, mkLambda (make_annot (Name (Id.of_string "y")) r, lift 1 ty, @@ -724,8 +724,7 @@ let unify_eqn (car, rel, prf, c1, c2, holes, sort) l2r flags env (sigma, cstrs) let rew = if l2r then rew else symmetry env sort rew in Some rew with - | e when Class_tactics.catchable e -> None - | Reduction.NotConvertible -> None + | e when noncritical e -> None let unify_abs (car, rel, prf, c1, c2) l2r sort env (sigma, cstrs) t = try @@ -741,8 +740,7 @@ let unify_abs (car, rel, prf, c1, c2) l2r sort env (sigma, cstrs) t = let rew = if l2r then rew else symmetry env sort rew in Some rew with - | e when Class_tactics.catchable e -> None - | Reduction.NotConvertible -> None + | e when noncritical e -> None type rewrite_flags = { under_lambdas : bool; on_morphisms : bool } @@ -789,7 +787,8 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev let morphargs, morphobjs = Array.chop first args in let morphargs', morphobjs' = Array.chop first args' in let appm = mkApp(m, morphargs) in - let appmtype = Typing.unsafe_type_of env (goalevars evars) appm in + let evd, appmtype = Typing.type_of env (goalevars evars) appm in + let evars = evd, snd evars in let cstrs = List.map (Option.map (fun r -> r.rew_car, get_opt_rew_rel r.rew_prf)) (Array.to_list morphobjs') @@ -1879,13 +1878,13 @@ let declare_projection n instance_id r = let rec aux t = match EConstr.kind sigma t with | App (f, [| a ; a' ; rel; rel' |]) - when Termops.is_global sigma (PropGlobal.respectful_ref ()) f -> + when isRefX sigma (PropGlobal.respectful_ref ()) f -> succ (aux rel') | _ -> 0 in let init = match EConstr.kind sigma typ with - App (f, args) when Termops.is_global sigma (PropGlobal.respectful_ref ()) f -> + App (f, args) when isRefX sigma (PropGlobal.respectful_ref ()) f -> mkApp (f, fst (Array.chop (Array.length args - 2) args)) | _ -> typ in aux init @@ -1906,7 +1905,7 @@ let declare_projection n instance_id r = let build_morphism_signature env sigma m = let m,ctx = Constrintern.interp_constr env sigma m in let sigma = Evd.from_ctx ctx in - let t = Typing.unsafe_type_of env sigma m in + let t = Retyping.get_type_of env sigma m in let cstrs = let rec aux t = match EConstr.kind sigma t with @@ -1936,7 +1935,7 @@ let build_morphism_signature env sigma m = let default_morphism sign m = let env = Global.env () in let sigma = Evd.from_env env in - let t = Typing.unsafe_type_of env sigma m in + let t = Retyping.get_type_of env sigma m in let evars, _, sign, cstrs = PropGlobal.build_signature (sigma, Evar.Set.empty) env t (fst sign) (snd sign) in @@ -2195,10 +2194,10 @@ let setoid_transitivity c = (transitivity_red true c) let setoid_symmetry_in id = - let open Tacmach.New in Proofview.Goal.enter begin fun gl -> - let sigma = project gl in - let ctype = pf_unsafe_type_of gl (mkVar id) in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let ctype = Retyping.get_type_of env sigma (mkVar id) in let binders,concl = decompose_prod_assum sigma ctype in let (equiv, args) = decompose_app sigma concl in let rec split_last_two = function diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 576ed686d4..1161c84e6a 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ltac/tacarg.ml b/plugins/ltac/tacarg.ml index 252c15478d..4d588cd9a9 100644 --- a/plugins/ltac/tacarg.ml +++ b/plugins/ltac/tacarg.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ltac/tacarg.mli b/plugins/ltac/tacarg.mli index 945f237c91..c1f7354cdd 100644 --- a/plugins/ltac/tacarg.mli +++ b/plugins/ltac/tacarg.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index a57cc76faa..04d85ed390 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -341,8 +341,8 @@ let coerce_to_reference sigma v = match Value.to_constr v with | Some c -> begin - try fst (Termops.global_of_constr sigma c) - with Not_found -> raise (CannotCoerceTo "a reference") + try fst (EConstr.destRef sigma c) + with DestKO -> raise (CannotCoerceTo "a reference") end | None -> raise (CannotCoerceTo "a reference") diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index 22d1681a61..3afbb56b23 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 13a2f3b8c0..4af5699317 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -191,7 +191,7 @@ let add_tactic_entry (kn, ml, tg) state = in let prods = List.map map tg.tacgram_prods in let rules = make_rule mkact prods in - let r = ExtendRule (entry, None, (pos, [(None, None, [rules])])) in + let r = ExtendRule (entry, (pos, [(None, None, [rules])])) in ([r], state) let tactic_grammar = @@ -415,7 +415,7 @@ let create_ltac_quotation name cast (e, l) = in let action _ v _ _ _ loc = cast (Some loc, v) in let gram = (level, assoc, [Rule (rule, action)]) in - Pcoq.grammar_extend Pltac.tactic_arg None (None, [gram]) + Pcoq.grammar_extend Pltac.tactic_arg (None, [gram]) (** Command *) @@ -759,7 +759,7 @@ let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) = e | Vernacextend.Arg_rules rules -> let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in - let () = Pcoq.grammar_extend e None (None, [(None, None, rules)]) in + let () = Pcoq.grammar_extend e (None, [(None, None, rules)]) in e in let (rpr, gpr, tpr) = arg.arg_printer in diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 95b958955e..ce38431a18 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index 8bafbb7ea3..ce9189792e 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli index 6a1e6e3bbd..ebb16eac52 100644 --- a/plugins/ltac/tacenv.mli +++ b/plugins/ltac/tacenv.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index e6e0c9d92c..b77fb3acc7 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 6abcdf2afa..cfa224319c 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 4dc2ade7a1..597c3fdaac 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -363,7 +363,7 @@ let intern_typed_pattern ist ~as_type ~ltacvars p = let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = let interp_ref r = try Inl (intern_evaluable ist r) - with e when Logic.catchable_exception e -> + with e when CErrors.noncritical e -> (* Compatibility. In practice, this means that the code above is useless. Still the idea of having either an evaluable ref or a pattern seems interesting, with "head" reduction diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index 0480b0c34d..22ec15566b 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 98aa649b62..9e0b9d3254 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -165,8 +165,8 @@ let catching_error call_trace fail (e, info) = let catch_error call_trace f x = try f x with e when CErrors.noncritical e -> - let e = CErrors.push e in - catching_error call_trace iraise e + let e = Exninfo.capture e in + catching_error call_trace Exninfo.iraise e let wrap_error tac k = if is_traced () then Proofview.tclORELSE tac k else tac @@ -717,13 +717,13 @@ let interp_may_eval f ist env sigma = function try f ist env sigma c with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in (* spiwack: to avoid unnecessary modifications of tacinterp, as this function already use effect, I call [run] hoping it doesn't mess up with any assumption. *) Proofview.NonLogical.run (debugging_exception_step ist false (fst reraise) (fun () -> str"interpretation of term " ++ pr_glob_constr_env env (fst c))); - iraise reraise + Exninfo.iraise reraise (* Interprets a constr expression possibly to first evaluate *) let interp_constr_may_eval ist env sigma c = @@ -731,12 +731,12 @@ let interp_constr_may_eval ist env sigma c = try interp_may_eval interp_constr ist env sigma c with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in (* spiwack: to avoid unnecessary modifications of tacinterp, as this function already use effect, I call [run] hoping it doesn't mess up with any assumption. *) Proofview.NonLogical.run (debugging_exception_step ist false (fst reraise) (fun () -> str"evaluation of term")); - iraise reraise + Exninfo.iraise reraise in begin (* spiwack: to avoid unnecessary modifications of tacinterp, as this @@ -2082,7 +2082,6 @@ let () = let open Goptions in declare_bool_option { optdepr = false; - optname = "Ltac debug"; optkey = ["Ltac";"Debug"]; optread = (fun () -> get_debug () != Tactic_debug.DebugOff); optwrite = vernac_debug } @@ -2091,7 +2090,6 @@ let () = let open Goptions in declare_bool_option { optdepr = false; - optname = "Ltac Backtrace"; optkey = ["Ltac"; "Backtrace"]; optread = (fun () -> !log_trace); optwrite = (fun b -> log_trace := b) } diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index c7c30bc167..ce34356a37 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index e864d31da4..600c30b403 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ltac/tacsubst.mli b/plugins/ltac/tacsubst.mli index 00b148166a..c6d48a5cf2 100644 --- a/plugins/ltac/tacsubst.mli +++ b/plugins/ltac/tacsubst.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 539536911c..5fbea4eeef 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -86,7 +86,6 @@ open Goptions let () = declare_bool_option { optdepr = false; - optname = "Ltac batch debug"; optkey = ["Ltac";"Batch";"Debug"]; optread = (fun () -> !batch); optwrite = (fun x -> batch := x) } @@ -108,13 +107,29 @@ let db_initialize = let int_of_string s = try Proofview.NonLogical.return (int_of_string s) - with e -> Proofview.NonLogical.raise e + with e -> + let e = Exninfo.capture e in + Proofview.NonLogical.raise e let string_get s i = try Proofview.NonLogical.return (String.get s i) - with e -> Proofview.NonLogical.raise e + with e -> + let e = Exninfo.capture e in + Proofview.NonLogical.raise e + +let check_positive n = + try + if n < 0 then + raise (Invalid_argument "number must be positive") + else + Proofview.NonLogical.return () + with e -> + let e = Exninfo.capture e in + Proofview.NonLogical.raise e -let run_invalid_arg () = Proofview.NonLogical.raise (Invalid_argument "run_com") +let run_invalid_arg () = + let info = Exninfo.null in + Proofview.NonLogical.raise (Invalid_argument "run_com", info) (* Gives the number of steps or next breakpoint of a run command *) let run_com inst = @@ -126,7 +141,7 @@ let run_com inst = let s = String.sub inst i (String.length inst - i) in if inst.[0] >= '0' && inst.[0] <= '9' then int_of_string s >>= fun num -> - (if num<0 then run_invalid_arg () else return ()) >> + check_positive num >> (skip:=num) >> (skipped:=0) else breakpoint:=Some (possibly_unquote s) @@ -157,11 +172,11 @@ let rec prompt level = let open Proofview.NonLogical in Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >> if Util.(!batch) then return (DebugOn (level+1)) else - let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in + let exit = (skip:=0) >> (skipped:=0) >> raise (Sys.Break, Exninfo.null) in Proofview.NonLogical.catch Proofview.NonLogical.read_line begin function (e, info) -> match e with | End_of_file -> exit - | e -> raise ~info e + | e -> raise (e, info) end >>= fun inst -> match inst with @@ -177,7 +192,7 @@ let rec prompt level = Proofview.NonLogical.catch (run_com inst >> runtrue >> return (DebugOn (level+1))) begin function (e, info) -> match e with | Failure _ | Invalid_argument _ -> prompt level - | e -> raise ~info e + | e -> raise (e, info) end end @@ -214,9 +229,7 @@ let debug_prompt lev tac f = Proofview.tclTHEN (Proofview.tclLIFT begin (skip:=0) >> (skipped:=0) >> - if Logic.catchable_exception reraise then - msg_tac_debug (str "Level " ++ int lev ++ str ": " ++ explain_logic_error reraise) - else return () + msg_tac_debug (str "Level " ++ int lev ++ str ": " ++ explain_logic_error reraise) end) (Proofview.tclZERO ~info reraise) end @@ -403,7 +416,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 Loc.finer loc tloc then loc else tloc), Some msg + (if Loc.finer loc tloc then loc else tloc), msg else (* We entered a primitive tactic, we don't display trace but report on the finest location *) @@ -419,7 +432,7 @@ let extract_ltac_trace ?loc trace = aux best_loc tail | [] -> best_loc in aux loc trace in - best_loc, None + best_loc, mt () let get_ltac_trace info = let ltac_trace = Exninfo.get info ltac_trace_info in diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli index e0126ad448..1cb0212580 100644 --- a/plugins/ltac/tactic_debug.mli +++ b/plugins/ltac/tactic_debug.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -79,4 +79,4 @@ val db_breakpoint : debug_info -> lident message_token list -> unit Proofview.NonLogical.t val extract_ltac_trace : - ?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.t option Loc.located + ?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.t Loc.located diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index eabfe2f540..525199735d 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -227,11 +227,9 @@ module PatternMatching (E:StaticEnvironment) = struct substitution. *) let wildcard_match_term = return - (** [pattern_match_term refresh pat term lhs] returns the possible - matchings of [term] with the pattern [pat => lhs]. If refresh is - true, refreshes the universes of [term]. *) - let pattern_match_term refresh pat term lhs = -(* let term = if refresh then Termops.refresh_universes_strict term else term in *) + (** [pattern_match_term pat term lhs] returns the possible + matchings of [term] with the pattern [pat => lhs]. *) + let pattern_match_term pat term lhs = match pat with | Term p -> begin @@ -262,7 +260,7 @@ module PatternMatching (E:StaticEnvironment) = struct matching rule [rule]. *) let rule_match_term term = function | All lhs -> wildcard_match_term lhs - | Pat ([],pat,lhs) -> pattern_match_term false pat term lhs + | Pat ([],pat,lhs) -> pattern_match_term pat term lhs | Pat _ -> (* Rules with hypotheses, only work in match goal. *) fail @@ -286,8 +284,7 @@ module PatternMatching (E:StaticEnvironment) = struct let hyp_match_type hypname pat hyps = pick hyps >>= fun decl -> let id = NamedDecl.get_id decl in - let refresh = is_local_def decl in - pattern_match_term refresh pat (NamedDecl.get_type decl) () <*> + pattern_match_term pat (NamedDecl.get_type decl) () <*> put_terms (id_map_try_add_name hypname (EConstr.mkVar id) empty_term_subst) <*> return id @@ -298,8 +295,8 @@ module PatternMatching (E:StaticEnvironment) = struct let hyp_match_body_and_type hypname bodypat typepat hyps = pick hyps >>= function | LocalDef (id,body,hyp) -> - pattern_match_term false bodypat body () <*> - pattern_match_term true typepat hyp () <*> + pattern_match_term bodypat body () <*> + pattern_match_term typepat hyp () <*> put_terms (id_map_try_add_name hypname (EConstr.mkVar id.binder_name) empty_term_subst) <*> return id.binder_name | LocalAssum (id,hyp) -> fail @@ -337,7 +334,7 @@ module PatternMatching (E:StaticEnvironment) = struct (* the rules are applied from the topmost one (in the concrete syntax) to the bottommost. *) let hyppats = List.rev hyppats in - pattern_match_term false conclpat concl () <*> + pattern_match_term conclpat concl () <*> hyp_pattern_list_match hyppats hyps lhs (** [match_goal hyps concl rules] matches the goal [hyps|-concl] diff --git a/plugins/ltac/tactic_matching.mli b/plugins/ltac/tactic_matching.mli index b847ebbc66..dbcb2d2025 100644 --- a/plugins/ltac/tactic_matching.mli +++ b/plugins/ltac/tactic_matching.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ltac/tactic_option.ml b/plugins/ltac/tactic_option.ml index da57f51ca3..c72a527537 100644 --- a/plugins/ltac/tactic_option.ml +++ b/plugins/ltac/tactic_option.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ltac/tactic_option.mli b/plugins/ltac/tactic_option.mli index 9705d225d4..6bd4b14286 100644 --- a/plugins/ltac/tactic_option.mli +++ b/plugins/ltac/tactic_option.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index ba759441e5..a7b571d3db 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -68,7 +68,6 @@ open Goptions let () = declare_bool_option { optdepr = false; - optname = "unfolding of not in intuition"; optkey = ["Intuition";"Negation";"Unfolding"]; optread = (fun () -> !negation_unfolding); optwrite = (:=) negation_unfolding } |