aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-06-05More straightforward native compilation of primitive projections.Pierre-Marie Pédrot
Instead of having a constant-based compilation of projections, we generate them at the compilation time of the inductive block to which they pertain.
2018-06-05Use projection indices in native compilation rather than constant names.Pierre-Marie Pédrot
2018-06-05Merge PR #7643: Fix #7631: native_compute fails to compile an example in Coq 8.8Pierre-Marie Pédrot
2018-06-05Merge PR #7690: Fixing typos in file Berardi.vPierre-Marie Pédrot
2018-06-05Merge PR #7646: Fix #4714: Stack overflow with native computePierre-Marie Pédrot
2018-06-05Merge PR #7099: Stronger invariants in unification signature.Matthieu Sozeau
2018-06-05Merge PR #7453: Refuse to parse empty [Context] command.Matthieu Sozeau
2018-06-05Merge PR #7495: Fix restrict_universe_contextMatthieu Sozeau
2018-06-05Make direct invocations of `simple apply` obey `Opaque` directive.Maxime Dénès
When called by auto, `simple apply` still does not respect `Opaque` because of compatibility issues.
2018-06-04Fix #7631: native_compute fails to compile an example in Coq 8.8Maxime Dénès
Dependency analysis for separate compilation was not iterated properly on rel_context and named_context.
2018-06-04Merge PR #7315: An attempt to clarify error message for Arguments needing ↵Maxime Dénès
"rename" flag
2018-06-04Tests for part of #7068 and for #7076 (vm/native_compute and return predicate).Hugo Herbelin
2018-06-04Preserving "canonical" form of return predicate in native_compute.Hugo Herbelin
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.
2018-06-04Preserving "canonical" form of return predicate in vm_compute.Hugo Herbelin
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.
2018-06-04Merge PR #7229: Deprecate implicit tactic solving.Hugo Herbelin
2018-06-04Merge PR #7486: Update old parts of CHANGES to use current bug numbers.Hugo Herbelin
2018-06-04Merge PR #7481: document 7025 (coq_makefile flag variables)Maxime Dénès
2018-06-04Merge PR #7596: [ci] [windows] Use newer OCaml version.Michael Soegtrop
2018-06-04Merge PR #7655: Refactor parsing rules for Hint Resolve -> and Hint Resolve <-Pierre-Marie Pédrot
2018-06-04[econstr] Remove some Unsafe.to_constr use.Emilio Jesus Gallego Arias
Most of it seems straightforward.
2018-06-04[termops] Update type of function, anyways not used in the codebase.Emilio Jesus Gallego Arias
Note that `Assumptions` ships its own copy, but for `Constr.t`.
2018-06-04[vernac] Switch back `auto_ind_decl` to Constr.Emilio Jesus Gallego Arias
AFAICT this tactic is always used on ground terms.
2018-06-04Make whitespace linter not check for trailing newlines.Gaëtan Gilbert
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 ```
2018-06-04Merge PR #7601: Fix notation for code snippet in documentationMaxime Dénès
2018-06-04Merge PR #7418: Actually take advantage of the normalization status of ↵Maxime Dénès
kernel closures.
2018-06-04test suite: make target to regenerate failing output testsGaëtan Gilbert
2018-06-04Merge PR #7199: Fixes #7195: missing freshness condition in Ltac ↵Matthieu Sozeau
pattern-matching names
2018-06-04Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode.Matthieu Sozeau
2018-06-04Merge PR #7114: Fix #7113: Program Let Fixpoint in section causes anomalyMatthieu Sozeau
2018-06-04Merge PR #7189: Fix #5539: algebraic universe produced by cases.Matthieu Sozeau
2018-06-04Merge PR #7349: Fix an anomaly when calling Obligation 0 or Obligation -1.Matthieu Sozeau
2018-06-04Documenting the API change.Pierre-Marie Pédrot
2018-06-04Adding an overlay for the Equations plugin.Pierre-Marie Pédrot
2018-06-04Stronger invariants in unification signature.Pierre-Marie Pédrot
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.
2018-06-04Merge PR #7013: Fixes #7011: Fix/CoFix were not considered in main loop of ↵Matthieu Sozeau
tactic unification.
2018-06-04Merge PR #7216: Replace uses of Termops.dependent by more specific functions.Matthieu Sozeau
2018-06-04Merge PR #7552: Fix #7539: Checker does not properly handle negative ↵Matthieu Sozeau
coinductive types.
2018-06-04Merge PR #7590: Fix #7586: Anomaly "Uncaught exception Not_found".Matthieu Sozeau
2018-06-04Documenting the deprecation.Pierre-Marie Pédrot
2018-06-04Deprecate implicit tactic solving.Pierre-Marie Pédrot
2018-06-04Merge PR #7249: Cleaning, documentation, uniformisation of the Coq extension ↵Pierre-Marie Pédrot
of List
2018-06-04Merge PR #7619: Mention test-suite in PR templateMaxime Dénès
2018-06-04Merge PR #7648: Indicate in the doc that clearbody can take several identsMaxime Dénès
2018-06-04Merge PR #7496: Fix #4403: insufficient handling of type-in-type in kernel.Maxime Dénès
2018-06-04Merge PR #7657: Fix a couple typos in deprecation messagesPierre-Marie Pédrot
2018-06-04Merge PR #7640: Small refactoring to clarify make_local_hint_db.Pierre-Marie Pédrot
2018-06-04Merge PR #7649: Remove some dead code in class_tactics.mlPierre-Marie Pédrot
2018-06-03Statment -> StatementHugo Herbelin
2018-06-03Fixing typos in file Berardi.vHugo Herbelin
Note that one of them is in the name of the main theorem, so we use a compatibility notation.
2018-06-03Merge PR #7682: Fixes #7641: more detailed message about disjunctive ↵Emilio Jesus Gallego Arias
patterns with different variables
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 01:14:58 +0000