| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-06-07 | Add is_ind, is_constructor, is_proj | Jason Gross | |
| 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. | |||
| 2016-05-04 | Do not generate generic arguments for data which only requires toplevel values. | Pierre-Marie Pédrot | |
| 2016-05-04 | More toplevel value representation sharing. | Pierre-Marie Pédrot | |
| 2016-05-04 | Moving the Val module to Geninterp. | Pierre-Marie Pédrot | |
| 2016-05-04 | Simplifying the code of Tacinterp. | Pierre-Marie Pédrot | |
| 2016-05-04 | Getting rid of the Geninterp.generic_interp function. | Pierre-Marie Pédrot | |
| 2016-05-04 | Switching to an untyped toplevel representation for Ltac values. | Pierre-Marie Pédrot | |
| 2016-05-02 | Generate parsing rules for ML tactics in the same order as before a7917a32. | Pierre-Marie Pédrot | |
| Once again showing the fragility of the parsing engine, commit a7917a32 reversed the relative order of the declaration of parsing rules for tactics declared through TACTIC EXTEND. There is probably no good order at all, but for retrocompatibility, this patch enforces the original one. | |||
| 2016-05-02 | Useless code in Tacentries. | Pierre-Marie Pédrot | |
| 2016-04-27 | Revert "In the short term, stronger invariant on the syntax of TacAssert, what" | Hugo Herbelin | |
| This reverts commit bde36d4b00185065628324d8ca71994f84eae244. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |