aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-04-28Revert "Using a more explicit algebraic type for evars of kind "MatchingVar"."Maxime Dénès
I'm sure this was pushed by accident, since testing shows immediately that it breaks the compilation of the ssreflect plugin, hence all developments relying on it in Travis.
2017-04-28Allow interactive editing of {C,}Morphisms in PGJason Gross
2017-04-28Add .dir-locals.el and _CoqProject files for emacs stdlib editingJason Gross
These set up PG to use the local coqtop, and the local coqlib, when editing files in the stdlib. As per https://github.com/coq/coq/pull/386#issuecomment-279012238, we can use `_CoqProject` for `theories/Init`, and this allows CoqIDE to edit those files. However, we cannot use it for `theories/`, because a `_CoqProject` file will override a `.dir-locals.el` in the same directory, and there is no way to get PG to pick up a valid `-coqlib` from `_CoqProject` (because it'll take the path relative to the current directory, not relative to the directory of `_CoqProject`).
2017-04-28Using a more explicit algebraic type for evars of kind "MatchingVar".Hugo Herbelin
A priori considered to be a good programming style.
2017-04-28Renaming allow_patvar flag of intern_gen into pattern_mode.Hugo Herbelin
This highlights that this is a binary mode changing the interpretation of "?x" rather than additionally allowing patvar.
2017-04-28Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).Hugo Herbelin
The fix follows an invariant enforced in proofview.ml on the kind of evars that are goals or that occur in goals. One day, evar kinds will need a little cleaning...
2017-04-28Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of ↵Maxime Dénès
let-ins
2017-04-27Post-rebase warnings (unused opens and 2 unused values)Gaetan Gilbert
2017-04-27Enable more warnings, and add -warn-error configure flagGaetan Gilbert
2017-04-27Fix 4.04 warningsGaetan Gilbert
2017-04-27Remove uses of [Flags.make_silent]Gaetan Gilbert
2017-04-27Warning 29: non escaped end of line may be non portableGaetan Gilbert
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-27Micromega: do not use Filename.temp_dir_path, remove unused valuesGaetan Gilbert
2017-04-27Remove unused constructorsGaetan Gilbert
2017-04-27Add [_] prefix to unused values which maybe should be keptGaetan Gilbert
2017-04-27Remove some unused values and typesGaetan Gilbert
2017-04-27Rename Sos_lib.(||) -> parser_or to avoid (deprecated) Pervasives.orGaetan Gilbert
2017-04-27Disambiguate Polynomial.Hyp and Mfourier.Hyp -> AssumGaetan Gilbert
2017-04-27Use [method!] to override methods (warning 7)Gaetan Gilbert
2017-04-27Fix omitted labels in function callsGaetan Gilbert
2017-04-27Remove unused [rec] keywordsGaetan Gilbert
2017-04-27Locally disable some warnings.Gaetan Gilbert
2017-04-27Merge PR#414: Some more theory on powerRZ.Maxime Dénès
2017-04-27Merge PR#583: [toplevel] More work on error handling.Maxime Dénès
2017-04-27Merge PR#587: Fix description of command-line arguments for Add (Rec) LoadPathMaxime Dénès
2017-04-27fix order of command-line arguments mentioned in Add LoadPathPaul Steckler
2017-04-27Merge PR#586: trivial cleanup commits which does not change Coq APIMaxime Dénès
2017-04-27Test for bug #5193: Uncaught exception Class_tactics.Search.ReachedLimitEx.Pierre-Marie Pédrot
2017-04-27Merge PR#568: Remove tactic compatibility layerMaxime Dénès
2017-04-27Tentative note in CHANGES about now applying βι while typing "match" branches.Hugo Herbelin
In practice, this is almost invisible except when using "refine". So, in some sense, it is aligning the behavior of pretyping on the one of logic.ml's "refine" so that the more natural behavior of 8.4's refine on this issue is restored.
2017-04-27Test surgical use of beta-iota in the type of variables coming fromHugo Herbelin
pattern-matching for refine.
2017-04-27A refined solution to the beta-iota discrepancies between 8.4 and 8.5 "refine".Hugo Herbelin
There is a long story of commits trying to improve the compatibility between 8.4 and 8.5 refine, as discussed in https://github.com/coq/coq/pull/346. ac9c5986b77bf4a783f2bd0ad571645694c960e1 add beta-iota in hypotheses and conclusion 8afac4f87d9d7e3add1c19485f475bd2207bfde7 remove beta-iota in hypotheses 08e87eb96ab67ead60d92394eec6066d9b52e55e re-add beta-iota in hypotheses c9c54122d1d9493a965b483939e119d52121d5a6 re-remove beta-iota in hypotheses 9194180e2da0f7f9a2b2c7574bb7261cc69ead17 revert re-remove beta-iota in hypotheses 6bb352a6743c7332b9715ac15e95c806a58d101c re-re-remove beta-iota in hypotheses if <= 8.5 d8baa76d86eaa691a5386669596a6004bb44bb7a idem if = 8.5 The current commit tries to identify (one of?) the exact points of divergence between 8.4 and 8.5 refine, namely the types inferred for the variables of a pattern-matching problem. Note that for the conclusion of each new goal, there were a nf_betaiota in 8.4 done in function Evarutil.evars_to_metas, so the compatibility expects that such a nf_betaiota on the conclusion of each goal remains.
2017-04-27Document the API changes.Pierre-Marie Pédrot
2017-04-27Merge PR#584: Give andb_prop a simpler proofMaxime Dénès
2017-04-27Merge PR#585: Small typo in commentMaxime Dénès
2017-04-27Fast path when checking equality of universe levels in UState.Pierre-Marie Pédrot
We export the relevant level equality function in UGraph which is way faster than checking that each one is smaller than the other as universes.
2017-04-27Code cleaning in unification algorithm for universes.Pierre-Marie Pédrot
This patch is only moving code around and expliciting statically the invariants of the functions, so it should be 1:1 equivalent to the other one. Amongst other goodies, the unification function is not recursive anymore, which ensures that it will terminate.
2017-04-27Merge branch 'v8.6'Pierre-Marie Pédrot
2017-04-27contracting the type of "Pfedit.solve_by_implicit_tactic"Matej Košík
2017-04-26Small typo in commentVadim Zaliva
2017-04-25transparent abstract: Respond to review commentJason Gross
https://github.com/coq/coq/pull/201#discussion_r110957570
2017-04-25transparent abstract: Respond to review commentJason Gross
https://github.com/coq/coq/pull/201#discussion_r110952601
2017-04-25Make opaque optional only for tclABSTRACTJason Gross
Also move named arguments to the beginning of the functions. As per https://github.com/coq/coq/pull/201#discussion_r110928302
2017-04-25Generalize cache_term_by_tactic_thenJason Gross
This will allow a cache_term tactic that doesn't suffer from the Not_found anomalies of abstract in typeclass resolution.
2017-04-25Mark transparent_abstract as risky in docsJason Gross
As per Enrico's request.
2017-04-25Add transparent_abstract tacticJason Gross
2017-04-25Add support for transparent abstract (no syntax)Jason Gross
This is a small change that allows a transparent version of tclABSTRACT. Additionally, it factors the machinery of [abstract] through a plugin-accessible function which allows alternate continuations (other than exact_no_check. It might be nice to factor it further, into a cache_term function that caches a term, and a separate bit that calls cache_term with the result of running the tactic.
2017-04-25Give andb_prop a simpler proofJason Gross
No need to use `discriminate`. This is the hopefully uncontroversial part of https://github.com/coq/coq/pull/401.
2017-04-25[toplevel] Remove unused parameter from `Vernac.process_expr`.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-23 23:36:51 +0000