aboutsummaryrefslogtreecommitdiff
path: root/ltac/tacinterp.ml
AgeCommit message (Expand)Author
2017-02-01Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-11-07Merge commit 'e6edb33' into v8.6Maxime Dénès
2016-11-07More explicit name for status of unification constraints.Maxime Dénès
2016-10-22Merge branch 'v8.5' into v8.6Hugo Herbelin
2016-09-05profile_ltac: rewritten to be purely functional and STM awareEnrico Tassi
2016-09-01Moving log of "TacReduce"/"reduce" to Tactics.reduce so that internalHugo Herbelin
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-06-20Do not evar-normalize goals when interpreting some hardwired genargs.Pierre-Marie Pédrot
2016-06-18Exporting a generic argument induction_arg. As a consequence,Hugo Herbelin
2016-06-18Adding eintros to respect the e- prefix policy.Hugo Herbelin
2016-06-16Fixing space in an error message.Hugo Herbelin
2016-06-16A stronger invariant on the syntax of TacAssert, what allows for aHugo Herbelin
2016-06-16Merge 'pr/191' into trunkEnrico Tassi
2016-06-16Merge PR #100: fresh now accepts more things than just identifiers.Pierre-Marie Pédrot
2016-06-14Goal selectors are now tacticals and can be used as such.Cyprien Mangin
2016-06-13Revert "Strip some trailing spaces"Pierre-Marie Pédrot
2016-06-05LtacProf for Coq trunkJason Gross
2016-06-05Strip some trailing spacesJason Gross
2016-06-03Removing "rename" from the tactic AST.Pierre-Marie Pédrot
2016-06-03Removing "exact" from the tactic AST.Pierre-Marie Pédrot
2016-06-03Removing "intro" from the tactic AST.Pierre-Marie Pédrot
2016-06-03Removing "double induction" from the tactic AST.Pierre-Marie Pédrot
2016-06-02Add a synonymous Set Debug Ltac for Set Ltac Debug, for uniformity.Hugo Herbelin
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-16Put the "change" 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 "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-09Merge branch 'v8.5'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 useless generic arguments.Pierre-Marie Pédrot
2016-05-04Interpretation function can return any untyped value.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
2016-05-04Moving the Val module to Geninterp.Pierre-Marie Pédrot
2016-05-04Simplifying the code of Tacinterp.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-04-27Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Hugo Herbelin
2016-04-27Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Hugo Herbelin
2016-04-27Revert "Passing around the precedence to the generic printer so as to solve"Hugo Herbelin
2016-04-27Revert "When interpreting "match goal with ... end" in ltac, expand evars by"Hugo Herbelin
2016-04-27Revert "Fixing space in an error message."Hugo Herbelin
2016-04-27Revert "Revert "Honor parsing and printing levels for tactic entry in TACTIC ...Hugo Herbelin
2016-04-27Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Hugo Herbelin
2016-04-27Fixing space in an error message.Hugo Herbelin
2016-04-27When interpreting "match goal with ... end" in ltac, expand evars byHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-13 22:23:25 +0000