aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
2016-06-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-06-11Fixing a try with in apply that has become too weak in 8.5.Hugo Herbelin
Don't know however what should be the right guard to this try. Now using catchable_exception, but even in 8.4, Failure was caught, which is strange.
2016-06-09Adding a bit of documentation in the mli.Pierre-Marie Pédrot
2016-06-09Improve the interpretation scope of arguments of an ltac match.Hugo Herbelin
Now, type_scope is consistently used whether it is an hypothesis or the conclusion, and consistently not used when in "context". The question of a compatibility support, e.g., as suggested by Jason, using a scope is still open though. See reports #3050 and #4398.
2016-06-07Fixing #4787 (Unset Bracketing Last Introduction Pattern not working).Hugo Herbelin
2016-06-05Removing the Q_constr file.Pierre-Marie Pédrot
2016-06-05Moving Hipattern to a regular ML file.Pierre-Marie Pédrot
2016-06-05Removing PATTERN uses in Hipattern.Pierre-Marie Pédrot
2016-06-02Add a synonymous Set Debug Typeclasses for Set Typeclasses Debug, for ↵Hugo Herbelin
uniformity.
2016-06-01Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-31Revert "Rename Lexer -> CLexer."Pierre-Marie Pédrot
This reverts commit a66b57ba4bba866bb626bde2b6fe3b762347eb3e.
2016-05-31Feedback cleanupEmilio 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-29Fix bug #4746: Anomaly: Evar ?X10 was not declared.Pierre-Marie Pédrot
Some dubious evarmap manipulation is going on in destruct because of the use of clenv primitives. Here, building a clenv was introducing new evars that were not taken into account in the remainder of the tactic. We plug them back using a local workaround. Eventually, this code should be replaced by an evar-based one, but meanwhile, we rely on what is probably a hack.
2016-05-26rewrite/Univs: Fix bug # 4498.Matthieu Sozeau
2016-05-23Hints/Univs: fix bug #4628 anomaliesMatthieu Sozeau
Fix handling of non-polymorphic hints built from polymorphic values, or simply producing new universes. We have to record the side effects of global hints built from constrs which are not polymorphic when they declare global universes, which might need to be discharged at the end of sections too. Also issue a warning when a Hint is declared for a polymorphic reference but the Hint isn't polymorphic itself (this used to produce an anomaly). For [using] hints, treat all lemmas as polymorphic, refreshing their universes at each use, as is done for their existentials (also used to produce an anomaly).
2016-05-17Removing some compatibility layers in Tactics.Pierre-Marie Pédrot
2016-05-17Removing the old refine tactic from the Tactics module.Pierre-Marie Pédrot
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.
2016-05-17Put the "move" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "change" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "specialize_eq" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "generalize dependent" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "generalize" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "cofix" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "*_cast_no_check" tactics in the monad.Pierre-Marie Pédrot
2016-05-16Put the "exact" family of tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "fix" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "exact_constr" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "clear" tactic into the monad.Pierre-Marie Pédrot
2016-05-09Rename Lexer -> CLexer.Pierre-Marie Pédrot
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-05-04Normalizing the names of dynamic types to follow a typ_* scheme.Pierre-Marie Pédrot
2016-05-04Removing external uses of Val.inject and making Geninterp.interp return Val.tPierre-Marie Pédrot
2016-05-04Removing 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-04Moving the Val module to Geninterp.Pierre-Marie Pédrot
2016-05-04Getting rid of the Geninterp.generic_interp function.Pierre-Marie Pédrot
2016-05-04Switching to an untyped toplevel representation for Ltac values.Pierre-Marie Pédrot
2016-05-04Moving Ftactic and Geninterp to the engine folder.Pierre-Marie Pédrot
2016-05-04Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-03In Regular Subst Tactic mode, ensure that the order of hypotheses isHugo Herbelin
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.
2016-05-03Fix bug #4707: clearbody much slower in 8.5pl1.Pierre-Marie Pédrot
We only retype hypotheses and conclusion when they do depend on the cleared identifier. This saves a lot of time.
2016-04-27Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Hugo Herbelin
This reverts commit bde36d4b00185065628324d8ca71994f84eae244.
2016-04-27In the short term, stronger invariant on the syntax of TacAssert, whatHugo Herbelin
allows for a simpler re-printing of assert. Also fixing the precedence for printing "by" clause.
2016-04-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-07Allow to unset the refinement mode of Instance in MLMatthieu 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-07Fixing an incorrect use of prod_appvect on a term which was not aHugo Herbelin
product in setoid_rewrite. Backport of d670c6b6ce from trunk.
2016-04-03Fixing the "No applicable tactic" non informative error messageHugo Herbelin
regression on apply.
2016-03-25Moving Autorewrite back to tactics/.Pierre-Marie Pédrot
2016-03-25Moving Eqdecide to tactics/.Pierre-Marie Pédrot
2016-03-25Moving Eauto and Class_tactics to tactics/.Pierre-Marie Pédrot
2016-03-21Creating a dedicated ltac/ folder for Hightactics.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 17:47:37 +0000