diff options
53 files changed, 282 insertions, 519 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 7dda19192d..ea7eccb47f 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -82,7 +82,7 @@ after_script: - echo 'end:coq:build' - echo 'start:coq.install' - - make install + - make install install-byte $EXTRA_INSTALL - make install-byte - cp bin/fake_ide _install_ci/bin/ - echo 'end:coq.install' @@ -196,6 +196,7 @@ build:base: COQ_EXTRA_CONF: "-native-compiler yes -coqide opt" # coqdoc for stdlib, until we know how to build it from installed Coq EXTRA_TARGET: "stdlib" + EXTRA_INSTALL: "install-doc-stdlib-html install-doc-printable" # no coqide for 32bit: libgtk installation problems build:base+32bit: diff --git a/dev/base_include b/dev/base_include index 0e12b57b36..d2e8f6d092 100644 --- a/dev/base_include +++ b/dev/base_include @@ -135,7 +135,6 @@ open Pfedit open Proof open Proof_using open Proof_global -open Proof_type open Redexpr open Refiner open Tacmach diff --git a/dev/ci/README.md b/dev/ci/README.md index 4709247549..7ed90f524c 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -179,7 +179,7 @@ Currently available artifacts are: + Coq's Reference Manual [master branch] https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman + Coq's Standard Library Documentation [master branch] - https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/html/stdlib/index.html?job=doc:refman + https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/html/stdlib/index.html?job=build:base + Coq's ML API Documentation [master branch] https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_build/default/_doc/_html/index.html?job=doc:ml-api:odoc diff --git a/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh b/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh new file mode 100644 index 0000000000..c8bea0c868 --- /dev/null +++ b/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "8998" ] || [ "$CI_BRANCH" = "legacy_proof_eng_clean" ]; then + + equations_CI_REF=legacy_proof_eng_clean + equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + +fi diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index c5ea88aaf6..3609171b82 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -10,7 +10,8 @@ Coq can now be built using [Dune](https://github.com/ocaml/dune). ## Quick Start -You need Dune >= 1.2.1 ; just type `dune build` to build the base Coq +Dune >= 1.5.0 is recommended, see `dune-project` for the minimum +required version; type `dune build` to build the base Coq libraries. No call to `./configure` is needed. Dune will get confused if it finds leftovers of in-tree compilation, @@ -49,14 +50,25 @@ The default dune target is `dune build` (or `dune build @install`), which will scan all sources in the Coq tree and then build the whole project, creating an "install" overlay in `_build/install/default`. -You can build some other target by doing `dune build $TARGET`. +You can build some other target by doing `dune build $TARGET`, where +`$TARGET` can be a `.cmxa`, a binary, a file that Dune considers a +target, an alias, etc... In order to build a single package, you can do `dune build $PACKAGE.install`. +A very useful target is `dune build @check`, that will compile all the +ml files in quick mode. + Dune also provides targets for documentation, testing, and release builds, please see below. +## Documentation and test targets + +Coq's test-suite can be run with `dune runtest`. + +The documentation target is not implemented in Dune yet. + ## Developer shell You can create a developer shell with `dune utop $library`, where @@ -139,11 +151,6 @@ Note that due to https://github.com/ocaml/dune/issues/1401 , we must perform a full rebuild each time as otherwise Dune will remove the files. We hope to solve this in the future. -## Documentation and test targets - -The documentation and test suite targets for Coq are still not -implemented in Dune. - ## Planned and Advanced features Dune supports or will support extra functionality that may result very diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt index 764d482957..e5e4f740bd 100644 --- a/dev/doc/coq-src-description.txt +++ b/dev/doc/coq-src-description.txt @@ -94,7 +94,7 @@ Tacexpr.glob_tactic_expr | | Tacinterp.eval_tactic (?) V -Proof_type.tactic +Proofview.V82.tac TODO: check with Hugo @@ -4,6 +4,7 @@ (synopsis "Coq's Debug Printers") (wrapped false) (modules :standard) + (optional) (libraries coq.toplevel coq.plugins.ltac)) (rule diff --git a/dev/top_printers.mli b/dev/top_printers.mli index eaa12ff702..5eac3e2b9c 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -120,9 +120,9 @@ val ppclenv : Clenv.clausenv -> unit val ppgoalgoal : Goal.goal -> unit -val ppgoal : Proof_type.goal Evd.sigma -> unit +val ppgoal : Goal.goal Evd.sigma -> unit (* also print evar map *) -val ppgoalsigma : Proof_type.goal Evd.sigma -> unit +val ppgoalsigma : Goal.goal Evd.sigma -> unit val pphintdb : Hints.Hint_db.t -> unit val ppproofview : Proofview.proofview -> unit @@ -43,3 +43,14 @@ (package coqide) (modules coqide_main) (libraries coqide.gui)) + +; FIXME: we should install those in share/coqide. We better do this +; once the make-based system has been phased out. +(install + (section share_root) + (package coqide) + (files + (coq.png as coq/coq.png) + (coq_style.xml as coq/coq_style.xml) + (coq.lang as coq/coq.lang) + (coq-ssreflect.lang as coq/coq-ssreflect.lang))) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 92fa94d6dc..ef1d1af199 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -131,8 +131,7 @@ let finish_proof dynamic_infos g = g -let refine c = - Tacmach.refine c +let refine c = Refiner.refiner ~check:true EConstr.Unsafe.(to_constr c) let thin l = Proofview.V82.of_tactic (Tactics.clear l) diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 188d5de7de..ac2d88dec2 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -697,7 +697,7 @@ type ('b, 'c) argument_interp = | ArgInterpFun : ('b, Val.t) interp_fun -> ('b, 'c) argument_interp | ArgInterpWit : ('a, 'b, 'r) Genarg.genarg_type -> ('b, 'c) argument_interp | ArgInterpLegacy : - (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp + (Geninterp.interp_sign -> Goal.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp type ('a, 'b, 'c) tactic_argument = { arg_parsing : 'a Vernacextend.argument_rule; diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 79f9e093fb..309db539d0 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -125,7 +125,7 @@ type ('b, 'c) argument_interp = | ArgInterpFun : ('b, Geninterp.Val.t) Geninterp.interp_fun -> ('b, 'c) argument_interp | ArgInterpWit : ('a, 'b, 'r) Genarg.genarg_type -> ('b, 'c) argument_interp | ArgInterpLegacy : - (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp + (Geninterp.interp_sign -> Goal.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp type ('a, 'b, 'c) tactic_argument = { arg_parsing : 'a Vernacextend.argument_rule; diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml index 1c4508abf4..3e0fbc9a8c 100644 --- a/plugins/ssr/ssrbwd.ml +++ b/plugins/ssr/ssrbwd.ml @@ -104,8 +104,6 @@ let mkRAppView ist gl rv gv = let nb_view_imps = interp_view_nbimps ist gl rv in mkRApp rv (mkRHoles (abs nb_view_imps)) -let prof_apply_interp_with = mk_profiler "ssrapplytac.interp_with";; - let refine_interp_apply_view dbl ist gl gv = let pair i = List.map (fun x -> i, x) in let rv = pf_intern_term ist gl gv in @@ -113,7 +111,6 @@ let refine_interp_apply_view dbl ist gl gv = let interp_with (dbl, hint) = let i = if dbl = Ssrview.AdaptorDb.Equivalence then 2 else 1 in interp_refine ist gl (mkRApp hint (v :: mkRHoles i)) in - let interp_with x = prof_apply_interp_with.profile interp_with x in let rec loop = function | [] -> (try apply_rconstr ~ist rv gl with _ -> view_error "apply" gv) | h :: hs -> (try refine_with (snd (interp_with h)) gl with _ -> loop hs) in diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 80d421b9fc..0a781ea8a9 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1000,7 +1000,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl = | _ -> assert false in loop sigma t [] n in pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t)); - Tacmach.refine_no_check t gl + Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t) gl let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl = let rec mkRels = function 1 -> [] | n -> mkRel n :: mkRels (n-1) in @@ -1017,81 +1017,6 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl = try applyn ~with_evars ~with_shelve:true ?beta n (EConstr.of_constr oc) gl with e when CErrors.noncritical e -> raise dependent_apply_error -(** Profiling *)(* {{{ *************************************************************) -type profiler = { - profile : 'a 'b. ('a -> 'b) -> 'a -> 'b; - reset : unit -> unit; - print : unit -> unit } -let profile_now = ref false -let something_profiled = ref false -let profilers = ref [] -let add_profiler f = profilers := f :: !profilers;; -let _ = - Goptions.declare_bool_option - { Goptions.optname = "ssreflect profiling"; - Goptions.optkey = ["SsrProfiling"]; - Goptions.optread = (fun _ -> !profile_now); - Goptions.optdepr = false; - Goptions.optwrite = (fun b -> - Ssrmatching.profile b; - profile_now := b; - if b then List.iter (fun f -> f.reset ()) !profilers; - if not b then List.iter (fun f -> f.print ()) !profilers) } -let () = - let prof_total = - let init = ref 0.0 in { - profile = (fun f x -> assert false); - reset = (fun () -> init := Unix.gettimeofday ()); - print = (fun () -> if !something_profiled then - prerr_endline - (Printf.sprintf "!! %-39s %10d %9.4f %9.4f %9.4f" - "total" 0 (Unix.gettimeofday() -. !init) 0.0 0.0)) } in - let prof_legenda = { - profile = (fun f x -> assert false); - reset = (fun () -> ()); - print = (fun () -> if !something_profiled then begin - prerr_endline - (Printf.sprintf "!! %39s ---------- --------- --------- ---------" - (String.make 39 '-')); - prerr_endline - (Printf.sprintf "!! %-39s %10s %9s %9s %9s" - "function" "#calls" "total" "max" "average") end) } in - add_profiler prof_legenda; - add_profiler prof_total -;; - -let mk_profiler s = - let total, calls, max = ref 0.0, ref 0, ref 0.0 in - let reset () = total := 0.0; calls := 0; max := 0.0 in - let profile f x = - if not !profile_now then f x else - let before = Unix.gettimeofday () in - try - incr calls; - let res = f x in - let after = Unix.gettimeofday () in - let delta = after -. before in - total := !total +. delta; - if delta > !max then max := delta; - res - with exc -> - let after = Unix.gettimeofday () in - let delta = after -. before in - total := !total +. delta; - if delta > !max then max := delta; - raise exc in - let print () = - if !calls <> 0 then begin - something_profiled := true; - prerr_endline - (Printf.sprintf "!! %-39s %10d %9.4f %9.4f %9.4f" - s !calls !total !max (!total /. (float_of_int !calls))) end in - let prof = { profile = profile; reset = reset; print = print } in - add_profiler prof; - prof -;; -(* }}} *) - (* We wipe out all the keywords generated by the grammar rules we defined. *) (* The user is supposed to Require Import ssreflect or Require ssreflect *) (* and Import ssreflect.SsrSyntax to obtain these keywords and as a *) diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index cf4e4b354e..e25c93bf0a 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -164,7 +164,7 @@ val mk_lterm : constr_expr -> ssrterm val mk_ast_closure_term : [ `None | `Parens | `DoubleParens | `At ] -> Constrexpr.constr_expr -> ast_closure_term -val interp_ast_closure_term : Geninterp.interp_sign -> Proof_type.goal +val interp_ast_closure_term : Geninterp.interp_sign -> Goal.goal Evd.sigma -> ast_closure_term -> Evd.evar_map * ast_closure_term val subst_ast_closure_term : Mod_subst.substitution -> ast_closure_term -> ast_closure_term val glob_ast_closure_term : Genintern.glob_sign -> ast_closure_term -> ast_closure_term @@ -378,13 +378,6 @@ val pf_interp_gen_aux : val is_name_in_ipats : Id.t -> ssripats -> bool -type profiler = { - profile : 'a 'b. ('a -> 'b) -> 'a -> 'b; - reset : unit -> unit; - print : unit -> unit } - -val mk_profiler : string -> profiler - (** Basic tactics *) val introid : ?orig:Name.t ref -> Id.t -> v82tac diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index d09b81593e..1bd88ae3dd 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -398,7 +398,7 @@ let revtoptac n0 gl = let dc, cl = EConstr.decompose_prod_n_assum (project gl) n (pf_concl gl) in let dc' = dc @ [Context.Rel.Declaration.LocalAssum(Name rev_id, EConstr.it_mkProd_or_LetIn cl (List.rev dc))] in let f = EConstr.it_mkLambda_or_LetIn (mkEtaApp (EConstr.mkRel (n + 1)) (-n) 1) dc' in - refine (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|])) gl + Refiner.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|]))) gl let equality_inj l b id c gl = let msg = ref "" in diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 2a69e3f23a..22475fef34 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -425,11 +425,6 @@ let rwcltac cl rdx dir sr gl = in tclTHEN cvtac' rwtac gl -let prof_rwcltac = mk_profiler "rwrxtac.rwcltac";; -let rwcltac cl rdx dir sr gl = - prof_rwcltac.profile (rwcltac cl rdx dir sr) gl -;; - [@@@ocaml.warning "-3"] let lz_coq_prod = @@ -455,8 +450,6 @@ let ssr_is_setoid env = Rewrite.is_applied_rewrite_relation env sigma [] (EConstr.mkApp (r, args)) <> None -let prof_rwxrtac_find_rule = mk_profiler "rwrxtac.find_rule";; - let closed0_check cl p gl = if closed0 cl then errorstrm Pp.(str"No occurrence of redex "++ pr_constr_env (pf_env gl) (project gl) p) @@ -556,7 +549,6 @@ let rwrxtac occ rdx_pat dir rule gl = d, (ise, Evd.evar_universe_context ise, Reductionops.nf_evar ise r) with _ -> rwtac rs in rwtac rules in - let find_rule rdx = prof_rwxrtac_find_rule.profile find_rule rdx in let sigma0, env0, concl0 = project gl, pf_env gl, pf_concl gl in let find_R, conclude = match rdx_pat with | Some (_, (In_T _ | In_X_In_T _)) | None -> @@ -582,11 +574,6 @@ let rwrxtac occ rdx_pat dir rule gl = rwcltac (EConstr.of_constr concl) (EConstr.of_constr rdx) d r gl ;; -let prof_rwxrtac = mk_profiler "rwrxtac";; -let rwrxtac occ rdx_pat dir rule gl = - prof_rwxrtac.profile (rwrxtac occ rdx_pat dir rule) gl -;; - let ssrinstancesofrule ist dir arg gl = let sigma0, env0, concl0 = project gl, pf_env gl, pf_concl gl in let rule = interp_term ist gl arg in diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 142d1ac790..8cb0a8b463 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -174,82 +174,6 @@ let nf_evar sigma c = (* }}} *) -(** Profiling *)(* {{{ *************************************************************) -type profiler = { - profile : 'a 'b. ('a -> 'b) -> 'a -> 'b; - reset : unit -> unit; - print : unit -> unit } -let profile_now = ref false -let something_profiled = ref false -let profilers = ref [] -let add_profiler f = profilers := f :: !profilers;; -let profile b = - profile_now := b; - if b then List.iter (fun f -> f.reset ()) !profilers; - if not b then List.iter (fun f -> f.print ()) !profilers -;; -let _ = - Goptions.declare_bool_option - { Goptions.optname = "ssrmatching profiling"; - Goptions.optkey = ["SsrMatchingProfiling"]; - Goptions.optread = (fun _ -> !profile_now); - Goptions.optdepr = false; - Goptions.optwrite = profile } -let () = - let prof_total = - let init = ref 0.0 in { - profile = (fun f x -> assert false); - reset = (fun () -> init := Unix.gettimeofday ()); - print = (fun () -> if !something_profiled then - prerr_endline - (Printf.sprintf "!! %-39s %10d %9.4f %9.4f %9.4f" - "total" 0 (Unix.gettimeofday() -. !init) 0.0 0.0)) } in - let prof_legenda = { - profile = (fun f x -> assert false); - reset = (fun () -> ()); - print = (fun () -> if !something_profiled then begin - prerr_endline - (Printf.sprintf "!! %39s ---------- --------- --------- ---------" - (String.make 39 '-')); - prerr_endline - (Printf.sprintf "!! %-39s %10s %9s %9s %9s" - "function" "#calls" "total" "max" "average") end) } in - add_profiler prof_legenda; - add_profiler prof_total -;; - -let mk_profiler s = - let total, calls, max = ref 0.0, ref 0, ref 0.0 in - let reset () = total := 0.0; calls := 0; max := 0.0 in - let profile f x = - if not !profile_now then f x else - let before = Unix.gettimeofday () in - try - incr calls; - let res = f x in - let after = Unix.gettimeofday () in - let delta = after -. before in - total := !total +. delta; - if delta > !max then max := delta; - res - with exc -> - let after = Unix.gettimeofday () in - let delta = after -. before in - total := !total +. delta; - if delta > !max then max := delta; - raise exc in - let print () = - if !calls <> 0 then begin - something_profiled := true; - prerr_endline - (Printf.sprintf "!! %-39s %10d %9.4f %9.4f %9.4f" - s !calls !total !max (!total /. (float_of_int !calls))) end in - let prof = { profile = profile; reset = reset; print = print } in - add_profiler prof; - prof -;; -(* }}} *) - exception NoProgress (** Unification procedures. *) @@ -286,11 +210,6 @@ let unif_EQ_args env sigma pa a = let rec loop i = (i = n) || unif_EQ env sigma pa.(i) a.(i) && loop (i + 1) in loop 0 -let prof_unif_eq_args = mk_profiler "unif_EQ_args";; -let unif_EQ_args env sigma pa a = - prof_unif_eq_args.profile (unif_EQ_args env sigma pa) a -;; - let unif_HO env ise p c = try Evarconv.the_conv_x env p c ise with Evarconv.UnableToUnify(ise, err) -> @@ -650,11 +569,6 @@ let match_upats_FO upats env sigma0 ise orig_c = iter_constr_LR loop f; Array.iter loop a in try loop orig_c with Invalid_argument _ -> CErrors.anomaly (str"IN FO.") -let prof_FO = mk_profiler "match_upats_FO";; -let match_upats_FO upats env sigma0 ise c = - prof_FO.profile (match_upats_FO upats env sigma0) ise c -;; - let match_upats_HO ~on_instance upats env sigma0 ise c = let dont_impact_evars = dont_impact_evars_in c in @@ -706,11 +620,6 @@ let match_upats_HO ~on_instance upats env sigma0 ise c = if !it_did_match then raise NoProgress; !failed_because_of_TC -let prof_HO = mk_profiler "match_upats_HO";; -let match_upats_HO ~on_instance upats env sigma0 ise c = - prof_HO.profile (match_upats_HO ~on_instance upats env sigma0) ise c -;; - let fixed_upat evd = function | {up_k = KpatFlex | KpatEvar _ | KpatProj _} -> false diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index b3ddb52e85..93a8c48435 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -221,10 +221,6 @@ val pf_unsafe_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma (* One can also "Set SsrMatchingDebug" from a .v *) val debug : bool -> unit -(* One should delimit a snippet with "Set SsrMatchingProfiling" and - * "Unset SsrMatchingProfiling" to get timings *) -val profile : bool -> unit - val ssrinstancesof : cpattern -> Tacmach.tactic (** Functions used for grammar extensions. Do not use. *) @@ -234,7 +230,7 @@ sig val wit_rpatternty : (rpattern, rpattern, rpattern) Genarg.genarg_type val glob_rpattern : Genintern.glob_sign -> rpattern -> rpattern val subst_rpattern : Mod_subst.substitution -> rpattern -> rpattern - val interp_rpattern : Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> rpattern -> Evd.evar_map * rpattern + val interp_rpattern : Geninterp.interp_sign -> Goal.goal Evd.sigma -> rpattern -> Evd.evar_map * rpattern val pr_rpattern : rpattern -> Pp.t val mk_rpattern : (cpattern, cpattern) ssrpattern -> rpattern val mk_lterm : Constrexpr.constr_expr -> Geninterp.interp_sign option -> cpattern @@ -242,7 +238,7 @@ sig val glob_cpattern : Genintern.glob_sign -> cpattern -> cpattern val subst_ssrterm : Mod_subst.substitution -> cpattern -> cpattern - val interp_ssrterm : Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> cpattern -> Evd.evar_map * cpattern + val interp_ssrterm : Geninterp.interp_sign -> Goal.goal Evd.sigma -> cpattern -> Evd.evar_map * cpattern val pr_ssrterm : cpattern -> Pp.t end diff --git a/printing/printer.mli b/printing/printer.mli index 785f452a7b..cefc005c74 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -13,7 +13,6 @@ open Constr open Environ open Pattern open Evd -open Proof_type open Glob_term open Ltac_pretype @@ -144,7 +143,7 @@ val pr_transparent_state : TransparentState.t -> Pp.t records containing the goal and sigma for, respectively, the new and old proof steps, e.g. [{ it = g ; sigma = sigma }]. *) -val pr_goal : ?diffs:bool -> ?og_s:(goal sigma) -> goal sigma -> Pp.t +val pr_goal : ?diffs:bool -> ?og_s:(Goal.goal sigma) -> Goal.goal sigma -> Pp.t (** [pr_subgoals ~pr_first ~diffs ~os_map close_cmd sigma ~seeds ~shelf ~stack ~unfocused ~goals] prints the goals in [goals] followed by the goals in [unfocused] in a compact form @@ -161,17 +160,17 @@ val pr_goal : ?diffs:bool -> ?og_s:(goal sigma) -> goal sigma -> there are non-instantiated existential variables. [stack] is used to print summary info on unfocused goals. *) -val pr_subgoals : ?pr_first:bool -> ?diffs:bool -> ?os_map:(evar_map * Evar.t Evar.Map.t) -> Pp.t option -> evar_map - -> seeds:goal list -> shelf:goal list -> stack:int list - -> unfocused: goal list -> goals:goal list -> Pp.t +val pr_subgoals : ?pr_first:bool -> ?diffs:bool -> ?os_map:(evar_map * Goal.goal Evar.Map.t) -> Pp.t option -> evar_map + -> seeds:Goal.goal list -> shelf:Goal.goal list -> stack:int list + -> unfocused:Goal.goal list -> goals:Goal.goal list -> Pp.t -val pr_subgoal : int -> evar_map -> goal list -> Pp.t +val pr_subgoal : int -> evar_map -> Goal.goal list -> Pp.t (** [pr_concl n ~diffs ~og_s sigma g] prints the conclusion of the goal [g] using [sigma]. The output is labelled "subgoal [n]". If [diffs] is true, highlight the differences between the old conclusion, [og_s], and [g]+[sigma]. [og_s] is a record containing the old goal and sigma, e.g. [{ it = g ; sigma = sigma }]. *) -val pr_concl : int -> ?diffs:bool -> ?og_s:(goal sigma) -> evar_map -> goal -> Pp.t +val pr_concl : int -> ?diffs:bool -> ?og_s:(Goal.goal sigma) -> evar_map -> Goal.goal -> Pp.t (** [pr_open_subgoals_diff ~quiet ~diffs ~oproof proof] shows the context for [proof] as used by, for example, coqtop. The first active goal is printed with all its antecedents and the conclusion. The other active goals only show their @@ -182,7 +181,7 @@ val pr_open_subgoals_diff : ?quiet:bool -> ?diffs:bool -> ?oproof:Proof.t -> Pr val pr_open_subgoals : proof:Proof.t -> Pp.t val pr_nth_open_subgoal : proof:Proof.t -> int -> Pp.t val pr_evar : evar_map -> (Evar.t * evar_info) -> Pp.t -val pr_evars_int : evar_map -> shelf:goal list -> givenup:goal list -> int -> evar_info Evar.Map.t -> Pp.t +val pr_evars_int : evar_map -> shelf:Goal.goal list -> givenup:Goal.goal list -> int -> evar_info Evar.Map.t -> Pp.t val pr_evars : evar_map -> evar_info Evar.Map.t -> Pp.t val pr_ne_evar_set : Pp.t -> Pp.t -> evar_map -> Evar.Set.t -> Pp.t diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli index 832393e15f..ce9ee5ae6f 100644 --- a/printing/proof_diffs.mli +++ b/printing/proof_diffs.mli @@ -16,7 +16,6 @@ val write_diffs_option : string -> unit val show_diffs : unit -> bool open Evd -open Proof_type open Environ open Constr @@ -31,7 +30,7 @@ If you want to make your call especially bulletproof, catch these exceptions, print a user-visible message, then recall this routine with the first argument set to None, which will skip the diff. *) -val diff_goal_ide : goal sigma option -> goal -> Evd.evar_map -> Pp.t list * Pp.t +val diff_goal_ide : Goal.goal sigma option -> Goal.goal -> Evd.evar_map -> Pp.t list * Pp.t (** Computes the diff between two goals @@ -43,7 +42,7 @@ If you want to make your call especially bulletproof, catch these exceptions, print a user-visible message, then recall this routine with the first argument set to None, which will skip the diff. *) -val diff_goal : ?og_s:(goal sigma) -> goal -> Evd.evar_map -> Pp.t +val diff_goal : ?og_s:(Goal.goal sigma) -> Goal.goal -> Evd.evar_map -> Pp.t (** Convert a string to a list of token strings using the lexer *) val tokenize_string : string -> string list @@ -53,7 +52,7 @@ val pr_leconstr_core : bool -> Environ.env -> Evd.evar_map -> EConstr.cons val pr_lconstr_env : env -> evar_map -> constr -> Pp.t (** Computes diffs for a single conclusion *) -val diff_concl : ?og_s:goal sigma -> Evd.evar_map -> Goal.goal -> Pp.t +val diff_concl : ?og_s:Goal.goal sigma -> Evd.evar_map -> Goal.goal -> Pp.t (** Generates a map from [np] to [op] that maps changed goals to their prior forms. The map doesn't include entries for unchanged goals; unchanged goals @@ -61,7 +60,7 @@ will have the same goal id in both versions. [op] and [np] must be from the same proof document and [op] must be for a state before [np]. *) -val make_goal_map : Proof.t option -> Proof.t -> Evar.t Evar.Map.t +val make_goal_map : Proof.t option -> Proof.t -> Goal.goal Evar.Map.t (* Exposed for unit test, don't use these otherwise *) (* output channel for the test log file *) diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index c7703b52c7..4720328893 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -16,7 +16,6 @@ open EConstr open Refiner open Logic open Reduction -open Tacmach open Clenv (* This function put casts around metavariables whose type could not be @@ -79,7 +78,7 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv = let clenv = { clenv with evd = evd' } in tclTHEN (tclEVARS (Evd.clear_metas evd')) - (refine_no_check (clenv_cast_meta clenv (clenv_value clenv))) gl + (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv)))) gl end let clenv_pose_dependent_evars ?(with_evars=false) clenv = diff --git a/proofs/logic.ml b/proofs/logic.ml index 4d5711c195..15ba0a704f 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -20,7 +20,6 @@ open Environ open Reductionops open Inductiveops open Typing -open Proof_type open Type_errors open Retyping @@ -62,6 +61,8 @@ let is_unification_error = function let catchable_exception = function | CErrors.UserError _ | TypeError _ + | Proof.OpenProof _ + (* abstract will call close_proof inside a tactic *) | Notation.NumeralNotationError _ | RefinerError _ | Indrec.RecursionSchemeError _ | Nametab.GlobalizationError _ @@ -583,12 +584,15 @@ let convert_hyp check sign sigma d = let prim_refiner r sigma goal = let env = Goal.V82.env sigma goal in let cl = Goal.V82.concl sigma goal in - match r with - (* Logical rules *) - | Refine c -> - let cl = EConstr.Unsafe.to_constr cl in - check_meta_variables env sigma c; - let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl c in - let sgl = List.rev sgl in - let sigma = Goal.V82.partial_solution env sigma goal (EConstr.of_constr oterm) in - (sgl, sigma) + let cl = EConstr.Unsafe.to_constr cl in + check_meta_variables env sigma r; + let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl r in + let sgl = List.rev sgl in + let sigma = Goal.V82.partial_solution env sigma goal (EConstr.of_constr oterm) in + (sgl, sigma) + +let prim_refiner ~check r sigma goal = + if check then + with_check (prim_refiner r sigma) goal + else + prim_refiner r sigma goal diff --git a/proofs/logic.mli b/proofs/logic.mli index 2cad278e10..f99076db23 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -13,27 +13,20 @@ open Names open Constr open Evd -open Proof_type -(** This suppresses check done in [prim_refiner] for the tactic given in - argument; works by side-effect *) - -val with_check : tactic -> tactic - -(** [without_check] respectively means:\\ - [Intro]: no check that the name does not exist\\ - [Intro_after]: no check that the name does not exist and that variables in +(** [check] respectively means:\\ + [Intro]: check that the name does not exist\\ + [Intro_after]: check that the name does not exist and that variables in its type does not escape their scope\\ - [Intro_replacing]: no check that the name does not exist and that + [Intro_replacing]: check that the name does not exist and that variables in its type does not escape their scope\\ [Convert_hyp]: - no check that the name exist and that its type is convertible\\ + check that the name exist and that its type is convertible\\ *) (** The primitive refiner. *) -val prim_refiner : prim_rule -> evar_map -> goal -> goal list * evar_map - +val prim_refiner : check:bool -> constr -> evar_map -> Goal.goal -> Goal.goal list * evar_map (** {6 Refiner errors. } *) diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 78080fa203..81122e6858 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -26,15 +26,6 @@ let _ = Goptions.declare_bool_option { let use_unification_heuristics () = !use_unification_heuristics_ref -let start_proof (id : Id.t) ?pl str sigma hyps c ?init_tac terminator = - let goals = [ (Global.env_of_context hyps , c) ] in - Proof_global.start_proof sigma id ?pl str goals terminator; - let env = Global.env () in - ignore (Proof_global.with_current_proof (fun _ p -> - match init_tac with - | None -> p,(true,[]) - | Some tac -> Proof.run_tactic env tac p)) - exception NoSuchGoal let _ = CErrors.register_handler begin function | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.") @@ -142,7 +133,8 @@ let next = let n = ref 0 in fun () -> incr n; !n let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac = let evd = Evd.from_ctx ctx in let terminator = Proof_global.make_terminator (fun _ -> ()) in - start_proof id goal_kind evd sign typ terminator; + let goals = [ (Global.env_of_context sign , typ) ] in + Proof_global.start_proof evd id goal_kind goals terminator; try let status = by tac in let open Proof_global in diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 76be7936b4..155221947a 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -16,19 +16,6 @@ open Environ open Decl_kinds (** {6 ... } *) -(** [start_proof s str env t hook tac] starts a proof of name [s] and - conclusion [t]; [hook] is optionally a function to be applied at - proof end (e.g. to declare the built constructions as a coercion - or a setoid morphism); init_tac is possibly a tactic to - systematically apply at initialization time (e.g. to start the - proof of mutually dependent theorems) *) - -val start_proof : - Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr -> - ?init_tac:unit Proofview.tactic -> - Proof_global.proof_terminator -> unit - -(** {6 ... } *) (** [get_goal_context n] returns the context of the [n]th subgoal of the current focused proof or raises a [UserError] if there is no focused proof or if there is no more subgoals *) diff --git a/proofs/proof.ml b/proofs/proof.ml index 8220949856..76a9a9f4c8 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -335,28 +335,42 @@ let dependent_start goals = let number_of_goals = List.length (Proofview.initial_goals pr.entry) in _focus end_of_stack (Obj.repr ()) 1 number_of_goals pr -exception UnfinishedProof -exception HasShelvedGoals -exception HasGivenUpGoals -exception HasUnresolvedEvar +type open_error_reason = + | UnfinishedProof + | HasShelvedGoals + | HasGivenUpGoals + | HasUnresolvedEvar + +let print_open_error_reason er = let open Pp in match er with + | UnfinishedProof -> + str "Attempt to save an incomplete proof" + | HasShelvedGoals -> + str "Attempt to save a proof with shelved goals" + | HasGivenUpGoals -> + strbrk "Attempt to save a proof with given up goals. If this is really what you want to do, use Admitted in place of Qed." + | HasUnresolvedEvar -> + strbrk "Attempt to save a proof with existential variables still non-instantiated" + +exception OpenProof of Names.Id.t option * open_error_reason + let _ = CErrors.register_handler begin function - | UnfinishedProof -> CErrors.user_err Pp.(str "Some goals have not been solved.") - | HasShelvedGoals -> CErrors.user_err Pp.(str "Some goals have been left on the shelf.") - | HasGivenUpGoals -> CErrors.user_err Pp.(str "Some goals have been given up.") - | HasUnresolvedEvar -> CErrors.user_err Pp.(str "Some existential variables are uninstantiated.") - | _ -> raise CErrors.Unhandled -end + | OpenProof (pid, reason) -> + let open Pp in + Option.cata (fun pid -> + str " (in proof " ++ Names.Id.print pid ++ str "): ") (mt()) pid ++ print_open_error_reason reason + | _ -> raise CErrors.Unhandled + end -let return p = +let return ?pid (p : t) = if not (is_done p) then - raise UnfinishedProof + raise (OpenProof(pid, UnfinishedProof)) else if has_shelved_goals p then - raise HasShelvedGoals + raise (OpenProof(pid, HasShelvedGoals)) else if has_given_up_goals p then - raise HasGivenUpGoals + raise (OpenProof(pid, HasGivenUpGoals)) else if has_unresolved_evar p then (* spiwack: for compatibility with <= 8.3 proof engine *) - raise HasUnresolvedEvar + raise (OpenProof(pid, HasUnresolvedEvar)) else let p = unfocus end_of_stack_kind p () in Proofview.return p.proofview @@ -449,11 +463,10 @@ module V82 = struct let grab_evars p = if not (is_done p) then - raise UnfinishedProof + raise (OpenProof(None, UnfinishedProof)) else { p with proofview = Proofview.V82.grab p.proofview } - (* Main component of vernac command Existential *) let instantiate_evar n com pr = let tac = diff --git a/proofs/proof.mli b/proofs/proof.mli index 8cf543557b..aaabea3454 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -89,11 +89,15 @@ val compact : t -> t Raises [HasShelvedGoals] if some goals are left on the shelf. Raises [HasGivenUpGoals] if some goals have been given up. Raises [HasUnresolvedEvar] if some evars have been left undefined. *) -exception UnfinishedProof -exception HasShelvedGoals -exception HasGivenUpGoals -exception HasUnresolvedEvar -val return : t -> Evd.evar_map +type open_error_reason = + | UnfinishedProof + | HasShelvedGoals + | HasGivenUpGoals + | HasUnresolvedEvar + +exception OpenProof of Names.Id.t option * open_error_reason + +val return : ?pid:Names.Id.t -> t -> Evd.evar_map (*** Focusing actions ***) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 25cf789193..cb4b5759dc 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -176,7 +176,6 @@ let simple_with_current_proof f = with_current_proof (fun t p -> f t p , ()) let compact_the_proof () = simple_with_current_proof (fun _ -> Proof.compact) - (* Sets the tactic to be used when a tactic line is closed with [...] *) let set_endline_tactic tac = match !pstates with @@ -416,20 +415,7 @@ let return_proof ?(allow_partial=false) () = proofs, Evd.evar_universe_context evd end else let initial_goals = Proof.initial_goals proof in - let evd = - let error s = - let prf = str " (in proof " ++ Id.print pid ++ str ")" in - raise (CErrors.UserError(Some "last tactic before Qed",s ++ prf)) - in - try Proof.return proof with - | Proof.UnfinishedProof -> - error(str"Attempt to save an incomplete proof") - | Proof.HasShelvedGoals -> - error(str"Attempt to save a proof with shelved goals") - | Proof.HasGivenUpGoals -> - error(strbrk"Attempt to save a proof with given up goals. If this is really what you want to do, use Admitted in place of Qed.") - | Proof.HasUnresolvedEvar-> - error(strbrk"Attempt to save a proof with existential variables still non-instantiated") in + let evd = Proof.return ~pid proof in let eff = Evd.eval_side_effects evd in let evd = Evd.minimize_universes evd in (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 2b04bfab57..e3808bc36d 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -60,14 +60,14 @@ type closed_proof = proof_object * proof_terminator val make_terminator : (proof_ending -> unit) -> proof_terminator val apply_terminator : proof_terminator -> proof_ending -> unit -(** [start_proof id str pl goals terminator] starts a proof of name [id] - with goals [goals] (a list of pairs of environment and - conclusion); [str] describes what kind of theorem/definition this - is (spiwack: for potential printing, I believe is used only by - closing commands and the xml plugin); [terminator] is used at the - end of the proof to close the proof. The proof is started in the - evar map [sigma] (which can typically contain universe - constraints), and with universe bindings pl. *) +(** [start_proof id str pl goals terminator] starts a proof of name + [id] with goals [goals] (a list of pairs of environment and + conclusion); [str] describes what kind of theorem/definition this + is; [terminator] is used at the end of the proof to close the proof + (e.g. to declare the built constructions as a coercion or a setoid + morphism). The proof is started in the evar map [sigma] (which can + typically contain universe constraints), and with universe bindings + pl. *) val start_proof : Evd.evar_map -> Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list -> diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml deleted file mode 100644 index 149f30c673..0000000000 --- a/proofs/proof_type.ml +++ /dev/null @@ -1,28 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** Legacy proof engine. Do not use in newly written code. *) - -open Evd -open Constr - -(** This module defines the structure of proof tree and the tactic type. So, it - is used by [Proof_tree] and [Refiner] *) - -type prim_rule = - | Refine of constr - -(** Nowadays, the only rules we'll consider are the primitive rules *) - -type rule = prim_rule - -type goal = Goal.goal - -type tactic = goal sigma -> goal list sigma diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 197f71ca91..dbd5be23ab 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -1,10 +1,9 @@ Miscprint Goal Evar_refiner -Proof_type -Logic Refine Proof +Logic Goal_select Proof_bullet Proof_global diff --git a/proofs/refiner.ml b/proofs/refiner.ml index be32aadd91..bce227dabb 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -12,9 +12,10 @@ open Pp open CErrors open Util open Evd -open Proof_type open Logic +type tactic = Proofview.V82.tac + module NamedDecl = Context.Named.Declaration let sig_it x = x.it @@ -25,16 +26,16 @@ let project x = x.sigma let pf_env gls = Global.env_of_context (Goal.V82.hyps (project gls) (sig_it gls)) let pf_hyps gls = EConstr.named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls)) -let refiner pr goal_sigma = - let (sgl,sigma') = prim_refiner pr goal_sigma.sigma goal_sigma.it in +let refiner ~check pr goal_sigma = + let (sgl,sigma') = prim_refiner ~check pr goal_sigma.sigma goal_sigma.it in { it = sgl; sigma = sigma'; } (* Profiling refiner *) -let refiner = +let refiner ~check = if Flags.profile then let refiner_key = CProfile.declare_profile "refiner" in - CProfile.profile2 refiner_key refiner - else refiner + CProfile.profile2 refiner_key (refiner ~check) + else refiner ~check (*********************) (* Tacticals *) @@ -178,9 +179,9 @@ let tclPROGRESS tac ptree = NOTE: some tactics delete hypothesis and reuse names (induction, destruct), this is not detected by this tactical. *) let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) - :Proof_type.goal list Evd.sigma = + : Goal.goal list Evd.sigma = let oldhyps = pf_hyps goal in - let rslt:Proof_type.goal list Evd.sigma = tac goal in + let rslt:Goal.goal list Evd.sigma = tac goal in let { it = gls; sigma = sigma; } = rslt in let hyps = List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 30af6d8e1a..52cbf7658b 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -11,18 +11,18 @@ (** Legacy proof engine. Do not use in newly written code. *) open Evd -open Proof_type open EConstr (** The refiner (handles primitive rules and high-level tactics). *) +type tactic = Proofview.V82.tac val sig_it : 'a sigma -> 'a val project : 'a sigma -> evar_map -val pf_env : goal sigma -> Environ.env -val pf_hyps : goal sigma -> named_context +val pf_env : Goal.goal sigma -> Environ.env +val pf_hyps : Goal.goal sigma -> named_context -val refiner : rule -> tactic +val refiner : check:bool -> Constr.t -> tactic (** {6 Tacticals. } *) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 231a8fe266..64d7630d55 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -17,9 +17,7 @@ open Evd open Typing open Redexpr open Tacred -open Proof_type open Logic -open Refiner open Context.Named.Declaration module NamedDecl = Context.Named.Declaration @@ -30,7 +28,7 @@ let re_sig it gc = { it = it; sigma = gc; } (* Operations for handling terms under a local typing context *) (**************************************************************) -type tactic = Proof_type.tactic +type tactic = Proofview.V82.tac let sig_it = Refiner.sig_it let project = Refiner.project @@ -103,20 +101,6 @@ let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind let pf_hnf_type_of gls = pf_get_type_of gls %> pf_whd_all gls -(********************************************) -(* Definition of the most primitive tactics *) -(********************************************) - -let refiner = refiner - -let refine_no_check c gl = - let c = EConstr.Unsafe.to_constr c in - refiner (Refine c) gl - -(* Versions with consistency checks *) - -let refine c = with_check (refine_no_check c) - (* Pretty-printers *) open Pp diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 14c83a6802..ef6a1544e4 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -12,85 +12,78 @@ open Names open Constr open Environ open EConstr -open Proof_type open Redexpr open Locus (** Operations for handling terms under a local typing context. *) open Evd -type tactic = Proof_type.tactic;; + +type tactic = Proofview.V82.tac val sig_it : 'a sigma -> 'a -val project : goal sigma -> evar_map +val project : Goal.goal sigma -> evar_map val re_sig : 'a -> evar_map -> 'a sigma -val pf_concl : goal sigma -> types -val pf_env : goal sigma -> env -val pf_hyps : goal sigma -> named_context -(*i val pf_untyped_hyps : goal sigma -> (Id.t * constr) list i*) -val pf_hyps_types : goal sigma -> (Id.t * types) list -val pf_nth_hyp_id : goal sigma -> int -> Id.t -val pf_last_hyp : goal sigma -> named_declaration -val pf_ids_of_hyps : goal sigma -> Id.t list -val pf_global : goal sigma -> Id.t -> evar_map * constr -val pf_unsafe_type_of : goal sigma -> constr -> types -val pf_type_of : goal sigma -> constr -> evar_map * types -val pf_hnf_type_of : goal sigma -> constr -> types +val pf_concl : Goal.goal sigma -> types +val pf_env : Goal.goal sigma -> env +val pf_hyps : Goal.goal sigma -> named_context +(*i val pf_untyped_hyps : Goal.goal sigma -> (Id.t * constr) list i*) +val pf_hyps_types : Goal.goal sigma -> (Id.t * types) list +val pf_nth_hyp_id : Goal.goal sigma -> int -> Id.t +val pf_last_hyp : Goal.goal sigma -> named_declaration +val pf_ids_of_hyps : Goal.goal sigma -> Id.t list +val pf_global : Goal.goal sigma -> Id.t -> evar_map * constr +val pf_unsafe_type_of : Goal.goal sigma -> constr -> types +val pf_type_of : Goal.goal sigma -> constr -> evar_map * types +val pf_hnf_type_of : Goal.goal sigma -> constr -> types -val pf_get_hyp : goal sigma -> Id.t -> named_declaration -val pf_get_hyp_typ : goal sigma -> Id.t -> types +val pf_get_hyp : Goal.goal sigma -> Id.t -> named_declaration +val pf_get_hyp_typ : Goal.goal sigma -> Id.t -> types -val pf_get_new_id : Id.t -> goal sigma -> Id.t +val pf_get_new_id : Id.t -> Goal.goal sigma -> Id.t -val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> evar_map * constr +val pf_reduction_of_red_expr : Goal.goal sigma -> red_expr -> constr -> evar_map * constr -val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a +val pf_apply : (env -> evar_map -> 'a) -> Goal.goal sigma -> 'a val pf_eapply : (env -> evar_map -> 'a -> evar_map * 'b) -> - goal sigma -> 'a -> goal sigma * 'b + Goal.goal sigma -> 'a -> Goal.goal sigma * 'b val pf_reduce : (env -> evar_map -> constr -> constr) -> - goal sigma -> constr -> constr + Goal.goal sigma -> constr -> constr val pf_e_reduce : (env -> evar_map -> constr -> evar_map * constr) -> - goal sigma -> constr -> evar_map * constr - -val pf_whd_all : goal sigma -> constr -> constr -val pf_hnf_constr : goal sigma -> constr -> constr -val pf_nf : goal sigma -> constr -> constr -val pf_nf_betaiota : goal sigma -> constr -> constr -val pf_reduce_to_quantified_ind : goal sigma -> types -> (inductive * EInstance.t) * types -val pf_reduce_to_atomic_ind : goal sigma -> types -> (inductive * EInstance.t) * types -val pf_compute : goal sigma -> constr -> constr + Goal.goal sigma -> constr -> evar_map * constr + +val pf_whd_all : Goal.goal sigma -> constr -> constr +val pf_hnf_constr : Goal.goal sigma -> constr -> constr +val pf_nf : Goal.goal sigma -> constr -> constr +val pf_nf_betaiota : Goal.goal sigma -> constr -> constr +val pf_reduce_to_quantified_ind : Goal.goal sigma -> types -> (inductive * EInstance.t) * types +val pf_reduce_to_atomic_ind : Goal.goal sigma -> types -> (inductive * EInstance.t) * types +val pf_compute : Goal.goal sigma -> constr -> constr val pf_unfoldn : (occurrences * evaluable_global_reference) list - -> goal sigma -> constr -> constr - -val pf_const_value : goal sigma -> pconstant -> constr -val pf_conv_x : goal sigma -> constr -> constr -> bool -val pf_conv_x_leq : goal sigma -> constr -> constr -> bool - -(** {6 The most primitive tactics. } *) - -val refiner : rule -> tactic -val refine_no_check : constr -> tactic + -> Goal.goal sigma -> constr -> constr -(** {6 The most primitive tactics with consistency and type checking } *) - -val refine : constr -> tactic +val pf_const_value : Goal.goal sigma -> pconstant -> constr +val pf_conv_x : Goal.goal sigma -> constr -> constr -> bool +val pf_conv_x_leq : Goal.goal sigma -> constr -> constr -> bool (** {6 Pretty-printing functions (debug only). } *) -val pr_gls : goal sigma -> Pp.t -val pr_glls : goal list sigma -> Pp.t +val pr_gls : Goal.goal sigma -> Pp.t +val pr_glls : Goal.goal list sigma -> Pp.t [@@ocaml.deprecated "Please move to \"new\" proof engine"] (** Variants of [Tacmach] functions built with the new proof engine *) module New : sig + val pf_apply : (env -> evar_map -> 'a) -> Proofview.Goal.t -> 'a val pf_global : Id.t -> Proofview.Goal.t -> GlobRef.t + (** FIXME: encapsulate the level in an existential type. *) - val of_old : (Proof_type.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a + val of_old : (Goal.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a val project : Proofview.Goal.t -> Evd.evar_map val pf_env : Proofview.Goal.t -> Environ.env diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 1bb33f2a23..5959dd54b1 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -358,7 +358,7 @@ let rec e_trivial_fail_db only_classes db_list local_db secvars = Eauto.registered_e_assumption :: (tclTHEN Tactics.intro trivial_fail :: [trivial_resolve]) in - tclFIRST (List.map tclCOMPLETE tacl) + tclSOLVE tacl and e_my_find_search db_list local_db secvars hdc complete only_classes env sigma concl = let open Proofview.Notations in diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 9a6bdab7b9..b8adb792e8 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -15,7 +15,6 @@ open Names open Constr open Termops open EConstr -open Proof_type open Tacticals open Tacmach open Evd @@ -151,7 +150,7 @@ let rec e_trivial_fail_db db_list local_db = (Tacticals.New.tclTHEN Tactics.intro next) :: (List.map fst (e_trivial_resolve (Tacmach.New.pf_env gl) (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_concl gl))) in - Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl) + Tacticals.New.tclSOLVE tacl end and e_my_find_search env sigma db_list local_db secvars hdc concl = @@ -203,7 +202,7 @@ let find_first_goal gls = type search_state = { priority : int; depth : int; (*r depth of search before failing *) - tacres : goal list sigma; + tacres : Goal.goal list sigma; last_tactic : Pp.t Lazy.t; dblist : hint_db list; localdb : hint_db list; diff --git a/tactics/eauto.mli b/tactics/eauto.mli index e161d88824..5aa2f42de1 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -26,7 +26,7 @@ val gen_eauto : ?debug:debug -> bool * int -> delayed_open_constr list -> val eauto_with_bases : ?debug:debug -> bool * int -> - delayed_open_constr list -> hint_db list -> Proof_type.tactic + delayed_open_constr list -> hint_db list -> Proofview.V82.tac val autounfold : hint_db_name list -> Locus.clause -> unit Proofview.tactic val autounfold_tac : hint_db_name list option -> Locus.clause -> unit Proofview.tactic diff --git a/tactics/equality.ml b/tactics/equality.ml index 969f539d1f..b8967775bf 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1028,7 +1028,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in let pf = Clenvtac.clenv_value_cast_meta absurd_clause in tclTHENS (assert_after Anonymous absurd_term) - [onLastHypId gen_absurdity; (Proofview.V82.tactic (Tacmach.refine pf))] + [onLastHypId gen_absurdity; (Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf)))] let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in @@ -1354,8 +1354,8 @@ let inject_if_homogenous_dependent_pair ty = tclTHENS (cut (mkApp (ceq,new_eq_args))) [clear [destVar sigma hyp]; Tacticals.New.pf_constr_of_global inj2 >>= fun inj2 -> - Proofview.V82.tactic (Tacmach.refine - (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|]))) + Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr + (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|])))) ])] with Exit -> Proofview.tclUNIT () @@ -1400,7 +1400,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = (Proofview.tclIGNORE (Proofview.Monad.List.map (fun (pf,ty) -> tclTHENS (cut ty) [inject_if_homogenous_dependent_pair ty; - Proofview.V82.tactic (Tacmach.refine pf)]) + Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf))]) (if l2r then List.rev injectors else injectors))) (tac (List.length injectors))) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index f2cf915fe3..224cd68cf9 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -26,6 +26,8 @@ module NamedDecl = Context.Named.Declaration (* Tacticals re-exported from the Refiner module *) (************************************************************************) +type tactic = Proofview.V82.tac + let tclIDTAC = Refiner.tclIDTAC let tclIDTAC_MESSAGE = Refiner.tclIDTAC_MESSAGE let tclORELSE0 = Refiner.tclORELSE0 diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index cc15469d0e..2947e44f7a 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -12,12 +12,13 @@ open Names open Constr open EConstr open Evd -open Proof_type open Locus open Tactypes (** Tacticals i.e. functions from tactics to tactics. *) +type tactic = Proofview.V82.tac + val tclIDTAC : tactic val tclIDTAC_MESSAGE : Pp.t -> tactic val tclORELSE0 : tactic -> tactic -> tactic @@ -65,20 +66,20 @@ val onNLastHypsId : int -> (Id.t list -> tactic) -> tactic val onNLastHyps : int -> (constr list -> tactic) -> tactic val onNLastDecls : int -> (named_context -> tactic) -> tactic -val lastHypId : goal sigma -> Id.t -val lastHyp : goal sigma -> constr -val lastDecl : goal sigma -> named_declaration -val nLastHypsId : int -> goal sigma -> Id.t list -val nLastHyps : int -> goal sigma -> constr list -val nLastDecls : int -> goal sigma -> named_context +val lastHypId : Goal.goal sigma -> Id.t +val lastHyp : Goal.goal sigma -> constr +val lastDecl : Goal.goal sigma -> named_declaration +val nLastHypsId : int -> Goal.goal sigma -> Id.t list +val nLastHyps : int -> Goal.goal sigma -> constr list +val nLastDecls : int -> Goal.goal sigma -> named_context -val afterHyp : Id.t -> goal sigma -> named_context +val afterHyp : Id.t -> Goal.goal sigma -> named_context val ifOnHyp : (Id.t * types -> bool) -> (Id.t -> tactic) -> (Id.t -> tactic) -> Id.t -> tactic -val onHyps : (goal sigma -> named_context) -> +val onHyps : (Goal.goal sigma -> named_context) -> (named_context -> tactic) -> tactic (** {6 Tacticals applying to goal components } *) @@ -127,11 +128,11 @@ val compute_constructor_signatures : rec_flag:bool -> inductive * 'a -> bool lis val compute_induction_names : bool list array -> or_and_intro_pattern option -> intro_patterns array -val elimination_sort_of_goal : goal sigma -> Sorts.family -val elimination_sort_of_hyp : Id.t -> goal sigma -> Sorts.family -val elimination_sort_of_clause : Id.t option -> goal sigma -> Sorts.family +val elimination_sort_of_goal : Goal.goal sigma -> Sorts.family +val elimination_sort_of_hyp : Id.t -> Goal.goal sigma -> Sorts.family +val elimination_sort_of_clause : Id.t option -> Goal.goal sigma -> Sorts.family -val pf_with_evars : (goal sigma -> Evd.evar_map * 'a) -> ('a -> tactic) -> tactic +val pf_with_evars : (Goal.goal sigma -> Evd.evar_map * 'a) -> ('a -> tactic) -> tactic val pf_constr_of_global : GlobRef.t -> (constr -> tactic) -> tactic (** Tacticals defined directly in term of Proofview *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 349cfce205..0beafb7e31 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -142,7 +142,6 @@ let introduction id = | _ -> raise (RefinerError (env, sigma, IntroNeedsProduct)) end -let refine = Tacmach.refine let error msg = CErrors.user_err Pp.(str msg) let convert_concl ?(check=true) ty k = @@ -1300,7 +1299,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) if not with_evars && occur_meta clenv.evd new_hyp_typ then error_uninstantiated_metas new_hyp_typ clenv; let new_hyp_prf = clenv_value clenv in - let exact_tac = Proofview.V82.tactic (Tacmach.refine_no_check new_hyp_prf) in + let exact_tac = Proofview.V82.tactic (Refiner.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf)) in let naming = NamingMustBe (CAst.make targetid) in let with_clear = do_replace (Some id) naming in Tacticals.New.tclTHEN @@ -1624,7 +1623,7 @@ let descend_in_conjunctions avoid tac (err, info) c = | Some (p,pt) -> Tacticals.New.tclTHENS (assert_before_gen false (NamingAvoid avoid) pt) - [Proofview.V82.tactic (refine p); + [Proofview.V82.tactic (refiner ~check:true EConstr.Unsafe.(to_constr p)); (* Might be ill-typed due to forbidden elimination. *) Tacticals.New.onLastHypId (tac (not isrec))] end))) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 4e91a9a728..75b5caaa36 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -12,7 +12,6 @@ open Names open Constr open EConstr open Environ -open Proof_type open Evd open Clenv open Redexpr @@ -50,8 +49,8 @@ val convert_leq : constr -> constr -> unit Proofview.tactic (** {6 Introduction tactics. } *) val fresh_id_in_env : Id.Set.t -> Id.t -> env -> Id.t -val fresh_id : Id.Set.t -> Id.t -> goal sigma -> Id.t -val find_intro_names : rel_context -> goal sigma -> Id.t list +val fresh_id : Id.Set.t -> Id.t -> Goal.goal sigma -> Id.t +val find_intro_names : rel_context -> Goal.goal sigma -> Id.t list val intro : unit Proofview.tactic val introf : unit Proofview.tactic diff --git a/test-suite/Makefile b/test-suite/Makefile index 928a77cb8e..1db97f43c5 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -187,14 +187,6 @@ summary.log: $(SHOW) BUILDING SUMMARY FILE $(HIDE)$(MAKE) --quiet summary > "$@" -# if not on travis we can get the log files (they're just there for a -# local build, and downloadable on GitLab) -PRINT_LOGS?= -TRAVIS?= # special because we want to print travis_fold directives -ifdef APPVEYOR -PRINT_LOGS:=APPVEYOR -endif #APPVEYOR - report: summary.log $(HIDE)bash report.sh diff --git a/test-suite/bugs/closed/gh6165.v b/test-suite/bugs/closed/bug_6165.v index b87a7caaf2..b87a7caaf2 100644 --- a/test-suite/bugs/closed/gh6165.v +++ b/test-suite/bugs/closed/bug_6165.v diff --git a/test-suite/bugs/closed/gh6384.v b/test-suite/bugs/closed/bug_6384.v index cec84642fb..cec84642fb 100644 --- a/test-suite/bugs/closed/gh6384.v +++ b/test-suite/bugs/closed/bug_6384.v diff --git a/test-suite/bugs/closed/gh6385.v b/test-suite/bugs/closed/bug_6385.v index 3bbb664f4f..3bbb664f4f 100644 --- a/test-suite/bugs/closed/gh6385.v +++ b/test-suite/bugs/closed/bug_6385.v diff --git a/test-suite/report.sh b/test-suite/report.sh index 05f39b4b02..c5e698232f 100755 --- a/test-suite/report.sh +++ b/test-suite/report.sh @@ -24,7 +24,7 @@ cp summary.log "$SAVEDIR"/ rm "$FAILED" # print info -if [ -n "$TRAVIS" ] || [ -n "$PRINT_LOGS" ]; then +if [ -n "$TRAVIS" ] || [ -n "$APPVEYOR" ] || [ -n "$PRINT_LOGS" ]; then find logs/ -name '*.log' -not -name 'summary.log' -print0 | while IFS= read -r -d '' file; do if [ -n "$TRAVIS" ]; then # ${foo////.} replaces every / by . in $foo @@ -40,12 +40,13 @@ if [ -n "$TRAVIS" ] || [ -n "$PRINT_LOGS" ]; then else printf '\n' fi done + printed_logs=1 fi if grep -q -F 'Error!' summary.log ; then echo FAILURES; grep -F 'Error!' summary.log; - if [ -z "$TRAVIS" ] && [ -z "$PRINT_LOGS" ]; then + if [ -z "$printed_logs" ]; then echo 'To print details of failed tests, rerun with environment variable PRINT_LOGS=1' echo 'eg "make report PRINT_LOGS=1" from the test suite directory"' echo 'See README.md in the test suite directory for more information.' diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 4e847a5590..de020926f6 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -331,7 +331,7 @@ let initialize_named_context_for_proof () = let d = if variable_opacity id then NamedDecl.LocalAssum (id, NamedDecl.get_type d) else d in Environ.push_named_context_val d signv) sign Environ.empty_named_context_val -let start_proof id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook = +let start_proof id ?pl kind sigma ?terminator ?sign c ?(compute_guard=[]) hook = let terminator = match terminator with | None -> standard_proof_terminator compute_guard hook | Some terminator -> terminator compute_guard hook @@ -341,19 +341,21 @@ let start_proof id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard= | Some sign -> sign | None -> initialize_named_context_for_proof () in - Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator + let goals = [ Global.env_of_context sign , c ] in + Proof_global.start_proof sigma id ?pl kind goals terminator -let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook = +let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?(compute_guard=[]) hook = let terminator = match terminator with | None -> universe_proof_terminator compute_guard hook | Some terminator -> terminator compute_guard hook in - let sign = + let sign = match sign with | Some sign -> sign | None -> initialize_named_context_for_proof () in - Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator + let goals = [ Global.env_of_context sign , c ] in + Proof_global.start_proof sigma id ?pl kind goals terminator let rec_tac_initializer finite guard thms snl = if finite then @@ -404,7 +406,11 @@ let start_proof_with_initialization kind sigma decl recguard thms snl hook = List.iter (fun (strength,ref,imps) -> maybe_declare_manual_implicits false ref imps; call_hook (fun exn -> exn) hook strength ref) thms_data in - start_proof_univs id ~pl:decl kind sigma t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard + start_proof_univs id ~pl:decl kind sigma t (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard; + ignore (Proof_global.with_current_proof (fun _ p -> + match init_tac with + | None -> p,(true,[]) + | Some tac -> Proof.run_tactic Global.(env ()) tac p)) let start_proof_com ?inference_hook kind thms hook = let env0 = Global.env () in diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 195fcbf4ca..246d8cbe6d 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -18,13 +18,13 @@ val call_hook : Future.fix_exn -> declaration_hook -> Decl_kinds.locality -> Glo val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> ?terminator:(Proof_global.lemma_possible_guards -> declaration_hook -> Proof_global.proof_terminator) -> ?sign:Environ.named_context_val -> EConstr.types -> - ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> + ?compute_guard:Proof_global.lemma_possible_guards -> declaration_hook -> unit val start_proof_univs : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> ?terminator:(Proof_global.lemma_possible_guards -> (UState.t option -> declaration_hook) -> Proof_global.proof_terminator) -> ?sign:Environ.named_context_val -> EConstr.types -> - ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> + ?compute_guard:Proof_global.lemma_possible_guards -> (UState.t option -> declaration_hook) -> unit val start_proof_com : diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 746db61cc3..8baf391c70 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -826,18 +826,34 @@ let rec string_of_list sep f = function | x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl (* Solve an obligation using tactics, return the corresponding proof term *) +let warn_solve_errored = CWarnings.create ~name:"solve_obligation_error" ~category:"tactics" (fun err -> + Pp.seq [str "Solve Obligations tactic returned error: "; err; fnl (); + str "This will become an error in the future"]) -let solve_by_tac name evi t poly ctx = +let solve_by_tac ?loc name evi t poly ctx = let id = name in (* spiwack: the status is dropped. *) - let (entry,_,ctx') = Pfedit.build_constant_by_tactic - id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps evi.evar_concl (Tacticals.New.tclCOMPLETE t) in - let env = Global.env () in - let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in - let body, () = Future.force entry.const_entry_body in - let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in - Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body)); - (fst body), entry.const_entry_type, Evd.evar_universe_context ctx' + try + let (entry,_,ctx') = + Pfedit.build_constant_by_tactic + id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps evi.evar_concl t in + let env = Global.env () in + let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in + let body, () = Future.force entry.const_entry_body in + let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in + Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body)); + Some (fst body, entry.const_entry_type, Evd.evar_universe_context ctx') + with + | Refiner.FailError (_, s) as exn -> + let _ = CErrors.push exn in + user_err ?loc ~hdr:"solve_obligation" (Lazy.force s) + (* If the proof is open we absorb the error and leave the obligation open *) + | Proof.OpenProof _ -> + None + | e when CErrors.noncritical e -> + let err = CErrors.print e in + warn_solve_errored ?loc err; + None let obligation_terminator name num guard hook auto pf = let open Proof_global in @@ -989,41 +1005,34 @@ and solve_obligation_by_tac prg obls i tac = match obl.obl_body with | Some _ -> None | None -> - try - if List.is_empty (deps_remaining obls obl.obl_deps) then - let obl = subst_deps_obl obls obl in - let tac = - match tac with - | Some t -> t - | None -> - match obl.obl_tac with - | Some t -> t - | None -> !default_tactic - in - let evd = Evd.from_ctx prg.prg_ctx in - let evd = Evd.update_sigma_env evd (Global.env ()) in - let t, ty, ctx = - solve_by_tac obl.obl_name (evar_of_obligation obl) tac - (pi2 prg.prg_kind) (Evd.evar_universe_context evd) - in - let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in - let prg = {prg with prg_ctx = ctx} in - let def, obl' = declare_obligation prg obl t ty uctx in - obls.(i) <- obl'; - if def && not (pi2 prg.prg_kind) then ( - (* Declare the term constraints with the first obligation only *) - let evd = Evd.from_env (Global.env ()) in - let evd = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx)) in - let ctx' = Evd.evar_universe_context evd in - Some {prg with prg_ctx = ctx'}) - else Some prg - else None - with e when CErrors.noncritical e -> - let (e, _) = CErrors.push e in - match e with - | Refiner.FailError (_, s) -> - user_err ?loc:(fst obl.obl_location) ~hdr:"solve_obligation" (Lazy.force s) - | e -> None (* FIXME really ? *) + if List.is_empty (deps_remaining obls obl.obl_deps) then + let obl = subst_deps_obl obls obl in + let tac = + match tac with + | Some t -> t + | None -> + match obl.obl_tac with + | Some t -> t + | None -> !default_tactic + in + let evd = Evd.from_ctx prg.prg_ctx in + let evd = Evd.update_sigma_env evd (Global.env ()) in + match solve_by_tac ?loc:(fst obl.obl_location) obl.obl_name (evar_of_obligation obl) tac + (pi2 prg.prg_kind) (Evd.evar_universe_context evd) with + | None -> None + | Some (t, ty, ctx) -> + let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in + let prg = {prg with prg_ctx = ctx} in + let def, obl' = declare_obligation prg obl t ty uctx in + obls.(i) <- obl'; + if def && not (pi2 prg.prg_kind) then ( + (* Declare the term constraints with the first obligation only *) + let evd = Evd.from_env (Global.env ()) in + let evd = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx)) in + let ctx' = Evd.evar_universe_context evd in + Some {prg with prg_ctx = ctx'}) + else Some prg + else None and solve_prg_obligations prg ?oblset tac = let obls, rem = prg.prg_obligations in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index df4193f397..a78329ad1d 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -489,8 +489,7 @@ let start_proof_and_print k l hook = Evarutil.is_ground_term sigma concl) then raise Exit; let c, _, ctx = - Pfedit.build_by_tactic env (Evd.evar_universe_context sigma) - concl (Tacticals.New.tclCOMPLETE tac) + Pfedit.build_by_tactic env (Evd.evar_universe_context sigma) concl tac in Evd.set_universe_context sigma ctx, EConstr.of_constr c with Logic_monad.TacticFailure e when Logic.catchable_exception e -> user_err Pp.(str "The statement obligations could not be resolved \ |