aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* | | | | | | | | | | | | | | | | | | Merge PR #7464: Make whitespace linter not check for trailing space.Gravatar Maxime Dénès2018-06-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | | | | * Define rec_declaration in terms of prec_declaration.Gravatar SimonBoulier2018-06-05
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | And similarly for fixpoint and cofixpoint.
| | | | | | | | * | | | | | | | | | | Update evarutil.mliGravatar Matthieu Sozeau2018-06-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Actually all the new_ functions are in evarutil still
| | | | | | | | * | | | | | | | | | | Fix wrong deprecation msgGravatar Matthieu Sozeau2018-06-05
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | | | | | Workaround a weird error of .. coqtop::Gravatar Théo Zimmermann2018-06-05
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | | | | | Remove many abusive .. coqtop in SSR chapter.Gravatar Théo Zimmermann2018-06-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Many still remain.
| | | | | | | | | | | | | * | | | | | A few additional small fixes.Gravatar Théo Zimmermann2018-06-05
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | | | | | [sphinx] Fix missing indices warnings.Gravatar Théo Zimmermann2018-06-05
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | | | | | [ssr] index entry for "without loss", "suffices" and "generally have"Gravatar Enrico Tassi2018-06-05
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | | | | | [ssr] some fixes to the documentation markupGravatar Enrico Tassi2018-06-05
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | | | | | [sphinx] Start fixing SSR chapter.Gravatar Théo Zimmermann2018-06-05
| |_|_|_|_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | |
| | | | | * | | | | | | | | | | | | More straightforward native compilation of primitive projections.Gravatar Pierre-Marie Pédrot2018-06-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Instead of having a constant-based compilation of projections, we generate them at the compilation time of the inductive block to which they pertain.
| | | | | * | | | | | | | | | | | | Use projection indices in native compilation rather than constant names.Gravatar Pierre-Marie Pédrot2018-06-05
| |_|_|_|/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | Merge PR #7643: Fix #7631: native_compute fails to compile an example in Coq 8.8Gravatar Pierre-Marie Pédrot2018-06-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7690: Fixing typos in file Berardi.vGravatar Pierre-Marie Pédrot2018-06-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | Merge PR #7646: Fix #4714: Stack overflow with native computeGravatar Pierre-Marie Pédrot2018-06-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7099: Stronger invariants in unification signature.Gravatar Matthieu Sozeau2018-06-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7453: Refuse to parse empty [Context] command.Gravatar Matthieu Sozeau2018-06-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7495: Fix restrict_universe_contextGravatar Matthieu Sozeau2018-06-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | * | | | | | | | | | | Make direct invocations of `simple apply` obey `Opaque` directive.Gravatar Maxime Dénès2018-06-05
| |_|_|_|_|_|_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When called by auto, `simple apply` still does not respect `Opaque` because of compatibility issues.
| | | | | | * | | | | | | | | | | | | | Fix #7631: native_compute fails to compile an example in Coq 8.8Gravatar Maxime Dénès2018-06-04
| |_|_|_|_|/ / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Dependency analysis for separate compilation was not iterated properly on rel_context and named_context.
* | | | | | | | | | | | | | | | | | | Merge PR #7315: An attempt to clarify error message for Arguments needing ↵Gravatar Maxime Dénès2018-06-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | "rename" flag
| | | | | | | | | * | | | | | | | | | | Tests for part of #7068 and for #7076 (vm/native_compute and return predicate).Gravatar Hugo Herbelin2018-06-04
| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | | | | | | Preserving "canonical" form of return predicate in native_compute.Gravatar Hugo Herbelin2018-06-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Note that the normalization of the context of the return predicate was not done by the native compilation but by the lazy machine. The patch also "fixes" an anomaly in the case of an arity which was not in canonical form as in: Inductive A : nat -> id (nat->Type) := . Eval native_compute in fun x => match x in A y z return y = z with end.
| | | | | | | | | * | | | | | | | | | | Preserving "canonical" form of return predicate in vm_compute.Gravatar Hugo Herbelin2018-06-04
| |_|_|_|_|_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Note that the normalization of the context of the return predicate was not done by the vm but by the lazy machine. The patch also "fixes" an anomaly in the case of an arity which was not in canonical form as in: Inductive A : nat -> id (nat->Type) := . Eval vm_compute in fun x => match x in A y z return y = z with end.
* | | | | | | | | | | | | | | | | | | Merge PR #7229: Deprecate implicit tactic solving.Gravatar Hugo Herbelin2018-06-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7486: Update old parts of CHANGES to use current bug numbers.Gravatar Hugo Herbelin2018-06-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7481: document 7025 (coq_makefile flag variables)Gravatar Maxime Dénès2018-06-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7596: [ci] [windows] Use newer OCaml version.Gravatar Michael Soegtrop2018-06-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7655: Refactor parsing rules for Hint Resolve -> and Hint Resolve <-Gravatar Pierre-Marie Pédrot2018-06-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | * | | | | | | | | | [econstr] Remove some Unsafe.to_constr use.Gravatar Emilio Jesus Gallego Arias2018-06-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Most of it seems straightforward.
| | | | | | | | | | | | | | * | | | | | | | | | [termops] Update type of function, anyways not used in the codebase.Gravatar Emilio Jesus Gallego Arias2018-06-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Note that `Assumptions` ships its own copy, but for `Constr.t`.
| | | | | | | | | | | | | | * | | | | | | | | | [vernac] Switch back `auto_ind_decl` to Constr.Gravatar Emilio Jesus Gallego Arias2018-06-04
| |_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | AFAICT this tactic is always used on ground terms.
| | | | | | | | | | | | * | | | | | | | | | | Make whitespace linter not check for trailing newlines.Gravatar Gaëtan Gilbert2018-06-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | git does not know how to fix this automatically when they appear by removing a chunk of text at the end of the file. eg ``` foo bar ``` to ``` foo ```
* | | | | | | | | | | | | | | | | | | | | | | Merge PR #7601: Fix notation for code snippet in documentationGravatar Maxime Dénès2018-06-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7418: Actually take advantage of the normalization status of ↵Gravatar Maxime Dénès2018-06-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | kernel closures.
| | | | | | | | | | | | | | * | | | | | | | | | test suite: make target to regenerate failing output testsGravatar Gaëtan Gilbert2018-06-04
| | | | | | | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | | | | | | Merge PR #7199: Fixes #7195: missing freshness condition in Ltac ↵Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | pattern-matching names
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode.Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7114: Fix #7113: Program Let Fixpoint in section causes anomalyGravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7189: Fix #5539: algebraic universe produced by cases.Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7349: Fix an anomaly when calling Obligation 0 or Obligation -1.Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | * | | | | | | | | | | | | Documenting the API change.Gravatar Pierre-Marie Pédrot2018-06-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | * | | | | | | | | | | | | Adding an overlay for the Equations plugin.Gravatar Pierre-Marie Pédrot2018-06-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | * | | | | | | | | | | | | Stronger invariants in unification signature.Gravatar Pierre-Marie Pédrot2018-06-04
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We use an option type instead of returning a pair with a boolean. Indeed, the boolean being true was always indicating that the returned value was unchanged. The previous API was somewhat error-prone, and I don't understand why it was designed this way in the first place.
* | | | | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #7013: Fixes #7011: Fix/CoFix were not considered in main loop of ↵Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | tactic unification.
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7216: Replace uses of Termops.dependent by more specific functions.Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7552: Fix #7539: Checker does not properly handle negative ↵Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | coinductive types.
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7590: Fix #7586: Anomaly "Uncaught exception Not_found".Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | * | | | | | | | | | | | | | | Documenting the deprecation.Gravatar Pierre-Marie Pédrot2018-06-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 00:32:50 +0000