| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-10-23 | Fixing order of declarations in the function which compacts variables | Hugo Herbelin | |
| of same type in a context. | |||
| 2014-10-23 | Fixing clash in output test-suite Cases. | Hugo Herbelin | |
| 2014-10-23 | Taking into account factorization of consecutive names of same types | Hugo Herbelin | |
| in goal context. Note: printing of a declaration was previously done in the context made of the preceding segment of hypotheses, while now it is made in the full context of all hyps (those coming before and after the hyp being printed). As a consequence, constants which could be confused with a variable in the context are now always qualified even if the conflicting variable name is coming later. But why not, that looks somehow more uniform like this. | |||
| 2014-10-23 | fix parsing of ---- +++++ ***** in CoqIDE | Enrico Tassi | |
| 2014-10-23 | Monad: change the error managing of two-list combinators. | Arnaud Spiwack | |
| Otherwise I risked catching errors from the argument functions when I wanted to catch size mismatch to add information to errors. | |||
| 2014-10-23 | Evd.future_goals: forgot to revert the list in two places. | Arnaud Spiwack | |
| 2014-10-23 | Proofview: forgot to change an exception after refactoring in ( ↵ | Arnaud Spiwack | |
| 9f51aafebd5f3a00dabfe056772a300830b3c430 ) | |||
| 2014-10-22 | Bugfix 3604 : more robust Unix.lockf | Frédéric Besson | |
| 2014-10-22 | Fixing typo in output test Notations. | Hugo Herbelin | |
| 2014-10-22 | Pushing Pierre's factorization of names in goal context printing from | Hugo Herbelin | |
| coqide to coqtop. (Joint work with Pierre) | |||
| 2014-10-22 | Removing an unused variant of Context.fold_named_context_reverse. | Hugo Herbelin | |
| 2014-10-22 | CoqIDE: fix parsing of multicharacter bullets | Enrico Tassi | |
| 2014-10-22 | Specializing tclBREAK so that it can choose the return exception in case | Pierre-Marie Pédrot | |
| of a break. | |||
| 2014-10-22 | Make rint_location_in_file resilient to Cd (close 3630) | Enrico Tassi | |
| Cd can make the relative path of the opened file wrong, and hence not available anymore when we reopen it to compute the line number. | |||
| 2014-10-22 | Fix the way lexeme start is computed (Close 3737) | Enrico Tassi | |
| 2014-10-22 | Goal printing made uniform: always done in STM (close 3585) | Enrico Tassi | |
| Goal printing was partially broken. Some commands in vernacentries were printing, but not all of them. Moreover an unlucky combination of `Flags.verbosely (fun () -> interp "Set Silent")` was making the silent flag not settable anymore. Now STM always print the open goals after a command when run in interactive mode via coqtop or emacs. More modern GUI do ask for the goals. | |||
| 2014-10-22 | Move 'Arguments: clear implicits' to 2.7.4 (Close 2891) | Enrico Tassi | |
| 2014-10-22 | Fix test-suite for #2729. | Maxime Dénès | |
| Was always failing due to an incorrect use of Ltac's or. | |||
| 2014-10-22 | Fix missing lift in VM and native compiler (second part of #2729). | Maxime Dénès | |
| Was occurring in the parameters of constructors when reifying a dependent pattern matching return predicate. Note: this does not affect the kernel, only the pretyper. | |||
| 2014-10-22 | Refine tactic: simplify the conclusion only at the end of the tactic. | Arnaud Spiwack | |
| It was the intended semantics from the beginning. I just wrote it wrong. Spotted by Hugo, fix by Hugo. | |||
| 2014-10-22 | Oversight in ce260a0db279ce09dda70e079ae3c35b49f05ec4 (Proper scoping of ↵ | Arnaud Spiwack | |
| future goals). Fixes #3757. Thanks to Hugo for helping pinpoint the issue. | |||
| 2014-10-22 | Remove an unnecessary use of [Proofview.Unsafe.tclEVARS] in [convert_concl]. | Arnaud Spiwack | |
| 2014-10-22 | EqdepFacts: generalize statements which were wrongly restricted to Prop. | Arnaud Spiwack | |
| 2014-10-22 | CHANGES: makes explicit the incompatibily introduced by the use of ↵ | Arnaud Spiwack | |
| Ltac-defined names in term binders. Closes #3747. | |||
| 2014-10-22 | Fixing an evar leak in pattern-matching compilation (#3758). | Hugo Herbelin | |
| 2014-10-22 | Fixing what really looks like a bug in the initial implementation of | Hugo Herbelin | |
| coqdoc links for modules (#3756). | |||
| 2014-10-22 | Supporting Greek and Coptic (U0370) as first letter of coqdoc identifiers. | Hugo Herbelin | |
| 2014-10-22 | Fixing typo absorption (bug #3751). | Hugo Herbelin | |
| 2014-10-22 | Proofview: documentation and re-ordering. | Arnaud Spiwack | |
| 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-22 | Make names in [Proofview_monad] more uniform. | Arnaud Spiwack | |
| ret -> return, bind -> (>>=), etc… So that monads expose a [Monad.S] signature. Also Proofview now exposes the [Monad.S] signature directly rather than in a [Monad.S] subdirectory. | |||
| 2014-10-22 | Proofview: remove and inline [on_advance] function. | Arnaud Spiwack | |
| [on_advance] gave almost no gain in readability, while costing a closure. | |||
| 2014-10-22 | Proofview: add a lens for the evar_map and factor some code. | Arnaud Spiwack | |
| 2014-10-22 | Proofview: use an iter-like combinator rather than a fold_left-like one for ↵ | Arnaud Spiwack | |
| dispatch. Leads to clearer an more efficient code. | |||
| 2014-10-22 | An additional [List.iter] monadic combinator. | Arnaud Spiwack | |
| 2014-10-22 | Add more primitives to the [Monad.Make] arguments. | Arnaud Spiwack | |
| For optimisation purposes. | |||
| 2014-10-22 | Improve readability the "lenses" in Proofview, using interfaces. | Arnaud Spiwack | |
| 2014-10-22 | Proofview: clean up code a little. | Arnaud Spiwack | |
| 2014-10-22 | Proofview: move [list_goto] to the [CList] module. | Arnaud Spiwack | |
| It is, after all, a generic function about lists. | |||
| 2014-10-22 | Proofview: replace the functions iter_list and iter_list2 by generic monadic ↵ | Arnaud Spiwack | |
| combinators. | |||
| 2014-10-22 | Add a two-list monadic fold_left iterator. | Arnaud Spiwack | |
| 2014-10-22 | Small optimisation in the monadic list combinators. | Arnaud Spiwack | |
| The monadic bind can be costly, so sparing a few can be worth it. Therefore I unrolled the last element of the recursions. I took the opportunity to do some loop unrolling, which is probably more useful for map combinators than for fold. | |||
| 2014-10-22 | Factor module signatures. | Arnaud Spiwack | |
| 2014-10-22 | Proofview: clean up commented out code. | Arnaud Spiwack | |
| 2014-10-22 | Proofview: remove a redundant primitive. | Arnaud Spiwack | |
| 2014-10-22 | Proofview: move more functions to the Unsafe module. | Arnaud Spiwack | |
| 2014-10-22 | Proofview: split [V82] module into [Unsafe] and [V82]. | Arnaud Spiwack | |
| The Unsafe module is for unsafe tactics which cannot be done without anytime soon. Whereas V82 indicates a function which we want to get rid of and that shouldn't be used in a new function. | |||
| 2014-10-22 | Proofview.mli: no more reference to Goal.goal. | Arnaud Spiwack | |
| 2014-10-22 | Proofview: factor init and dependent_init. | Arnaud Spiwack | |
| 2014-10-22 | Remove unused functions for side effects. | Arnaud Spiwack | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |