aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-04-12Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of ↵Maxime Dénès
record fields.
2017-04-12Missing optimization when Kernel Term Sharing is disabled.Pierre-Marie Pédrot
We don't have to perfom in-place updates because we actually know that there is none on the stack. This should speed up UniMath.
2017-04-11Merge PR#549: Fast path in weak head reduction of applied atoms.Maxime Dénès
2017-04-11Update INSTALL now that -debug is the default.Théo Zimmermann
Also updates the references to debugging documentation.
2017-04-11Merge PR#543: Sanitize instance interpretationMaxime Dénès
2017-04-11Update RefMan-pre to mention template polymorphism.Gaetan Gilbert
2017-04-11Update various comments to use "template polymorphism"Gaetan Gilbert
Also remove obvious comments.
2017-04-11Use "template polymorphism" in the documentation.Gaetan Gilbert
2017-04-11Mention template polymorphism in the documentation.Gaetan Gilbert
Since About mentions it the doc should as well.
2017-04-11Merge PR#532: Clean Nsatz implementation.Maxime Dénès
2017-04-11Merge PR#537: Efficient side-effect abstractionMaxime Dénès
2017-04-11Merge PR#379: Introducing evar-insensitive constrsMaxime Dénès
2017-04-10Adding a test for 'rewrite in *' when an evar is solved by side-effect.Pierre-Marie Pédrot
2017-04-10Adding a test for the correctness of normalization in legacy typeclasses.Pierre-Marie Pédrot
This is a test for commit 9d1230d484a2cf519f9cd76dc0f37815f3c6339b.
2017-04-10Documenting the changes introduced by the EConstr branch.Pierre-Marie Pédrot
2017-04-10Revert "refactoring: Reductionops.contextual_reduction_function type"Matej Košík
This reverts commit 470d0d56467a3a587dc34f958ffea8259618d1ae.
2017-04-10Revert "comment: typo"Matej Košík
This reverts commit cd248e01d6834bc43d733c08b5955c332d2146a6.
2017-04-10Revert "refactoring: Names.DirPath.equal"Matej Košík
This reverts commit 0d364f7aa5cee042f0b327966fce35778f3285e0.
2017-04-10Revert "refactoring: Names.DirPath.compare"Matej Košík
This reverts commit 7a51d6a94bdd6cc889cd69fa0fbb5c8a655b2b16.
2017-04-10Revert "refactoring: Names.DirPath.is_empty"Matej Košík
This reverts commit e180cce2384bacaa5ad5b9d6e15b55de8cc913cc.
2017-04-10Revert "simplify: Environ.push_named"Matej Košík
This reverts commit 9394aefa8e519a9e2b1b45659a47d5ff3f15ed16.
2017-04-10Revert "trivial"Matej Košík
This reverts commit 28973285f4b9389ed0610b94ba907684214dd279.
2017-04-10Revert "trivial"Matej Košík
This reverts commit 9b627431516f2cf88312329def9e0ec5e8605a98.
2017-04-10Revert "comments: corrected in the Context module"Matej Košík
This reverts commit 538d8edf708ba049e60e6bc32902ba5fdca720bb.
2017-04-10comments: corrected in the Context moduleMatej Kosik
2017-04-10trivialMatej Kosik
2017-04-10trivialMatej Kosik
2017-04-10simplify: Environ.push_namedMatej Kosik
2017-04-10refactoring: Names.DirPath.is_emptyMatej Kosik
2017-04-10refactoring: Names.DirPath.compareMatej Kosik
2017-04-10refactoring: Names.DirPath.equalMatej Kosik
2017-04-10comment: typoMatej Kosik
2017-04-10refactoring: Reductionops.contextual_reduction_function typeMatej Kosik
2017-04-10Merge PR#547: [toplevel] Remove the feedback printer only on exit.Maxime Dénès
2017-04-10Merge PR#548: [ide] Correctly place warning tags.Maxime Dénès
2017-04-09Merge PR#460: Turning the printing primitive projection compatibility flag ↵Maxime Dénès
off by default
2017-04-09Fix an algorithmic issue in Nsatz.Pierre-Marie Pédrot
We use heaps instead of continuously adding elements to an ordered list, which was quadratic in the worst case. As a byproduct, this solves bug #5359, which was due to a stack overflow on big lists.
2017-04-09Academic prescriptivism strikes back: down with baroque programming in Nsatz.Pierre-Marie Pédrot
Several cleanups were performed. 1. Removal of dead code lurking around. 2. Removal of global variables used to pass arguments to functions, as well as unnecessary mutable state here and there. We rely on state-passing and encapsulated mutable state. 3. Removal of crazy reference manipulation and its replacement with proper list handling, as well as cleaning up the source and taking advantage of invariants. This should solve algorithmic limitations of the previous code. 4. Opacification of some structures to have a clearer idea of the code requirements. 5. Cleaning of debug printing functions. We thunk the computation of the debugging data, whose computation can be costly for no reason, and we rely on Feedback-based interaction instead of Printf-debugging.
2017-04-09Fixing #5420 as well as many related bugs due to miscounting let-ins.Hugo Herbelin
- Supporting let-ins in tactic "fix", and hence in interactive Fixpoint and mutual theorems. - Documenting more precisely the meaning of n in tactic "fix id n". - Fixing computation of recursive index at interpretation time in the presence of let-ins.
2017-04-09Fixing several wrong computations of implicit arguments by positionHugo Herbelin
in the presence of let-ins.
2017-04-09Minor cosmetic commit.Hugo Herbelin
2017-04-09Documenting how the recursive indices of a fixpoint are computed.Hugo Herbelin
Also documenting how the implicit arguments by position are computed.
2017-04-09More explicit message when a {struct x} argument refers to a local definition.Hugo Herbelin
2017-04-09Removing internal support for accepting "{struct x}" and co in "Theorem with".Hugo Herbelin
There were actually no syntax for it, and I'm still unsure what good syntax to give to it, even more that it would be useful to have one.
2017-04-08Fast path in weak head reduction of applied atoms.Pierre-Marie Pédrot
Instead of calling the whole reduction machirery, we check before reducing that a term is an applied atom, i.e. inductive, constructor, evar or meta. In that case, the abstract machine acts as the identity but needs to destruct and reconstruct the whole term, which can be very costly. This fixes part of bug #5421: vm_compute is very slow at doing nothing, where recomputation of the type of a big inductive was incredibly expensive.
2017-04-08Fixing #5460 (limitation in computing deps in pattern-matching compilation).Hugo Herbelin
This was assuming dependencies occurring in configurations of the form x:A, y:B x, z:C x y |- match x, y, z with ... end". But still work to do for better management of dependencies in general...
2017-04-08[ide] Correctly place warning tags.Emilio Jesus Gallego Arias
8e07227c5853de78eaed4577eefe908fb84507c0 introduced an incorrect duplicate of `position_error_tag_at_sentence`, which sets the end of the underlining position starting at the end of the sentence, whereas the location in the feedback refers to the beginning, thus it highlights more text than it should. This was missed in 8.6 as it seems that the code was not called. We undo the duplication and fix the bug.
2017-04-08Update the .mailmap file.Guillaume Melquiond
2017-04-08Fix a heuristic used by legacy typeclass resolution.Pierre-Marie Pédrot
The evarmap used by the heuristic could contain resolved evars, which could lead to a failure of backtracking in the EConstr branch. This is experimental and may be to costly.
2017-04-07[stm] remove process_error_hookEmilio Jesus Gallego Arias
`process_error_hook` seems unnecesary, we just call the proper error interpretation.
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-28 13:47:37 +0000