| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-01-12 | Update headers. | Maxime Dénès | |
| 2015-01-08 | Avoiding introducing yet another convention in naming files. | Hugo Herbelin | |
| 2014-12-30 | Compatibility ocaml 3.12. | Hugo Herbelin | |
| 2014-12-30 | Minor fixes for the win32 installer | Enrico Tassi | |
| 2014-12-19 | Win32: fix installer | Enrico Tassi | |
| Still unsure about .o file (should they be shipped for the native_compute machinery or .cmxs suffice?) | |||
| 2014-12-16 | More printers for ltac signatures. | Hugo Herbelin | |
| 2014-12-09 | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey | |
| 2014-12-07 | Removing import of Proofview in debugger because its module Goal hides | Hugo Herbelin | |
| the import of goal.ml and, afaiu, ocaml does not provide a way to refer to a shadowed module. | |||
| 2014-12-05 | More printers in tracer. | Hugo Herbelin | |
| 2014-12-04 | Reactivating option "Set Printing Existential Instances" for asking printing ↵ | Hugo Herbelin | |
| full instances. | |||
| 2014-11-27 | Reverting the following block of three commits: | Hugo Herbelin | |
| - Registering strict implicit arguments systematically (35fc7d728168) - Experimenting always forcing convertibility on strict implicit arguments (a1a6d7b99eef5e6) - Fixing Coq compilation (894a3d16471) Systematically computing strict implicit arguments can lead to big computations, so I suspend this attempt, waiting for improved computation of implicit arguments, or alternative heuristics going toward having more conversion in rewrite. | |||
| 2014-11-26 | Experimenting always forcing convertibility on strict implicit arguments | Hugo Herbelin | |
| in tactic unification. | |||
| 2014-11-23 | Add printer for transparent state for ocamldebug. | Hugo Herbelin | |
| 2014-11-22 | Specific printer of Evar.Set.t for ocamldebug + more information in | Hugo Herbelin | |
| a UserError to ease debugging. | |||
| 2014-11-15 | Adding a pretty-printing style library. | Pierre-Marie Pédrot | |
| 2014-11-10 | Plug the dynamic tags in the Richpp mechanism. | Pierre-Marie Pédrot | |
| 2014-10-31 | More "open" by default for trace debugging. | Hugo Herbelin | |
| 2014-10-22 | Split [Proofview] into a file where the basic operations on the state are ↵ | Arnaud Spiwack | |
| defined and the file providing the primitives. The datatypes are defined in [Proofview_monad], previous [Proofview_monad] is now called [Logic_monad] since it is more generic since the refactoring. | |||
| 2014-10-15 | Fix ill-typed debugging function | Matthieu Sozeau | |
| 2014-10-13 | Adding printers for ppproofview. | Hugo Herbelin | |
| 2014-10-10 | Add debug printers for projections, fix printing of evar constraints | Matthieu Sozeau | |
| and unsatisfiable constraints which were not done in the right environment. | |||
| 2014-10-09 | Adding printer for named_context_val and Goal.goal in debugger. | Hugo Herbelin | |
| 2014-10-07 | Adding a printer for hints. | Hugo Herbelin | |
| 2014-10-02 | Fixing interpretation of constr under binders which was broken after | Hugo Herbelin | |
| it became possible to have binding names themselves bound to ltac variables (2fcc458af16b). | |||
| 2014-10-01 | Fixing nice printing of error reporting with ml tactics bound to ltac names. | Hugo Herbelin | |
| 2014-10-01 | Fixing use of arguments renaming in apply which was broken after | Hugo Herbelin | |
| reorganization of apply in d5fece25d8964d5d9fcd55b66164286aeef5fb9f: using renaming also in retyping. | |||
| 2014-09-27 | Index keys instead of simply global references. | Matthieu Sozeau | |
| 2014-09-27 | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau | |
| so as to reproduce correctly the reduction behavior of existing projections, i.e. delta + iota. Make [projection] an abstract datatype in Names.ml, most of the patch is about using that abstraction. Fix unification.ml which tried canonical projections too early in presence of primitive projections. | |||
| 2014-09-19 | win32: embed NSIS for plugin writers | Enrico Tassi | |
| 2014-09-18 | Fix debug printing with primitive projections. | Matthieu Sozeau | |
| Add a flag to indicate if we're in the toplevel or debuggger to not try to retype terms in the wrong environment (and making find_rectype, get_type_of untraceable). This fixes bug #3638 along with the previous commit. | |||
| 2014-09-17 | win32: remove outdated splash screen | Enrico Tassi | |
| The official Coq logo does not work as a splash screen. Simplest fix: no splash screen. | |||
| 2014-09-17 | win32: use subsystem windows on windows (and not console) | Enrico Tassi | |
| This makes the hammer tools/mkwinapp.ml kind of obsolete | |||
| 2014-09-12 | Fix base_include due to change in argument order of env and evar_map | Matthieu Sozeau | |
| 2014-09-12 | Uniformisation of the order of arguments env and sigma. | Hugo Herbelin | |
| 2014-09-12 | Referring to evars by names. Added a parser for evars (but parsing of | Hugo Herbelin | |
| instances still to do). Using heuristics to name after the quantifier name it comes. Also added a "sigma" to almost all printing functions. | |||
| 2014-09-10 | VernacExtend does not dispatch on type anymore. | Pierre-Marie Pédrot | |
| 2014-09-09 | Merge remote-tracking branch 'jason/win32-improvements' into trunk | Enrico Tassi | |
| 2014-09-09 | Bump CoqSDK revision number | Jason Gross | |
| 2014-09-09 | Add a VERBOSE flag to make-sdk-win32 | Jason Gross | |
| For debugging purposes. | |||
| 2014-09-09 | Minor code style cleanup in make-sdk-win32 | Jason Gross | |
| 2014-09-09 | Support 64-bit cygwin | Jason Gross | |
| 2014-09-09 | Support machines that have a full or nonexistant C drive | Jason Gross | |
| 2014-09-09 | Support environments where `find` is Windows' find | Jason Gross | |
| 2014-09-09 | Installer for win improved | Enrico Tassi | |
| - checks for paths containing whitespaces - Coqide has syntax highlighting - does not include the ocaml compiler, since it would not work anyway for the purpose of native compile. For that we really need the whole toolchain, including the C linker/assembler. Hence we should just recommend to install the SDK | |||
| 2014-09-09 | Installer for win32 | Enrico Tassi | |
| Not 100% functional, but coqide works. The native compiler is embedded but: - some path mangling problem prevents it from working even when run via cygwin (like in the build process) - CAMLLIB must be exported to ${COQ}\ocaml\lib to have it run (coq should do it). fix | |||
| 2014-08-26 | Debug RAKAM | Pierre Boutillier | |
| 2014-08-18 | A reorganization of the "assert" tactics (hopefully uniform naming | Hugo Herbelin | |
| scheme, redundancies, possibility of chaining a tactic knowing the name of introduced hypothesis, new proof engine). | |||
| 2014-08-18 | Reorganisation of intropattern code | Hugo Herbelin | |
| - emphasizing the different kinds of patterns - factorizing code of the non-naming intro-patterns Still some questions: - Should -> and <- apply to hypotheses or not (currently they apply to hypotheses either when used in assert-style tactics or apply in, or when the term to rewrite is a variable, in which case "subst" is applied)? - Should "subst" be used when the -> or <- rewrites an equation x=t posed by "assert" (i.e. rewrite everywhere and clearing x and hyp)? - Should -> and <- be applicable in non assert-style if the lemma has quantifications? | |||
| 2014-08-18 | Fixing include of debugger. | Pierre-Marie Pédrot | |
| 2014-08-04 | STM: encapsulate Pp.message in Feedback.feedback | Carst Tankink | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |