aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Collapse)AuthorAge
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Removing some compatibility layers in Tactics.Gravatar Pierre-Marie Pédrot2016-05-17
|
* Removing the old refine tactic from the Tactics module.Gravatar Pierre-Marie Pédrot2016-05-17
| | | | | | It is indeed confusing, as it has little to do with the proper refine defined in the New submodule. Legacy code relying on it should call the Logic or Tacmach modules instead.
* Put the "move" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-17
|
* Put the "change" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
|
* Put the "specialize_eq" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
|
* Put the "generalize dependent" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
|
* Put the "generalize" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
|
* Put the "cofix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
|
* Put the "*_cast_no_check" tactics in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
|
* Put the "exact" family of tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
|
* Put the "fix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
|
* Put the "exact_constr" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
|
* Put the "clear" tactic into the monad.Gravatar Pierre-Marie Pédrot2016-05-16
|
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
|
* Normalizing the names of dynamic types to follow a typ_* scheme.Gravatar Pierre-Marie Pédrot2016-05-04
|
* Removing external uses of Val.inject and making Geninterp.interp return Val.tGravatar Pierre-Marie Pédrot2016-05-04
|
* Removing the Value.of_* API for parameterized types.Gravatar Pierre-Marie Pédrot2016-05-04
| | | | | Although still working, it is now bad practice to use it, and it is not widely spread anyway.
* Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
|
* Getting rid of the Geninterp.generic_interp function.Gravatar Pierre-Marie Pédrot2016-05-04
|
* Switching to an untyped toplevel representation for Ltac values.Gravatar Pierre-Marie Pédrot2016-05-04
|
* Moving Ftactic and Geninterp to the engine folder.Gravatar Pierre-Marie Pédrot2016-05-04
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\
| * In Regular Subst Tactic mode, ensure that the order of hypotheses isGravatar Hugo Herbelin2016-05-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | preserved, which is a source of incompatibilities w.r.t. released 8.5 but which looks to me to be the only possible canonical behavior. This is I believe a better behavior than the Regular Subst Tactic behavior in the released 8.5 and 8.5pl1. There, the order of hypotheses in which substitutions happened was respected, but their interleaving with other hypotheses was not respected. So, I consider this to be a fix to the "Regular Subst Tactic" mode. Also added a more detailed "specification" of the "Regular" behavior of "subst" in the reference manual.
| * Fix bug #4707: clearbody much slower in 8.5pl1.Gravatar Pierre-Marie Pédrot2016-05-03
| | | | | | | | | | We only retype hypotheses and conclusion when they do depend on the cleared identifier. This saves a lot of time.
* | Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit bde36d4b00185065628324d8ca71994f84eae244.
* | In the short term, stronger invariant on the syntax of TacAssert, whatGravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | allows for a simpler re-printing of assert. Also fixing the precedence for printing "by" clause.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-09
|\|
| * Allow to unset the refinement mode of Instance in MLGravatar Matthieu Sozeau2016-04-07
| | | | | | | | | | | | 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.
| * Fixing an incorrect use of prod_appvect on a term which was not aGravatar Hugo Herbelin2016-04-07
| | | | | | | | | | | | product in setoid_rewrite. Backport of d670c6b6ce from trunk.
| * Fixing the "No applicable tactic" non informative error messageGravatar Hugo Herbelin2016-04-03
| | | | | | | | regression on apply.
* | Moving Autorewrite back to tactics/.Gravatar Pierre-Marie Pédrot2016-03-25
| |
* | Moving Eqdecide to tactics/.Gravatar Pierre-Marie Pédrot2016-03-25
| |
* | Moving Eauto and Class_tactics to tactics/.Gravatar Pierre-Marie Pédrot2016-03-25
| |
* | Creating a dedicated ltac/ folder for Hightactics.Gravatar Pierre-Marie Pédrot2016-03-21
| |
* | Moving Tacsubst to hightactics.Gravatar Pierre-Marie Pédrot2016-03-20
| |
* | Relying on generic arguments to represent Extern hints.Gravatar Pierre-Marie Pédrot2016-03-20
| |
* | Adding a new Ltac generic argument for forced tactics returing unit.Gravatar Pierre-Marie Pédrot2016-03-20
| |
* | Moving Tacenv to Hightactics.Gravatar Pierre-Marie Pédrot2016-03-20
| |
* | Moving Tactic_debug to Hightactic.Gravatar Pierre-Marie Pédrot2016-03-20
| |
* | Making Evarutil independent from Reductionops.Gravatar Pierre-Marie Pédrot2016-03-20
| |
* | Moving Refine to its proper module.Gravatar Pierre-Marie Pédrot2016-03-20
| |
* | Making Proofview independent of Logic.Gravatar Pierre-Marie Pédrot2016-03-20
| |
* | Fixing the classification of Tactic Notation.Gravatar Pierre-Marie Pédrot2016-03-20
| |
| * Fixing bug #4630: Some tactics are 20x slower in 8.5 than 8.4.Gravatar Pierre-Marie Pédrot2016-03-20
| | | | | | | | | | | | The interpretation of arguments of tactic notations were normalizing the goal beforehand, which incurred an important time penalty. We now do this argumentwise which allows to save time in frequent cases, notably tactic arguments.
* | Moving Tacintern to Hightactics.Gravatar Pierre-Marie Pédrot2016-03-20
| |
* | Moving the Ltac definition command to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
| |
* | Moving the tactic related code from Metasyntax to a new file.Gravatar Pierre-Marie Pédrot2016-03-20
| |
* | Moving Print Ltac to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
| |
* | Moving Tactic Notation to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 17:42:45 +0000