aboutsummaryrefslogtreecommitdiff
path: root/ltac/tacinterp.ml
AgeCommit message (Expand)Author
2017-02-17Ltac as a plugin.Pierre-Marie Pédrot
2017-02-01Merge branch 'v8.6'Pierre-Marie Pédrot
2017-02-01Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-11-18Merge branch 'v8.6'Pierre-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-24Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-22Merge branch 'v8.5' into v8.6Hugo Herbelin
2016-09-21Merging Stdarg and Constrarg.Pierre-Marie Pédrot
2016-09-15Moving Ltac-specific generic arguments to their own file in the ltac/ folder.Pierre-Marie Pédrot
2016-09-08Making Proof_global terminator generic in external tactics.Pierre-Marie Pédrot
2016-09-08Merge PR #244.Pierre-Marie Pédrot
2016-09-07Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-05profile_ltac: rewritten to be purely functional and STM awareEnrico Tassi
2016-09-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-01Moving log of "TacReduce"/"reduce" to Tactics.reduce so that internalHugo Herbelin
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Remove errorlabstrm in favor of user_errEmilio Jesus Gallego Arias
2016-08-19Unify location handling of error functions.Emilio Jesus Gallego Arias
2016-07-12Renouncing for uniformity to the few instances of pf_interp_* in Tacinterp.Hugo 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:20:11 +0000