aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-08-31Require Ltac2.Fresh in Ltac2.Ltac2Jason Gross
2017-08-31Fix coq/ltac2#3: Constructor expects n arguments should name which ↵Pierre-Marie Pédrot
constructor it is.
2017-08-31Fix the type of the Constructor constructor.Pierre-Marie Pédrot
2017-08-31Document primitive projections in more detailMatthieu Sozeau
2017-08-31RefMan-ssr: fix warningMatthieu Sozeau
2017-08-31Fix install-doc targetGaëtan Gilbert
Since 8995d0857277019b54c24672439d3e19b2fcb5af [make doc] puts css files in subdirectories of doc/refman/html. These subdirectories cause a failure when doing [install doc/refman/html/* target].
2017-08-31Merge PR #980: Adding combinators + a canonical renaming in List, Option, NameMaxime Dénès
2017-08-31Merge PR #992: Fix BZ#5687: Coqtop died badly modal message box from CoqIDE.Maxime Dénès
2017-08-31Merge PR #993: Credits for version 8.7Maxime Dénès
2017-08-31Credits for version 8.7Matthieu Sozeau
2017-08-31Merge PR #999: For BZ#5688, mention hanging issue in ocamldebug and workaroundMaxime Dénès
2017-08-31Merge PR #996: Fix BZ#5697: Congruence does not work with primitive projectionsMaxime Dénès
2017-08-31Merge PR #995: Program: fix BZ#5683, missing lift when building case predicateMaxime Dénès
2017-08-31Merge PR #994: Fix BZ#5245 hnf on projections with simpl never flagMaxime Dénès
2017-08-31Merge PR #989: Prevent overallocation in Array.map_to_list and remove custom ↵Maxime Dénès
implementation from Detyping.
2017-08-31Merge PR #971: Don't allow coq-dpdgraph to failMaxime Dénès
2017-08-31Merge PR #969: Fix a typoMaxime Dénès
2017-08-31Merge PR #967: Update debuggingMaxime Dénès
2017-08-31Merge PR #958: coq_makefile: build/use .cma for packed plugins tooMaxime Dénès
2017-08-30Merge PR #998: Avoid running interactive tests on Windows.Maxime Dénès
2017-08-30Fixing part of #5707 (allowing destruct to use non dependent case analysis).Hugo Herbelin
The fix covers the case of a non-dependent goal with unavailable dependent case analysis: destruct was not seeing that it could still use non-dependent case analysis.
2017-08-30Fixing a capitalization in the middle of the sentence of an error message.Hugo Herbelin
2017-08-30Binding reduction functions acting on terms.Pierre-Marie Pédrot
2017-08-29Fix printing of Ltac2 in quotations.Pierre-Marie Pédrot
2017-08-29Fixing printing of tactic expressions.Pierre-Marie Pédrot
2017-08-29Centralizing tag declarations.Pierre-Marie Pédrot
2017-08-29mention issue with OCAMLRUNPARAM and ocamldebugPaul Steckler
2017-08-29Rolling our own generic arguments.Pierre-Marie Pédrot
2017-08-29coq_makefile: fix .merlin generation (FLG -thread)Enrico Tassi
2017-08-29coq_makefile: improve documentationEnrico Tassi
2017-08-29Rolling our own dynamic types for Ltac2.Pierre-Marie Pédrot
This prevents careless confusions with generic arguments from Coq.
2017-08-29coq_makefile: print error message when coqlib is not set properlyEnrico Tassi
2017-08-29coq_makefile(pack): ml -> cmx --pack-> cmx -> cmxa -> cmxsEnrico Tassi
2017-08-29Fix link to debugging file.Théo Zimmermann
2017-08-29[general] Merge parsing with highparsing, put toplevel at the top of the ↵Emilio Jesus Gallego Arias
linking chain.
2017-08-29[vernac] Store Infix Modifier in Vernac Notation.Pierre-Marie Pédrot
This removes a dependency from `G_vernac` to `Metasyntax`.
2017-08-29Adapt debugging doc to configure/Makefile changes.Théo Zimmermann
2017-08-29Move debugging to Markdown.Théo Zimmermann
With a minimal diff (so I'm not putting quotes ` ` around all the code).
2017-08-29Fix deployment to multiple providers.Maxime Dénès
2017-08-29Merge PR #961: Add a set of contributing guidelinesMaxime Dénès
2017-08-29Avoid running interactive tests on Windows.Maxime Dénès
This is a temporary workaround, until we fix the underlying issue which makes coqtop hang on those tests.
2017-08-29Statically enforcing that module types have no retroknowledge.Pierre-Marie Pédrot
2017-08-29Separating the module_type and module_body types by using a type parameter.Pierre-Marie Pédrot
As explained in edf85b9, the original commit that merged the module_body and module_type_body representations, this was delayed to a later time assumedly due to OCaml lack of GADTs. Actually, the only thing that was needed was polymorphic recursion, which has been around already for a relatively long time (since 3.12).
2017-08-29[parsing] Remove hacks for reduced Prelude.Emilio Jesus Gallego Arias
These hacks to warn the users about needed modules are not needed anymore in 8.8, as the proper error message is done in 8.7 already. This helps in avoiding a dependency from parsing to MlTop.
2017-08-29Properly handling parameters of primitive projections in cctac.Pierre-Marie Pédrot
2017-08-29Fix BZ#5697: Congruence does not work with primitive projections.Pierre-Marie Pédrot
The code generating the projection was unconditionally generating pattern-matchings, although this is incorrect for primitive records.
2017-08-29Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170Maxime Dénès
2017-08-29Merge PR #988: Fix obsolete description of real numerals.Maxime Dénès
2017-08-29Pass Ltac2 variables in a dedicated environment for generic arguments.Pierre-Marie Pédrot
This is a way to hack around the fact that various interpretation functions rely wrongly on the values of the environment to do nasty tricks. Typically, the interpretation of terms is broken, as it will fail when there is a bound variable with the same name as a hypothesis, instead of producing the hypothesis itself.
2017-08-29Removing dead code for handling of array litterals.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-26 08:54:08 +0000