aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-03-03Completing basic lemmas about <= and < in BinInt.Z.Pos2Z.Hugo Herbelin
2017-03-03Relying on BinInt.Z.Pos2Z for proofs of a few lemmas in Zorder.Hugo Herbelin
2017-03-03Completing "few lemmas about Zneg" with lemmas also about Zpos.Hugo Herbelin
2017-03-03A couple of other useful properties about compare_cont.Hugo Herbelin
Don't know if compare_cont is very useful to use, but, at least, these extensions make sense.
2017-03-03Compatibility of iff wrt not and imp.Hugo Herbelin
This completes the series and cannot hurt.
2017-02-23Fixing #use"include" after vernac is added and ltac is moved to a plugin.Hugo Herbelin
2017-02-22Merge branch 'v8.6'Pierre-Marie Pédrot
2017-02-22Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2017-02-21[travis] track an 8.7 specific branch of HoTT.Maxime Dénès
This is required since we merged PR#309: Ltac as a plugin.
2017-02-21Merge PR#309: Ltac as a pluginMaxime Dénès
2017-02-21Add empty ltac_plugin file for forward compatibility.Maxime Dénès
This is in preparation for landing of PR#309: Ltac as a plugin
2017-02-20Merge PR#189: Remove tabulation support from pretty-printing.Maxime Dénès
2017-02-19Fixing debugger after the split of toplevel into vernac.Pierre-Marie Pédrot
2017-02-17remove obsolete file dev/Makefile.ougPierre Letouzey
2017-02-17Removing spurious folder includes in coq_makefile.Pierre-Marie Pédrot
2017-02-17Documenting the pluginification of Ltac.Pierre-Marie Pédrot
2017-02-17Fix .gitignore.Pierre-Marie Pédrot
2017-02-17Moving the Ltac plugin to a pack-based one.Pierre-Marie Pédrot
This is cumbersome, because now code may fail at link time if it's not referring to the correct module name. Therefore, one has to add corresponding open statements a the top of every file depending on a Ltac module. This includes seemingly unrelated files that use EXTEND statements.
2017-02-17Ltac as a plugin.Pierre-Marie Pédrot
This commit is essentially moving files around. In particular, the corresponding plugin still relies on a mllib file rather than a mlpack one. Otherwise, this causes link-time issues for third-party plugins depending on modules defined in the Ltac plugin.
2017-02-16Fixing #5339 (anomaly with 'pat in record parameters).Hugo Herbelin
2017-02-16Merge PR#403: Split Vernacular Processing from ToplevelMaxime Dénès
2017-02-16Merge PR#431Maxime Dénès
[travis] Add math-comp overlays, update CompCert to official version, add UniMath
2017-02-15[travis] [External CI] CompCert official 8.6 support + UniMathEmilio Jesus Gallego Arias
2017-02-15[travis] [External CI] Factor out math-comp installs.Emilio Jesus Gallego Arias
We make math-comp overlays easier, we also start structuring the scripts a bit more.
2017-02-15Make Obligations see fix_exnEnrico Tassi
2017-02-15[stm] Remove unused legacy stm interface.Emilio Jesus Gallego Arias
2017-02-15[cosmetic] Reorder makefile as suggested by @herbelinEmilio Jesus Gallego Arias
2017-02-15[stm] Reenable Show Script command.Emilio Jesus Gallego Arias
We extend `Stm.vernac_interp` so it can handle the commands it should by level. This reenables `Show Script` handling, and this interpretation function should handle more commands in the future such as Load. However note that we must first refactor the parsing state handling a bit and remove the legacy `Stm.interp` before that.
2017-02-15[stm] Break stm/toplevel dependency loop.Emilio Jesus Gallego Arias
Currently, the STM, vernac interpretation, and the toplevel are intertwined in a mutual dependency that needs to be resolved using imperative callbacks. This is problematic for a few reasons, in particular it makes the interpretation of commands that affect the document quite intricate. As a first step, we split the `toplevel/` directory into two: "pure" vernac interpretation is moved to the `vernac/` directory, on which the STM relies. Test suite passes, and only one command seems to be disabled with this approach, "Show Script" which is to my understanding obsolete. Subsequent commits will fix this and refine some of the invariants that are not needed anymore.
2017-02-15Merge PR#314: Miscellaneous fixes for Ocaml warnings.Maxime Dénès
2017-02-15[unicode] Address comments in PR#314.Emilio Jesus Gallego Arias
2017-02-14[safe-string] Switch to buffer to `Bytes`Emilio Jesus Gallego Arias
2017-02-14[safe-string] Use `String.init` to build string.Emilio Jesus Gallego Arias
2017-02-14[misc] Remove unused binding.Emilio Jesus Gallego Arias
2017-02-14Merge PR#253: Sort Search results by relevanceMaxime Dénès
2017-02-14Test-suite: output of SearchArnaud Spiwack
Fix the ordering of the results in the output of Search to correspond to the "priority" ordering.
2017-02-13Merge PR#349: Proofview: tclINDEPENDENTLMaxime Dénès
2017-02-10Proofview: tclINDEPENDENTLEnrico Tassi
2017-02-09Turning an anomaly on 'pat into a proper "unsupported" error message.Hugo Herbelin
2017-02-09Fixing bug #5346 (an unimplemented application of 'pat).Hugo Herbelin
2017-02-08Merge PR#405: Type cleanup in `Metasyntax`Maxime Dénès
2017-02-08Merge PR#393: Replace Typeops with Fast_typeopsMaxime Dénès
2017-02-07Revert "Extraction: avoid deprecated functions of module String"Pierre Letouzey
This reverts commit 69c4e7cfa0271f024b2178082e4be2e3ca3be263. String.capitalize_ascii are only available for ocaml >= 4.03, sorry...
2017-02-07Extraction cosmetic: no whitespaces in printing empty modulesPierre Letouzey
2017-02-07Extraction: remove the "print to devnull" hack now that pp isn't lazy anymorePierre Letouzey
2017-02-07Extraction: avoid deprecated functions of module StringPierre Letouzey
- A few tweaks of string are now done via the Bytes module - lots of String.capitalize_ascii and co
2017-02-07Extraction: simplify the generated code for difficult name conflictsPierre Letouzey
No more pp_alias_spec et pp_alias_decl. Instead, we use "include" and "module type of". The extracted code might hence need OCaml 3.12 (quite rarely)
2017-02-07Extraction : get_duplicates (via option) instead of check_duplicates (via ↵Pierre Letouzey
Not_found) This clarifies the execution flow
2017-02-07configure: avoid deprecated warningsPierre Letouzey
2017-02-07Extraction: fix complexity issue #5310Pierre Letouzey
A double call to pp_module_type inside Ocaml.pp_specif was causing an complexity blowup when pretty-printing heavily modular extracted code. I wasn't able to figure out why this double call is there. It could be the leftover of some intermediate work in 2007 before commit 350398eae (which introduced global printing phases Pre/Impl/Intf). Anyway I'm reasonably sure that today these two pp_module_type calls produce the exact same pretty-printed signature (even if there's a large bunch of imperative states around). Moreover, this duplicated signature is actually slightly wrong: when we alias a module M with a unambiguous name like Coq__123, the type of Coq__123 should not be an exact copy of the type of M, but rather a "strengthened" version of it (with equality between inductive types). So the best solution is now to use this funny feature of OCaml introduced in 3.12 : module Coq__123 : module type of struct include M end This "module type of struct include" is slightly awkward, but short, correct, and trivial to produce :-). And I doubt anybody will object to the (rare) use of some 3.12 features in extracted code of 2017...
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 09:20:39 +0000