aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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.
2017-08-29Implementing Ltac2 antiquotations in constr syntax.Pierre-Marie Pédrot
2017-08-29Binding an unsafe substitution function.Pierre-Marie Pédrot
2017-08-29Binding primitives to generate fresh variables.Pierre-Marie Pédrot
2017-08-28Fix README.Pierre-Marie Pédrot
2017-08-28Fix coq/ltac2#6: Expected and actual types are flipped.Pierre-Marie Pédrot
2017-08-28typosgallais
2017-08-27Do not reuse the Val.t type in toplevel values.Pierre-Marie Pédrot
2017-08-27Notation for clear.Pierre-Marie Pédrot
2017-08-27Fix semantics of the solve tactical.Pierre-Marie Pédrot
2017-08-27Ensure no confusion with unit in rigid variables.Pierre-Marie Pédrot
2017-08-27Proper handling of rigid variables in subtyping.Pierre-Marie Pédrot
2017-08-27Introducing rebindable toplevel definitions.Pierre-Marie Pédrot
2017-08-26Allowing calls to Ltac2 inside Ltac1.Pierre-Marie Pédrot
2017-08-26TyposHugo Herbelin
2017-08-26Allowing to insert calls to Ltac1 references in Ltac2.Pierre-Marie Pédrot
2017-08-25Adding more notations for the lulz.Pierre-Marie Pédrot
2017-08-25Introducing a distinct bindings scope.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-27 06:20:23 +0000