aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2017-08-29Move dev/doc/changes to Markdown.Théo Zimmermann
And remove old French part. And move part about the plugin API to the right section.
2017-08-29Post-merge API fix.Maxime Dénès
2017-08-29Merge PR #946: Functional pretyping interfaceMaxime Dénès
2017-08-29Factorizing code for declaration of primitive tactics.Pierre-Marie Pédrot
2017-08-29Merge PR #937: [general] Remove spurious dependency of highparsing on toplevel.Maxime Dénès
2017-08-29Merge PR #916: Fixing notation bug 5608 involving { } and a slight ↵Maxime Dénès
restructuration
2017-08-29Merge PR #838: Have coq-dpdgraph ci test print the differencesMaxime Dénès
2017-08-29Merge PR #830: Moving assert (the "Cut" rule) to new proof engineMaxime Dénès
2017-08-29Merge PR #819: Cleanup old thingsMaxime Dénès
2017-08-29Merge PR #805: Functional tacticsMaxime Dénès
2017-08-29Merge PR #773: [flags] Remove XML output flag.Maxime Dénès
2017-08-29Merge PR #966: Makefile : ignore user-contrib in various file searchesMaxime Dénès
2017-08-29coq_makefile: do not overwrite CAMLFLAGSEnrico Tassi
2017-08-29coq_makefile: use dedicated variable for extra packagesEnrico Tassi
CAMLPKGS is now used to hold extra findlib -packages The previous solution was to use CAMLFLAGS but since 4.05 an invocation of `ocamlopt -pack useless.cmxa foo.cmx -o packedfoo.cmx` fails saying that `useless.cmxa` is not a compilation unit description. CAMLPKGS is used in all `ocamlopt` invocations but for the one performing the packing.
2017-08-29coq_makefile: build/use .cma for packed pluginsEnrico Tassi
The build chain is always ml -> cmo -> cma ml -> cmx -> cmxa -> cmxs If we are packing, then it becomes ml -> cmo \ ml -> cmo --> cmo -> cma ml -> cmo / ml -> cmxo \ ml -> cmxo --> cmxo -> cmxa -> cmxs ml -> cmxo / The interest of always having a .cma or .cmxa is that such file can carry linking flags, that in findlib terms means which -package was use to build the plugin.
2017-08-29coq_makefile: test using findlib's packageEnrico Tassi
2017-08-29test-suite: depend on byte compilation tooEnrico Tassi
coq-makefile's tests do depend on this
2017-08-29Merge PR #985: Fix coqdoc test-suite target on Windows.Maxime Dénès
2017-08-29Trying to fix deployment of master on bintray, and deploy tags to github.Maxime Dénès
Deployment doesn't work on PRs, so I have to push it directly, sorry for the noise.
2017-08-29Master now deploys 8.8+alpha.Maxime Dénès
2017-08-29coqdoc: Support comments in verbatim outputTej Chajed
Fixes BZ#5700
2017-08-29Quoting notations in incompatible-level error message.Hugo Herbelin
2017-08-29A new step of restructuration of notations.Hugo Herbelin
This allows to issue a more appropriate message when a notation with a { } cannot be defined because of an incompatible level. E.g.: Notation "{ A } + B" := (sumbool A B) (at level 20).
2017-08-29Adding a test for #5569 (warning about skipping spaces).Hugo Herbelin
The two previous commits make the warning irrelevant and useless.
2017-08-29Dropping former fix to bug #5469 (notation format not recognizing curly braces).Hugo Herbelin
This reverts commit 53a50875 and a bit more: it also makes the check for possibly ignoring formatting spaces irrelevant, since the previous commit makes that curly brackets are not any more dropped for printing.
2017-08-29A little reorganization of notations + a fix to #5608.Hugo Herbelin
- Formerly, notations such as "{ A } + { B }" were typically split into "{ _ }" and "_ + _". We keep the split only for parsing, which is where it is really needed, but not anymore for interpretation, nor printing. - As a consequence, one notation string can give rise to several grammar entries, but still only one printing entry. - As another consequence, "{ A } + { B }" and "A + { B }" must be reserved to be used, which is after all the natural expectation, even if the sublevels are constrained. - We also now keep the information "is ident", "is binder" in the "key" characterizing the level of a notation.
2017-08-29Canonically renaming fold_map into fold_left_map in library Name.Hugo Herbelin
Also adding fold_right_map by consistency.
2017-08-29Adapting code to renaming Option.fold_map -> Option.fold_left_map.Hugo Herbelin
2017-08-29Canonically renaming fold_map into fold_left_map in library Option.Hugo Herbelin
Also adding fold_right_map by consistency.
2017-08-29Adapting code to renaming Array.fold_map -> Array.fold_left_map.Hugo Herbelin
2017-08-29Canonically renaming fold_map into fold_left_map in library Array.Hugo Herbelin
Also renaming fold_map' into fold_right_map, and fold_map2' into fold_right2_map.
2017-08-29Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_mapHugo Herbelin
(from module List).
2017-08-29Adding combinators + a canonical renaming in cList.ml.Hugo Herbelin
- Adding fold_left2_map/fold_right2_map. - Canonically renaming fold_map/fold_map' into fold_left_map/fold_right_map.
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-01 15:45:54 +0000