diff options
34 files changed, 206 insertions, 181 deletions
diff --git a/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh b/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh new file mode 100644 index 0000000000..4032b1c6b5 --- /dev/null +++ b/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10125" ] || [ "$CI_BRANCH" = "run_tactic_gen" ]; then + + paramcoq_CI_REF=run_tactic_gen + paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq + +fi diff --git a/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh b/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh new file mode 100644 index 0000000000..bc8aa33565 --- /dev/null +++ b/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10135" ] || [ "$CI_BRANCH" = "detype-anonymous" ]; then + + unicoq_CI_REF=detype-anonymous + unicoq_CI_GITURL=https://github.com/maximedenes/unicoq + +fi diff --git a/dev/include_printers b/dev/include_printers index 90088e40bf..d077075eeb 100644 --- a/dev/include_printers +++ b/dev/include_printers @@ -11,6 +11,7 @@ #install_printer (* universes *) ppuniverses;; #install_printer (* univ level *) ppuni_level;; #install_printer (* univ context *) ppuniverse_context;; +#install_printer (* univ context *) ppaucontext;; #install_printer (* univ context future *) ppuniverse_context_future;; #install_printer (* univ context set *) ppuniverse_context_set;; #install_printer (* univ set *) ppuniverse_set;; diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg index a6ecec7e33..82f2e79549 100644 --- a/dev/top_printers.dbg +++ b/dev/top_printers.dbg @@ -62,6 +62,7 @@ install_printer Top_printers.ppuni_level install_printer Top_printers.ppuniverse_set install_printer Top_printers.ppuniverse_instance install_printer Top_printers.ppuniverse_context +install_printer Top_printers.ppaucontext install_printer Top_printers.ppuniverse_context_set install_printer Top_printers.ppuniverse_subst install_printer Top_printers.ppuniverse_opt_subst diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 816316487c..2859b56cbe 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -27,7 +27,6 @@ open Clenv let _ = Detyping.print_evar_arguments := true let _ = Detyping.print_universes := true let _ = Goptions.set_bool_option_value ["Printing";"Matching"] false -let _ = Detyping.set_detype_anonymous (fun ?loc _ -> raise Not_found) (* std_ppcmds *) let pp x = Pp.pp_with !Topfmt.std_ft x @@ -236,6 +235,15 @@ let ppnamedcontextval e = let sigma = Evd.from_env env in pp (pr_named_context env sigma (named_context_of_val e)) +let ppaucontext auctx = + let nas = AUContext.names auctx in + let prlev l = match Level.var_index l with + | Some n -> Name.print nas.(n) + | None -> prlev l + in + pp (pr_universe_context prlev (AUContext.repr auctx)) + + let ppenv e = pp (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++ str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]") diff --git a/dev/top_printers.mli b/dev/top_printers.mli index cb32d2294c..2aa1808322 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -137,6 +137,7 @@ val prlev : Univ.Level.t -> Pp.t (* with global names (does this work?) *) val ppuniverse_set : Univ.LSet.t -> unit val ppuniverse_instance : Univ.Instance.t -> unit val ppuniverse_context : Univ.UContext.t -> unit +val ppaucontext : Univ.AUContext.t -> unit val ppuniverse_context_set : Univ.ContextSet.t -> unit val ppuniverse_subst : Univ.universe_subst -> unit val ppuniverse_opt_subst : UnivSubst.universe_opt_subst -> unit diff --git a/doc/changelog/03-notations/10061-print-custom-grammar.rst b/doc/changelog/03-notations/10061-print-custom-grammar.rst deleted file mode 100644 index 8786c7ce6b..0000000000 --- a/doc/changelog/03-notations/10061-print-custom-grammar.rst +++ /dev/null @@ -1,4 +0,0 @@ -- Allow inspecting custom grammar entries by :cmd:`Print Custom Grammar` - (`#10061 <https://github.com/coq/coq/pull/10061>`_, - fixes `#9681 <http://github.com/coq/coq/pull/9681>`_, - by Jasper Hugunin, review by Pierre-Marie Pédrot and Hugo Herbelin). diff --git a/doc/changelog/04-tactics/09996-hint-mode.rst b/doc/changelog/04-tactics/09996-hint-mode.rst deleted file mode 100644 index 06e9059b45..0000000000 --- a/doc/changelog/04-tactics/09996-hint-mode.rst +++ /dev/null @@ -1,5 +0,0 @@ -- Modes are now taken into account by :tacn:`typeclasses eauto` for - local hypotheses - (`#9996 <https://github.com/coq/coq/pull/9996>`_, - fixes `#5752 <https://github.com/coq/coq/issues/5752>`_, - by Maxime Dénès, review by Pierre-Marie Pédrot). diff --git a/doc/changelog/04-tactics/10059-change-no-check.rst b/doc/changelog/04-tactics/10059-change-no-check.rst deleted file mode 100644 index 987b2a8ccd..0000000000 --- a/doc/changelog/04-tactics/10059-change-no-check.rst +++ /dev/null @@ -1,7 +0,0 @@ -- New variant :tacn:`change_no_check` of :tacn:`change`, usable as a - documented replacement of :tacn:`convert_concl_no_check` - (`#10012 <https://github.com/coq/coq/pull/10012>`_, - `#10017 <https://github.com/coq/coq/pull/10017>`_, - `#10053 <https://github.com/coq/coq/pull/10053>`_, and - `#10059 <https://github.com/coq/coq/pull/10059>`_, - by Hugo Herbelin and Paolo G. Giarrusso). diff --git a/doc/changelog/06-ssreflect/09995-notations.rst b/doc/changelog/06-ssreflect/09995-notations.rst deleted file mode 100644 index 3dfc45242d..0000000000 --- a/doc/changelog/06-ssreflect/09995-notations.rst +++ /dev/null @@ -1,8 +0,0 @@ -- `inE` now expands `y \in r x` when `r` is a `simpl_rel`. - New `{pred T}` notation for a `pred T` alias in the `pred_sort` coercion - class, simplified `predType` interface: `pred_class` and `mkPredType` - deprecated, `{pred T}` and `PredType` should be used instead. - `if c return t then ...` now expects `c` to be a variable bound in `t`. - New `nonPropType` interface matching types that do _not_ have sort `Prop`. - New `relpre R f` definition for the preimage of a relation R under f - (`#9995 <https://github.com/coq/coq/pull/9995>`_, by Georges Gonthier). diff --git a/doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst b/doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst deleted file mode 100644 index 732c088f45..0000000000 --- a/doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst +++ /dev/null @@ -1,3 +0,0 @@ -- Added :g:`Coq.Structures.EqualitiesFacts.PairUsualDecidableTypeFull` - (`#9984 <https://github.com/coq/coq/pull/9984>`_, - by Jean-Christophe Léchenet and Oliver Nash). diff --git a/doc/changelog/12-misc/09964-changes.rst b/doc/changelog/12-misc/09964-changes.rst deleted file mode 100644 index dd873cfdd5..0000000000 --- a/doc/changelog/12-misc/09964-changes.rst +++ /dev/null @@ -1,14 +0,0 @@ -- Changelog has been moved from a specific file `CHANGES.md` to the - reference manual; former Credits chapter of the reference manual has - been split in two parts: a History chapter which was enriched with - additional historical information about Coq versions 1 to 5, and a - Changes chapter which was enriched with the content formerly in - `CHANGES.md` and `COMPATIBILITY` - (`#9133 <https://github.com/coq/coq/pull/9133>`_, - `#9668 <https://github.com/coq/coq/pull/9668>`_, - `#9939 <https://github.com/coq/coq/pull/9939>`_, - `#9964 <https://github.com/coq/coq/pull/9964>`_, - and `#10085 <https://github.com/coq/coq/pull/10085>`_, - by Théo Zimmermann, - with help and ideas from Emilio Jesús Gallego Arias, Gaëtan - Gilbert, Clément Pit-Claudel, Matthieu Sozeau, and Enrico Tassi). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 574b943a78..cca3b2e06b 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -355,6 +355,11 @@ Other changes in 8.10+beta1 that will do it automatically, using the output of ``coqc`` (`#8638 <https://github.com/coq/coq/pull/8638>`_, by Jason Gross). + - Allow inspecting custom grammar entries by :cmd:`Print Custom Grammar` + (`#10061 <https://github.com/coq/coq/pull/10061>`_, + fixes `#9681 <http://github.com/coq/coq/pull/9681>`_, + by Jasper Hugunin, review by Pierre-Marie Pédrot and Hugo Herbelin). + - The `quote plugin <https://coq.inria.fr/distrib/V8.9.0/refman/proof-engine/detailed-tactic-examples.html#quote>`_ was removed. If some users are interested in maintaining this plugin @@ -400,7 +405,32 @@ Other changes in 8.10+beta1 closes `#7632 <https://github.com/coq/coq/issues/7632>`_, by Théo Zimmermann). - - SSReflect clear discipline made consistent across the entire proof language. + - Modes are now taken into account by :tacn:`typeclasses eauto` for + local hypotheses + (`#9996 <https://github.com/coq/coq/pull/9996>`_, + fixes `#5752 <https://github.com/coq/coq/issues/5752>`_, + by Maxime Dénès, review by Pierre-Marie Pédrot). + + - New variant :tacn:`change_no_check` of :tacn:`change`, usable as a + documented replacement of :tacn:`convert_concl_no_check` + (`#10012 <https://github.com/coq/coq/pull/10012>`_, + `#10017 <https://github.com/coq/coq/pull/10017>`_, + `#10053 <https://github.com/coq/coq/pull/10053>`_, and + `#10059 <https://github.com/coq/coq/pull/10059>`_, + by Hugo Herbelin and Paolo G. Giarrusso). + + - The simplified value returned by :tacn:`field_simplify` is not + always a fraction anymore. When the denominator is :g:`1`, it + returns :g:`x` while previously it was returning :g:`x/1`. This + change could break codes that were post-processing application of + :tacn:`field_simplify` to get rid of these :g:`x/1` + (`#9854 <https://github.com/coq/coq/pull/9854>`_, + by Laurent Théry, + with help from Michael Soegtrop, Maxime Dénès, and Vincent Laporte). + +- SSReflect: + + - Clear discipline made consistent across the entire proof language. Whenever a clear switch `{x..}` comes immediately before an existing proof context entry (used as a view, as a rewrite rule or as name for a new context entry) then such entry is cleared too. @@ -414,6 +444,15 @@ Other changes in 8.10+beta1 (`#9341 <https://github.com/coq/coq/pull/9341>`_, by Enrico Tassi). + - `inE` now expands `y \in r x` when `r` is a `simpl_rel`. + New `{pred T}` notation for a `pred T` alias in the `pred_sort` coercion + class, simplified `predType` interface: `pred_class` and `mkPredType` + deprecated, `{pred T}` and `PredType` should be used instead. + `if c return t then ...` now expects `c` to be a variable bound in `t`. + New `nonPropType` interface matching types that do _not_ have sort `Prop`. + New `relpre R f` definition for the preimage of a relation R under f + (`#9995 <https://github.com/coq/coq/pull/9995>`_, by Georges Gonthier). + - Vernacular commands: - Binders for an :cmd:`Instance` now act more like binders for a :cmd:`Theorem`. @@ -535,10 +574,28 @@ Other changes in 8.10+beta1 `fset` database (`#9725 <https://github.com/coq/coq/pull/9725>`_, by Frédéric Besson). + - Added :g:`Coq.Structures.EqualitiesFacts.PairUsualDecidableTypeFull` + (`#9984 <https://github.com/coq/coq/pull/9984>`_, + by Jean-Christophe Léchenet and Oliver Nash). + - Some error messages that show problems with a pair of non-matching values will now highlight the differences (`#8669 <https://github.com/coq/coq/pull/8669>`_, by Jim Fehrle). +- Changelog has been moved from a specific file `CHANGES.md` to the + reference manual; former Credits chapter of the reference manual has + been split in two parts: a History chapter which was enriched with + additional historical information about Coq versions 1 to 5, and a + Changes chapter which was enriched with the content formerly in + `CHANGES.md` and `COMPATIBILITY` + (`#9133 <https://github.com/coq/coq/pull/9133>`_, + `#9668 <https://github.com/coq/coq/pull/9668>`_, + `#9939 <https://github.com/coq/coq/pull/9939>`_, + `#9964 <https://github.com/coq/coq/pull/9964>`_, + and `#10085 <https://github.com/coq/coq/pull/10085>`_, + by Théo Zimmermann, + with help and ideas from Emilio Jesús Gallego Arias, Gaëtan + Gilbert, Clément Pit-Claudel, Matthieu Sozeau, and Enrico Tassi). Version 8.9 ----------- diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 4425e41652..4769c2dc53 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -102,6 +102,7 @@ let start_deriving f suchthat lemma = let terminator = Proof_global.make_terminator terminator in let pstate = Proof_global.start_dependent_proof ~ontop:None lemma kind goals terminator in - fst @@ Proof_global.with_current_proof begin fun _ p -> - Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p + Proof_global.simple_with_current_proof begin fun _ p -> + let p,_,() = Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p in + p end pstate diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 062e3ca8b2..82726eccf0 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -708,9 +708,6 @@ type binder_kind = BProd | BLambda | BLetIn (**********************************************************************) (* Main detyping function *) -let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable.")) -let set_detype_anonymous f = detype_anonymous := f - let detype_level sigma l = let l = hack_qualid_of_univ_level sigma l in GType (UNamed l) @@ -732,11 +729,13 @@ and detype_r d flags avoid env sigma t = match EConstr.kind sigma (collapse_appl sigma t) with | Rel n -> (try match lookup_name_of_rel n (fst env) with - | Name id -> GVar id - | Anonymous -> GVar (!detype_anonymous n) + | Name id -> GVar id + | Anonymous -> + let s = "_ANONYMOUS_REL_"^(string_of_int n) in + GVar (Id.of_string s) with Not_found -> - let s = "_UNBOUND_REL_"^(string_of_int n) - in GVar (Id.of_string s)) + let s = "_UNBOUND_REL_"^(string_of_int n) + in GVar (Id.of_string s)) | Meta n -> (* Meta in constr are not user-parsable and are mapped to Evar *) if n = Constr_matching.special_meta then diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 1a8e97efb8..00b0578a52 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -68,9 +68,6 @@ val detype_closed_glob : ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> clo val lookup_name_as_displayed : env -> evar_map -> constr -> Id.t -> int option val lookup_index_as_renamed : env -> evar_map -> constr -> int -> int option -(* XXX: This is a hack and should go away *) -val set_detype_anonymous : (?loc:Loc.t -> int -> Id.t) -> unit - val force_wildcard : unit -> bool val synthetize_type : unit -> bool diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 4f36354f79..52e15f466f 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -98,7 +98,7 @@ let solve ?with_end_tac gi info_lvl tac pr = else tac in let env = Global.env () in - let (p,(status,info)) = Proof.run_tactic env tac pr in + let (p,(status,info),()) = Proof.run_tactic env tac pr in let env = Global.env () in let sigma = Evd.from_env env in let () = @@ -161,7 +161,7 @@ let refine_by_tactic ~name ~poly env sigma ty tac = let prev_future_goals = save_future_goals sigma in (* Start a proof *) let prf = Proof.start ~name ~poly sigma [env, ty] in - let (prf, _) = + let (prf, _, ()) = try Proof.run_tactic env tac prf with Logic_monad.TacticFailure e as src -> (* Catch the inner error of the monad tactic *) diff --git a/proofs/proof.ml b/proofs/proof.ml index 567012c15f..09e4e898fe 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -372,7 +372,7 @@ let run_tactic env tac pr = let sp = pr.proofview in let undef sigma l = List.filter (fun g -> Evd.is_undefined sigma g) l in let tac = - tac >>= fun () -> + tac >>= fun result -> Proofview.tclEVARMAP >>= fun sigma -> (* Already solved goals are not to be counted as shelved. Nor are they to be marked as unresolvable. *) @@ -383,10 +383,10 @@ let run_tactic env tac pr = CErrors.anomaly Pp.(str "Evars generated outside of proof engine (e.g. V82, clear, ...) are not supposed to be explicitly given up."); let sigma = Proofview.Unsafe.mark_as_goals sigma retrieved in Proofview.Unsafe.tclEVARS sigma >>= fun () -> - Proofview.tclUNIT retrieved + Proofview.tclUNIT (result,retrieved) in let { name; poly } = pr in - let (retrieved,proofview,(status,to_shelve,give_up),info_trace) = + let ((result,retrieved),proofview,(status,to_shelve,give_up),info_trace) = Proofview.apply ~name ~poly env tac sp in let sigma = Proofview.return proofview in @@ -400,7 +400,7 @@ let run_tactic env tac pr = in let given_up = pr.given_up@give_up in let proofview = Proofview.Unsafe.reset_future_goals proofview in - { pr with proofview ; shelf ; given_up },(status,info_trace) + { pr with proofview ; shelf ; given_up },(status,info_trace),result (*** Commands ***) diff --git a/proofs/proof.mli b/proofs/proof.mli index 1f4748141a..248b9d921e 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -172,7 +172,7 @@ val no_focused_goal : t -> bool used. In which case it is [false]. *) val run_tactic : Environ.env - -> unit Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree) + -> 'a Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree) * 'a val maximal_unfocus : 'a focus_kind -> t -> t diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 08b98d702a..40ae4acc88 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -345,6 +345,6 @@ let update_global_env (pf : t) = with_current_proof (fun _ p -> Proof.in_proof p (fun sigma -> let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in - let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac p in + let (p,(status,info),()) = Proof.run_tactic (Global.env ()) tac p in (p, ()))) pf in res diff --git a/stm/stm.ml b/stm/stm.ml index 3eb6d03529..21618bc044 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2085,8 +2085,8 @@ end = struct (* {{{ *) let st = Vernacstate.freeze_interp_state ~marshallable:false in stm_fail ~st fail (fun () -> (if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () -> - ignore(TaskQueue.with_n_workers nworkers (fun queue -> - PG_compat.with_current_proof (fun _ p -> + TaskQueue.with_n_workers nworkers (fun queue -> + PG_compat.simple_with_current_proof (fun _ p -> let Proof.{goals} = Proof.data p in let open TacTask in let res = CList.map_i (fun i g -> @@ -2131,7 +2131,8 @@ end = struct (* {{{ *) if solve then Tacticals.New.tclSOLVE [] else tclUNIT () end) in - Proof.run_tactic (Global.env()) assign_tac p)))) ()) + let p,_,() = Proof.run_tactic (Global.env()) assign_tac p in + p))) ()) end (* }}} *) diff --git a/tactics/equality.ml b/tactics/equality.ml index f049f8c568..45a4799ea1 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -417,7 +417,7 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars d find_elim hdcncl lft2rgt dep cls (Some t) >>= fun elim -> general_elim_clause with_evars frzevars tac cls c t l (match lft2rgt with None -> false | Some b -> b) - {elimindex = None; elimbody = (elim,NoBindings); elimrename = None} + {elimindex = None; elimbody = (elim,NoBindings) } end let adjust_rewriting_direction args lft2rgt = diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 4aa4d13e1e..6efa1ece9c 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -204,10 +204,7 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op = (str"Computed inversion goal was not closed in initial signature."); *) let pf = Proof.start ~name ~poly (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in - let pf = - fst (Proof.run_tactic env ( - tclTHEN intro (onLastHypId inv_op)) pf) - in + let pf, _, () = Proof.run_tactic env (tclTHEN intro (onLastHypId inv_op)) pf in let pfterm = List.hd (Proof.partial_proof pf) in let global_named_context = Global.named_context_val () in let ownSign = ref begin diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 806c955591..2bdfc85d6d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1302,14 +1302,11 @@ let do_replace id = function [Ti] and the first one (resp last one) being [G] whose hypothesis [id] is replaced by P using the proof given by [tac] *) -let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) - targetid id sigma0 clenv tac = +let clenv_refine_in with_evars targetid id sigma0 clenv tac = let clenv = Clenvtac.clenv_pose_dependent_evars ~with_evars clenv in let clenv = - if with_classes then { clenv with evd = Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd } - else clenv in let new_hyp_typ = clenv_type clenv in if not with_evars then check_unresolved_evars_of_metas sigma0 clenv; @@ -1321,11 +1318,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) let with_clear = do_replace (Some id) naming in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS (clear_metas clenv.evd)) - (if sidecond_first then - Tacticals.New.tclTHENFIRST - (assert_before_then_gen with_clear naming new_hyp_typ tac) exact_tac - else - Tacticals.New.tclTHENLAST + (Tacticals.New.tclTHENLAST (assert_after_then_gen with_clear naming new_hyp_typ tac) exact_tac) (********************************************) @@ -1360,22 +1353,25 @@ let rec contract_letin_in_lam_header sigma c = | LetIn (x,b,t,c) -> contract_letin_in_lam_header sigma (subst1 b c) | _ -> c -let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags ()) - rename i (elim, elimty, bindings) indclause = - Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let elim = contract_letin_in_lam_header sigma elim in - let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in - let indmv = - (match EConstr.kind sigma (nth_arg sigma i elimclause.templval.rebus) with - | Meta mv -> mv - | _ -> user_err ~hdr:"elimination_clause" - (str "The type of elimination clause is not well-formed.")) +let elimination_in_clause_scheme env sigma with_evars ~flags + id hypmv elimclause = + let hyp = mkVar id in + let hyp_typ = Retyping.get_type_of env sigma hyp in + let hypclause = mk_clenv_from_env env sigma (Some 0) (hyp, hyp_typ) in + let elimclause'' = + (* The evarmap of elimclause is assumed to be an extension of hypclause, so + we do not need to merge the universes coming from hypclause. *) + try clenv_fchain ~with_univs:false ~flags hypmv elimclause hypclause + with PretypeError (env,evd,NoOccurrenceFound (op,_)) -> + (* Set the hypothesis name in the message *) + raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id))) in - let elimclause' = clenv_fchain ~flags indmv elimclause indclause in - Clenvtac.res_pf elimclause' ~with_evars ~with_classes ~flags - end + let new_hyp_typ = clenv_type elimclause'' in + if EConstr.eq_constr sigma hyp_typ new_hyp_typ then + user_err ~hdr:"general_rewrite_in" + (str "Nothing to rewrite in " ++ Id.print id ++ str"."); + clenv_refine_in with_evars id id sigma elimclause'' + (fun id -> Proofview.tclUNIT ()) (* * Elimination tactic with bindings and using an arbitrary @@ -1387,11 +1383,10 @@ let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags type eliminator = { elimindex : int option; (* None = find it automatically *) - elimrename : (bool * int array) option; (** None = don't rename Prop hyps with H-names *) elimbody : EConstr.constr with_bindings } -let general_elim_clause_gen elimtac indclause elim = +let general_elim_clause with_evars flags where indclause elim = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in @@ -1399,7 +1394,27 @@ let general_elim_clause_gen elimtac indclause elim = let elimt = Retyping.get_type_of env sigma elimc in let i = match elim.elimindex with None -> index_of_ind_arg sigma elimt | Some i -> i in - elimtac elim.elimrename i (elimc, elimt, lbindelimc) indclause + let elimc = contract_letin_in_lam_header sigma elimc in + let elimclause = make_clenv_binding env sigma (elimc, elimt) lbindelimc in + let indmv = + (match EConstr.kind sigma (nth_arg sigma i elimclause.templval.rebus) with + | Meta mv -> mv + | _ -> user_err ~hdr:"elimination_clause" + (str "The type of elimination clause is not well-formed.")) + in + match where with + | None -> + let elimclause = clenv_fchain ~flags indmv elimclause indclause in + Clenvtac.res_pf elimclause ~with_evars ~with_classes:true ~flags + | Some id -> + let hypmv = + match List.remove Int.equal indmv (clenv_independent elimclause) with + | [a] -> a + | _ -> user_err ~hdr:"elimination_clause" + (str "The type of elimination clause is not well-formed.") + in + let elimclause = clenv_fchain ~flags indmv elimclause indclause in + elimination_in_clause_scheme env sigma with_evars ~flags id hypmv elimclause end let general_elim with_evars clear_flag (c, lbindc) elim = @@ -1408,12 +1423,12 @@ let general_elim with_evars clear_flag (c, lbindc) elim = let sigma = Tacmach.New.project gl in let ct = Retyping.get_type_of env sigma c in let t = try snd (reduce_to_quantified_ind env sigma ct) with UserError _ -> ct in - let elimtac = elimination_clause_scheme with_evars in let indclause = make_clenv_binding env sigma (c, t) lbindc in let sigma = meta_merge sigma (clear_metas indclause.evd) in + let flags = elim_flags () in Proofview.Unsafe.tclEVARS sigma <*> Tacticals.New.tclTHEN - (general_elim_clause_gen elimtac indclause elim) + (general_elim_clause with_evars flags None indclause elim) (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c) end @@ -1436,8 +1451,7 @@ let general_case_analysis_in_context with_evars clear_flag (c,lbindc) = let elim = EConstr.of_constr elim in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (general_elim with_evars clear_flag (c,lbindc) - {elimindex = None; elimbody = (elim,NoBindings); - elimrename = Some (false, constructors_nrealdecls env (fst mind))}) + {elimindex = None; elimbody = (elim,NoBindings); }) end let general_case_analysis with_evars clear_flag (c,lbindc as cx) = @@ -1468,8 +1482,7 @@ let find_eliminator c gl = let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_unsafe_type_of gl c) in if is_nonrec ind then raise IsNonrec; let evd, c = find_ind_eliminator ind (Tacticals.New.elimination_sort_of_goal gl) gl in - evd, {elimindex = None; elimbody = (c,NoBindings); - elimrename = Some (true, constructors_nrealdecls (Global.env()) ind)} + evd, { elimindex = None; elimbody = (c,NoBindings) } let default_elim with_evars clear_flag (c,_ as cx) = Proofview.tclORELSE @@ -1489,7 +1502,7 @@ let default_elim with_evars clear_flag (c,_ as cx) = let elim_in_context with_evars clear_flag c = function | Some elim -> general_elim with_evars clear_flag c - {elimindex = Some (-1); elimbody = elim; elimrename = None} + { elimindex = Some (-1); elimbody = elim } | None -> default_elim with_evars clear_flag c let elim with_evars clear_flag (c,lbindc as cx) elim = @@ -1515,48 +1528,6 @@ let simplest_elim c = default_elim false None (c,NoBindings) (e.g. it could replace id:A->B->C by id:C, knowing A/\B) *) -let clenv_fchain_in id ?(flags=elim_flags ()) mv elimclause hypclause = - (* The evarmap of elimclause is assumed to be an extension of hypclause, so - we do not need to merge the universes coming from hypclause. *) - try clenv_fchain ~with_univs:false ~flags mv elimclause hypclause - with PretypeError (env,evd,NoOccurrenceFound (op,_)) -> - (* Set the hypothesis name in the message *) - raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id))) - -let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) - id rename i (elim, elimty, bindings) indclause = - Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let elim = contract_letin_in_lam_header sigma elim in - let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in - let indmv = destMeta sigma (nth_arg sigma i elimclause.templval.rebus) in - let hypmv = - match List.remove Int.equal indmv (clenv_independent elimclause) with - | [a] -> a - | _ -> user_err ~hdr:"elimination_clause" - (str "The type of elimination clause is not well-formed.") - in - let elimclause' = clenv_fchain ~flags indmv elimclause indclause in - let hyp = mkVar id in - let hyp_typ = Retyping.get_type_of env sigma hyp in - let hypclause = mk_clenv_from_env env sigma (Some 0) (hyp, hyp_typ) in - let elimclause'' = clenv_fchain_in id ~flags hypmv elimclause' hypclause in - let new_hyp_typ = clenv_type elimclause'' in - if EConstr.eq_constr sigma hyp_typ new_hyp_typ then - user_err ~hdr:"general_rewrite_in" - (str "Nothing to rewrite in " ++ Id.print id ++ str"."); - clenv_refine_in with_evars id id sigma elimclause'' - (fun id -> Proofview.tclUNIT ()) - end - -let general_elim_clause with_evars flags id c e = - let elim = match id with - | None -> elimination_clause_scheme with_evars ~with_classes:true ~flags - | Some id -> elimination_in_clause_scheme with_evars ~flags id - in - general_elim_clause_gen elim c e - (* Apply a tactic below the products of the conclusion of a lemma *) type conjunction_status = @@ -1828,7 +1799,7 @@ let apply_in_once_main flags innerclause env sigma (loc,d,lbind) = in aux (make_clenv_binding env sigma (d,thm) lbind) -let apply_in_once ?(respect_opaque = false) sidecond_first with_delta +let apply_in_once ?(respect_opaque = false) with_delta with_destruct with_evars naming id (clear_flag,{ CAst.loc; v= d,lbind}) tac = let open Context.Rel.Declaration in Proofview.Goal.enter begin fun gl -> @@ -1849,7 +1820,7 @@ let apply_in_once ?(respect_opaque = false) sidecond_first with_delta if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in try let clause = apply_in_once_main flags innerclause env sigma (loc,c,lbind) in - clenv_refine_in ~sidecond_first with_evars targetid id sigma clause + clenv_refine_in with_evars targetid id sigma clause (fun id -> Tacticals.New.tclTHENLIST [ apply_clear_request clear_flag false c; @@ -1866,14 +1837,14 @@ let apply_in_once ?(respect_opaque = false) sidecond_first with_delta aux [] with_destruct d end -let apply_in_delayed_once ?(respect_opaque = false) sidecond_first with_delta +let apply_in_delayed_once ?(respect_opaque = false) with_delta with_destruct with_evars naming id (clear_flag,{CAst.loc;v=f}) tac = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let (sigma, c) = f env sigma in Tacticals.New.tclWITHHOLES with_evars - (apply_in_once ~respect_opaque sidecond_first with_delta with_destruct with_evars + (apply_in_once ~respect_opaque with_delta with_destruct with_evars naming id (clear_flag,CAst.(make ?loc c)) tac) sigma end @@ -2493,7 +2464,7 @@ and intro_pattern_action ?loc with_evars b style pat thin destopt tac id = clear [id] in let f env sigma = let (sigma, c) = f env sigma in (sigma,(c, NoBindings)) in - apply_in_delayed_once false true true with_evars naming id (None,CAst.make ?loc:loc' f) + apply_in_delayed_once true true with_evars naming id (None,CAst.make ?loc:loc' f) (fun id -> Tacticals.New.tclTHENLIST [doclear; tac_ipat id; tac thin None []]) and prepare_intros ?loc with_evars dft destopt = function @@ -2561,10 +2532,10 @@ let assert_as first hd ipat t = (* apply in as *) -let general_apply_in ?(respect_opaque=false) sidecond_first with_delta +let general_apply_in ?(respect_opaque=false) with_delta with_destruct with_evars id lemmas ipat = let tac (naming,lemma) tac id = - apply_in_delayed_once ~respect_opaque sidecond_first with_delta + apply_in_delayed_once ~respect_opaque with_delta with_destruct with_evars naming id lemma tac in Proofview.Goal.enter begin fun gl -> let destopt = @@ -2593,10 +2564,10 @@ let general_apply_in ?(respect_opaque=false) sidecond_first with_delta let apply_in simple with_evars id lemmas ipat = let lemmas = List.map (fun (k,{CAst.loc;v=l}) -> k, CAst.make ?loc (fun _ sigma -> (sigma,l))) lemmas in - general_apply_in false simple simple with_evars id lemmas ipat + general_apply_in simple simple with_evars id lemmas ipat let apply_delayed_in simple with_evars id lemmas ipat = - general_apply_in ~respect_opaque:true false simple simple with_evars id lemmas ipat + general_apply_in ~respect_opaque:true simple simple with_evars id lemmas ipat (*****************************) (* Tactics abstracting terms *) @@ -4183,7 +4154,7 @@ let find_induction_type isrec elim hyp0 gl = let scheme = compute_elim_sig sigma ~elimc elimt in if Option.is_empty scheme.indarg then error "Cannot find induction type"; let indsign = compute_scheme_signature evd scheme hyp0 ind_guess in - let elim = ({elimindex = Some(-1); elimbody = elimc; elimrename = None},elimt) in + let elim = ({ elimindex = Some(-1); elimbody = elimc },elimt) in scheme, ElimUsing (elim,indsign) in match scheme.indref with @@ -4210,10 +4181,7 @@ let get_eliminator elim dep s gl = | ElimOver (isrec,id) -> let evd, (elimc,elimt),_ as elims = guess_elim isrec dep s id gl in let _, (l, s) = compute_elim_signature elims id in - let branchlengthes = List.map (fun d -> assert (RelDecl.is_local_assum d); pi1 (decompose_prod_letin (Tacmach.New.project gl) (RelDecl.get_type d))) - (List.rev s.branches) - in - evd, isrec, ({elimindex = None; elimbody = elimc; elimrename = Some (isrec,Array.of_list branchlengthes)}, elimt), l + evd, isrec, ({ elimindex = None; elimbody = elimc }, elimt), l (* Instantiate all meta variables of elimclause using lid, some elts of lid are parameters (first ones), the other are @@ -4257,7 +4225,7 @@ let recolle_clenv i params args elimclause gl = let induction_tac with_evars params indvars elim = Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in - let ({elimindex=i;elimbody=(elimc,lbindelimc);elimrename=rename},elimt) = elim in + let ({ elimindex=i;elimbody=(elimc,lbindelimc) },elimt) = elim in let i = match i with None -> index_of_ind_arg sigma elimt | Some i -> i in (* elimclause contains this: (elimc ?i ?j ?k...?l) *) let elimc = contract_letin_in_lam_header sigma elimc in @@ -4362,7 +4330,7 @@ let induction_without_atomization isrec with_evars elim names lid = (* FIXME: Tester ca avec un principe dependant et non-dependant *) induction_tac with_evars params realindvars elim; ] in - let elim = ElimUsing (({elimindex = Some (-1); elimbody = Option.get scheme.elimc; elimrename = None}, scheme.elimt), indsign) in + let elim = ElimUsing (({ elimindex = Some (-1); elimbody = Option.get scheme.elimc }, scheme.elimt), indsign) in apply_induction_in_context with_evars None [] elim indvars names induct_tac end diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 9eb8196280..32c64bacf6 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -282,7 +282,6 @@ val compute_elim_sig : evar_map -> ?elimc:constr with_bindings -> types -> elim_ (** elim principle with the index of its inductive arg *) type eliminator = { elimindex : int option; (** None = find it automatically *) - elimrename : (bool * int array) option; (** None = don't rename Prop hyps with H-names *) elimbody : constr with_bindings } diff --git a/test-suite/bugs/closed/bug_10026.v b/test-suite/bugs/closed/bug_10026.v new file mode 100644 index 0000000000..0d3142d0f2 --- /dev/null +++ b/test-suite/bugs/closed/bug_10026.v @@ -0,0 +1,3 @@ +Require Import Coq.Lists.List. +Set Debug RAKAM. +Check fun _ => fold_right (fun A B => prod A B) unit _. diff --git a/test-suite/bugs/opened/bug_3754.v b/test-suite/bugs/closed/bug_3754.v index 18820b1a4c..7031cbf132 100644 --- a/test-suite/bugs/opened/bug_3754.v +++ b/test-suite/bugs/closed/bug_3754.v @@ -281,5 +281,7 @@ Defined. (factor2 fact)). rewrite <- ap_p_pp; rewrite_moveL_Mp_p. Set Debug Tactic Unification. - Fail rewrite (concat_Ap ff2). + rewrite (concat_Ap ff2). Abort. + +End Factorization. diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v index d8d222730e..1701bf4365 100644 --- a/user-contrib/Ltac2/Constr.v +++ b/user-contrib/Ltac2/Constr.v @@ -38,6 +38,7 @@ Ltac2 Type kind := [ | Fix (int array, int, ident option array, constr array, constr array) | CoFix (int, ident option array, constr array, constr array) | Proj (projection, constr) +| Uint63 (uint63) ]. Ltac2 @ external kind : constr -> kind := "ltac2" "constr_kind". diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v index 16e7d7a6f9..dc1690bdfb 100644 --- a/user-contrib/Ltac2/Init.v +++ b/user-contrib/Ltac2/Init.v @@ -14,6 +14,7 @@ Ltac2 Type int. Ltac2 Type string. Ltac2 Type char. Ltac2 Type ident. +Ltac2 Type uint63. (** Constr-specific built-in types *) Ltac2 Type meta. diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index d7e7b91ee6..da8600109e 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -424,8 +424,8 @@ let () = define1 "constr_kind" constr begin fun c -> Value.of_ext Value.val_projection p; Value.of_constr c; |] - | Int _ -> - assert false + | Int n -> + v_blk 17 [|Value.of_uint63 n|] end end @@ -503,6 +503,9 @@ let () = define1 "constr_make" valexpr begin fun knd -> let p = Value.to_ext Value.val_projection p in let c = Value.to_constr c in EConstr.mkProj (p, c) + | (17, [|n|]) -> + let n = Value.to_uint63 n in + EConstr.mkInt n | _ -> assert false in return (Value.of_constr c) diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index 9fd01426de..254c2e5086 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -740,7 +740,6 @@ let register_redefinition ?(local = false) qid e = Lib.add_anonymous_leaf (inTac2Redefinition def) let perform_eval ~pstate e = - let open Proofview.Notations in let env = Global.env () in let (e, ty) = Tac2intern.intern ~strict:false e in let v = Tac2interp.interp Tac2interp.empty_environment e in @@ -761,12 +760,8 @@ let perform_eval ~pstate e = | Goal_select.SelectAll -> v | Goal_select.SelectAlreadyFocused -> assert false (* TODO **) in - (* HACK: the API doesn't allow to return a value *) - let ans = ref None in - let tac = (v >>= fun r -> ans := Some r; Proofview.tclUNIT ()) in - let (proof, _) = Proof.run_tactic (Global.env ()) tac proof in + let (proof, _, ans) = Proof.run_tactic (Global.env ()) v proof in let sigma = Proof.in_proof proof (fun sigma -> sigma) in - let ans = match !ans with None -> assert false | Some r -> r in let name = int_name () in Feedback.msg_notice (str "- : " ++ pr_glbtype name (snd ty) ++ spc () ++ str "=" ++ spc () ++ diff --git a/user-contrib/Ltac2/tac2ffi.ml b/user-contrib/Ltac2/tac2ffi.ml index e3127ab9df..1043d25a75 100644 --- a/user-contrib/Ltac2/tac2ffi.ml +++ b/user-contrib/Ltac2/tac2ffi.ml @@ -30,6 +30,8 @@ type valexpr = (** Open constructors *) | ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr (** Arbitrary data *) +| ValUint63 of Uint63.t + (** Primitive integers *) and closure = MLTactic : (valexpr, 'v) arity0 * 'v -> closure @@ -47,21 +49,21 @@ type t = valexpr let is_int = function | ValInt _ -> true -| ValBlk _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ -> false +| ValBlk _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ | ValUint63 _ -> false let tag v = match v with | ValBlk (n, _) -> n -| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ -> +| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ | ValUint63 _ -> CErrors.anomaly (Pp.str "Unexpected value shape") let field v n = match v with | ValBlk (_, v) -> v.(n) -| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ -> +| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ | ValUint63 _ -> CErrors.anomaly (Pp.str "Unexpected value shape") let set_field v n w = match v with | ValBlk (_, v) -> v.(n) <- w -| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ -> +| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ | ValUint63 _ -> CErrors.anomaly (Pp.str "Unexpected value shape") let make_block tag v = ValBlk (tag, v) @@ -192,7 +194,7 @@ let of_closure cls = ValCls cls let to_closure = function | ValCls cls -> cls -| ValExt _ | ValInt _ | ValBlk _ | ValStr _ | ValOpn _ -> assert false +| ValExt _ | ValInt _ | ValBlk _ | ValStr _ | ValOpn _ | ValUint63 _ -> assert false let closure = { r_of = of_closure; @@ -318,6 +320,17 @@ let open_ = { r_id = false; } +let of_uint63 n = ValUint63 n +let to_uint63 = function +| ValUint63 n -> n +| _ -> assert false + +let uint63 = { + r_of = of_uint63; + r_to = to_uint63; + r_id = false; +} + let of_constant c = of_ext val_constant c let to_constant c = to_ext val_constant c let constant = repr_ext val_constant diff --git a/user-contrib/Ltac2/tac2ffi.mli b/user-contrib/Ltac2/tac2ffi.mli index bfc93d99e6..f8581061a0 100644 --- a/user-contrib/Ltac2/tac2ffi.mli +++ b/user-contrib/Ltac2/tac2ffi.mli @@ -28,6 +28,8 @@ type valexpr = (** Open constructors *) | ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr (** Arbitrary data *) +| ValUint63 of Uint63.t + (** Primitive integers *) type 'a arity @@ -143,6 +145,10 @@ val of_open : KerName.t * valexpr array -> valexpr val to_open : valexpr -> KerName.t * valexpr array val open_ : (KerName.t * valexpr array) repr +val of_uint63 : Uint63.t -> valexpr +val to_uint63 : valexpr -> Uint63.t +val uint63 : Uint63.t repr + type ('a, 'b) fun1 val app_fun1 : ('a, 'b) fun1 -> 'a repr -> 'b repr -> 'a -> 'b Proofview.tactic diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 1c7cc5e636..2dae0ad125 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -395,10 +395,10 @@ let start_proof_with_initialization ~ontop ?hook kind sigma decl recguard thms s maybe_declare_manual_implicits false ref imps; call_hook ?hook ctx [] strength ref) thms_data in let pstate = start_proof ~ontop id ~pl:decl kind sigma t ~hook ~compute_guard:guard in - let pstate, _ = Proof_global.with_current_proof (fun _ p -> + let pstate = Proof_global.simple_with_current_proof (fun _ p -> match init_tac with - | None -> p,(true,[]) - | Some tac -> Proof.run_tactic Global.(env ()) tac p) pstate in + | None -> p + | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p) pstate in pstate let start_proof_com ~program_mode ~ontop ?inference_hook ?hook kind thms = |