| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-04-09 | A small test of Print Ltac. | Hugo Herbelin | |
| 2016-04-09 | Removing extra spaces in printing arguments of VERNAC EXTEND. | Hugo Herbelin | |
| 2016-04-09 | Removing automatic printing of leading space in auto_using and | Hugo Herbelin | |
| hintbases so that it does not put extra space when auto is defined as a TACTIC EXTEND. | |||
| 2016-04-09 | Re-add printer for tacdef_body so that Ltac definitions are printed by ↵ | Hugo Herbelin | |
| pr_vernac. | |||
| 2016-04-09 | Simplifying code for printing VERNAC EXTEND. | Hugo Herbelin | |
| 2016-04-09 | Fixing extra space in printing inductive types with no explicit type given. | Hugo Herbelin | |
| 2016-04-09 | In pr_clauses, do not print a leading space by default so that it can | Hugo Herbelin | |
| be used in the generic printer for tactics. Allows e.g. to print "symmetry in H" correctly after its move to TACTIC EXTEND. | |||
| 2016-04-09 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-04-08 | Added compatibility coercions from Specif.v which were present in Coq 8.4. | Hugo Herbelin | |
| 2016-04-08 | Fixing a source of inefficiency and an artificial dependency in the | Daniel de Rauglaudre | |
| printer in the congruence tactic. Debugging messages were always built even when not in the verbose mode of congruence. | |||
| 2016-04-08 | Fixing printing of toplevel values. | Pierre-Marie Pédrot | |
| This is not perfect yet, in particular the whole precedence system is a real mess, as there is a real need for tidying up the Pptactic implementation. Nonetheless, printing toplevel values is only used for debugging purposes, where an ugly display is better than none at all. | |||
| 2016-04-08 | Fixing printing of Tactic Notations with tactic arguments. | Pierre-Marie Pédrot | |
| 2016-04-07 | Allow to unset the refinement mode of Instance in ML | Matthieu Sozeau | |
| Falling back to the global setting if not given. Useful to make Add Morphism fail correctly when the given proof terms are incomplete. Adapt test-suite file #2848 accordingly. | |||
| 2016-04-07 | Fixing an incorrect use of prod_appvect on a term which was not a | Hugo Herbelin | |
| product in setoid_rewrite. Backport of d670c6b6ce from trunk. | |||
| 2016-04-07 | Merge PR#152: Add -compat 8.4 econstructor tactics, and tests | Maxime Dénès | |
| 2016-04-07 | An example which failed in 8.5 and that d670c6b6 fixes. | Hugo Herbelin | |
| Thanks to Matthieu for the example. | |||
| 2016-04-07 | Use -win32 and -win64 suffixes for installer name on Windows. | Maxime Dénès | |
| 2016-04-05 | Add -compat 8.4 econstructor tactics, and tests | Jason Gross | |
| Passing `-compat 8.4` now allows the use of `econstructor (tac)`, as in 8.4. | |||
| 2016-04-05 | Fix bug #4656 | Jason Gross | |
| I introduced this bug in 4c078b0362542908eb2fe1d63f0d867b339953fd; Coq.Init.Notations.constructor does not take any arguments. | |||
| 2016-04-04 | Update Coq84.v | Jason Gross | |
| We no longer need to redefine `refine` (it now shelves by default). Also clean up `constructor` a bit. | |||
| 2016-04-04 | Add compatibility Nonrecursive Elimination Schemes | Jason Gross | |
| 2016-04-04 | Fix after merge, the revert of Bind Scope applies to trunk only. | Matthieu Sozeau | |
| 2016-04-04 | Merge remote-tracking branch 'origin/pr/78' into trunk: | Maxime Dénès | |
| An .emacs-ready elisp snippet to parse location of Anomaly backtraces and jump to them conveniently from the Emacs *compilation* output. | |||
| 2016-04-04 | Merge branch 'trunk' of git+ssh://scm.gforge.inria.fr/gitroot/coq/coq into trunk | Matej Kosik | |
| 2016-04-04 | Merging "https://github.com/coq/coq/pull/94", i.e. "Traversal of inductive ↵ | Matej Kosik | |
| defs in Print Assumptions" | |||
| 2016-04-04 | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq ↵ | Matthieu Sozeau | |
| into JasonGross-trunk-function_scope | |||
| 2016-04-04 | Merge branch 'linear-comparison' of https://github.com/aspiwack/coq into ↵ | Matthieu Sozeau | |
| aspiwack-linear-comparison Fixing a -1 -> +1 typo | |||
| 2016-04-03 | Fixing the "No applicable tactic" non informative error message | Hugo Herbelin | |
| regression on apply. | |||
| 2016-04-01 | Getting rid of the "_mods" parsing entry. | Pierre-Marie Pédrot | |
| It was only used by setoid_ring for the Add Ring command, and was easily replaced by a dedicated argument. Moreover, it was of no use to tactic notations. | |||
| 2016-03-31 | Providing an API to access the parsing engine summary in a first-class way. | Pierre-Marie Pédrot | |
| Instead of hardwiring a few special cases in Egramcoq, we allow the grammar state to contain arbitrary data structures. This permits to extend the parsing engine while retaining the synchronization with the global state, e.g. for use in plugins. | |||
| 2016-03-31 | Adding a test for bug #1850. | Pierre-Marie Pédrot | |
| 2016-03-31 | Moving the code handling tactic notations to Tacentries. | Pierre-Marie Pédrot | |
| 2016-03-31 | Abstracting away the Summary-synchronized grammar-modifying commands. | Pierre-Marie Pédrot | |
| We provide an API so that external code such as plugins can define grammar extensions synchronized with the summary. This API is not perfect yet and is a mere abstraction of the current behaviour. In particular, it expects the user to modify the parser in an imperative way. | |||
| 2016-03-31 | Moving the Tactic Notation entry parser from Pcoq to Tacentries. | Pierre-Marie Pédrot | |
| 2016-03-30 | Ensuring that the type of base generic arguments contain triples. | Pierre-Marie Pédrot | |
| 2016-03-30 | Removing dead code in Genarg. | Pierre-Marie Pédrot | |
| 2016-03-30 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-03-29 | Update version number for 8.5pl1 | Maxime Dénès | |
| 2016-03-28 | Fixing an incorrect use of prod_appvect on a term which was not a | Hugo Herbelin | |
| product in setoid_rewrite. Before commit e8c47b652, it was raising an error which has been turned to an anomaly. This impacted Compcert where the former error was (apparently) caught so that setoid_rewrite was returning back to ordinary rewrite. | |||
| 2016-03-28 | Updating .gitignore. | Pierre-Marie Pédrot | |
| 2016-03-28 | Fixing an evar leak in Rewrite introduced by 968dfdb15. | Pierre-Marie Pédrot | |
| 2016-03-28 | Was too restrictive in syntactic definitions, not imagining that they | Hugo Herbelin | |
| could be used with arguments which are binding variables, as was done in ssrfun.v. | |||
| 2016-03-25 | Univs: fix get_current_context (bug #4603, part I) | Matthieu Sozeau | |
| Return an evar_map with the right universes, when there are no focused subgoals or the proof is finished. | |||
| 2016-03-25 | Moving back some tactics not essentially related to Ltac into the tactics/ ↵ | Pierre-Marie Pédrot | |
| folder. | |||
| 2016-03-25 | Moving Autorewrite back to tactics/. | Pierre-Marie Pédrot | |
| 2016-03-25 | Making Autorewrite independent from Ltac. | Pierre-Marie Pédrot | |
| 2016-03-25 | Moving Eqdecide to tactics/. | Pierre-Marie Pédrot | |
| 2016-03-25 | Making Eqdecide independent of Extratactics. | Pierre-Marie Pédrot | |
| 2016-03-25 | Moving Eauto and Class_tactics to tactics/. | Pierre-Marie Pédrot | |
| 2016-03-25 | Moving type_uconstr to Pretyping. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |