| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-06-14 | Merge remote-tracking branch 'origin/pr/173' into trunk | Enrico Tassi | |
| This is the "error resiliency" mode for STM | |||
| 2016-06-14 | Merge branch "LtacProf for trunk" (PR #165). | Pierre-Marie Pédrot | |
| 2016-06-14 | Commenting out debugging code. | Pierre-Marie Pédrot | |
| 2016-06-14 | Correct use of printing primitives. | Pierre-Marie Pédrot | |
| 2016-06-14 | Better coding style (semantics). | Pierre-Marie Pédrot | |
| 2016-06-14 | Better coding style (syntax). | Pierre-Marie Pédrot | |
| 2016-06-14 | Adding Coq headers. | Pierre-Marie Pédrot | |
| 2016-06-14 | Moving back Ltac profiling to the Ltac folder. | Pierre-Marie Pédrot | |
| 2016-06-13 | Revert "Strip some trailing spaces" | Pierre-Marie Pédrot | |
| This reverts commit 45748e4efae8630cc13b0199dfcc9803341e8cd8. | |||
| 2016-06-09 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-06-06 | About printing of traces of failures while calling ltac code. | Hugo Herbelin | |
| An Ltac trace printing mechanism was introduced in 8.4 which was inadvertedly modified by a series of commits such as 8e10368c3, 91f44f1da7a, ... It was also sometimes buggy, iirc, when entering ML tactics which themselves were calling ltac code. It got really bad in 8.5 as in: Tactic Notation "f" constr(x) := apply x. Ltac g x := f x. Goal False. idtac; f I. (* bad location reporting *) g I. (* was referring to tactic name "Top.Top#<>#1" *) which this commit fixes. I don't have a clear idea of what would be the best ltac tracing mechanism, but to avoid it to be broken without being noticed, I started to add some tests. Eventually, it might be worth that an Ltac expert brainstrom on it! | |||
| 2016-06-06 | STM: proof block detection for par: | Enrico Tassi | |
| "par: tac" is a terminator, if it fails we can admit all focused goals and continue. | |||
| 2016-06-06 | STM: proof block detection/error resilience API | Enrico Tassi | |
| This commit introduces the concept of proof blocks that are resilient to errors. They are represented as ErrorBound boxes in the STM document with the topological invariant that they never overlap. The detection and error recovery of ErrorBound boxes is defined outside the STM. One can define a box by providing a function to detect it statically by crawling the parsed document and a function to recover from an error at run time. | |||
| 2016-06-05 | Make Ltac Profiling an setting | Jason Gross | |
| 2016-06-05 | Synchronize the profiler state with the document | Jason Gross | |
| This is suboptimal, because mutation leaves room for subtle bugs, but rewriting @tebbi's code to be functional was a pain, and not something I could figure out how to do easily. I'm working under the assumption that there is no sharing in a single treenode, which I'm not completely sure is valid. That said, a few simple tests seem to indicate that this works as expected. | |||
| 2016-06-05 | LtacProf for Coq trunk | Jason Gross | |
| This add LtacProfiling. Much of the code was written by Tobias Tebbi (@tebbi), and Paul A. Steckler was invaluable in porting the code to Coq v8.5 and Coq trunk. | |||
| 2016-06-05 | Strip some trailing spaces | Jason Gross | |
| 2016-06-05 | Adding the Print Ltac Signature command. | Pierre-Marie Pédrot | |
| 2016-06-03 | Removing "rename" from the tactic AST. | Pierre-Marie Pédrot | |
| 2016-06-03 | Removing "exact" from the tactic AST. | Pierre-Marie Pédrot | |
| 2016-06-03 | Removing "intro" from the tactic AST. | Pierre-Marie Pédrot | |
| Note that this breaks the compatibility, in a beneficial way I believe. Tactics defined in strict mode (i.e. through Ltac foo := ...) may not do an introduction on a local identifier anymore. They must use the "fresh" primitive instead. | |||
| 2016-06-03 | Removing "double induction" from the tactic AST. | Pierre-Marie Pédrot | |
| 2016-06-02 | Add a synonymous Set Debug Ltac for Set Ltac Debug, for uniformity. | Hugo Herbelin | |
| 2016-06-01 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-05-31 | Feedback cleanup | Emilio Jesus Gallego Arias | |
| This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work. | |||
| 2016-05-17 | Put the "move" tactic in the monad. | Pierre-Marie Pédrot | |
| 2016-05-16 | Put the "change" tactic in the monad. | Pierre-Marie Pédrot | |
| 2016-05-16 | Put the "specialize_eq" tactic in the monad. | Pierre-Marie Pédrot | |
| 2016-05-16 | Put the "generalize dependent" tactic in the monad. | Pierre-Marie Pédrot | |
| 2016-05-16 | Put the "generalize" tactic in the monad. | Pierre-Marie Pédrot | |
| 2016-05-16 | Put the "cofix" tactic in the monad. | Pierre-Marie Pédrot | |
| 2016-05-16 | Put the "*_cast_no_check" tactics in the monad. | Pierre-Marie Pédrot | |
| 2016-05-16 | Put the "exact" family of tactic in the monad. | Pierre-Marie Pédrot | |
| 2016-05-16 | Put the "fix" tactic in the monad. | Pierre-Marie Pédrot | |
| 2016-05-16 | Put the "clear" tactic into the monad. | Pierre-Marie Pédrot | |
| 2016-05-16 | Generate more user-readable tactic notation kernel names. | Pierre-Marie Pédrot | |
| This has no influence on user-side, and only makes the life of the debugging developer easier. | |||
| 2016-05-11 | Making the grammar command extend API purely functional. | Pierre-Marie Pédrot | |
| Instead of leaving the responsibility of extending the grammar to the caller, we ask for a list of extensions in the return value of the function. | |||
| 2016-05-11 | Moving the constr empty entry registering to the state-based API. | Pierre-Marie Pédrot | |
| 2016-05-11 | Turning the grammar extend command API into a state-passing one. | Pierre-Marie Pédrot | |
| 2016-05-11 | Moving the grammar summary to Pcoq. | Pierre-Marie Pédrot | |
| 2016-05-10 | AlistNsep token now accepts an arbitrary separator. | Pierre-Marie Pédrot | |
| 2016-05-10 | Removing the Entry module now that rules need not be marshalled. | Pierre-Marie Pédrot | |
| 2016-05-09 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-05-08 | Pass user symbol to tactic notation printers. | Pierre-Marie Pédrot | |
| 2016-05-08 | Removing dead code and unused opens. | Pierre-Marie Pédrot | |
| 2016-05-04 | Normalizing the names of dynamic types to follow a typ_* scheme. | Pierre-Marie Pédrot | |
| 2016-05-04 | Removing useless generic arguments. | Pierre-Marie Pédrot | |
| 2016-05-04 | Interpretation function can return any untyped value. | Pierre-Marie Pédrot | |
| 2016-05-04 | Removing external uses of Val.inject and making Geninterp.interp return Val.t | Pierre-Marie Pédrot | |
| 2016-05-04 | Removing the Value.of_* API for parameterized types. | Pierre-Marie Pédrot | |
| Although still working, it is now bad practice to use it, and it is not widely spread anyway. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |