aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac/tacinterp.ml
Commit message (Expand)AuthorAge
* profile_ltac: rewritten to be purely functional and STM awareGravatar Enrico Tassi2016-09-05
* Moving log of "TacReduce"/"reduce" to Tactics.reduce so that internalGravatar Hugo Herbelin2016-09-01
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* Do not evar-normalize goals when interpreting some hardwired genargs.Gravatar Pierre-Marie Pédrot2016-06-20
* Exporting a generic argument induction_arg. As a consequence,Gravatar Hugo Herbelin2016-06-18
* Adding eintros to respect the e- prefix policy.Gravatar Hugo Herbelin2016-06-18
* Fixing space in an error message.Gravatar Hugo Herbelin2016-06-16
* A stronger invariant on the syntax of TacAssert, what allows for aGravatar Hugo Herbelin2016-06-16
* Merge 'pr/191' into trunkGravatar Enrico Tassi2016-06-16
|\
* \ Merge PR #100: fresh now accepts more things than just identifiers.Gravatar Pierre-Marie Pédrot2016-06-16
|\ \
| | * Goal selectors are now tacticals and can be used as such.Gravatar Cyprien Mangin2016-06-14
| |/ |/|
* | Revert "Strip some trailing spaces"Gravatar Pierre-Marie Pédrot2016-06-13
* | LtacProf for Coq trunkGravatar Jason Gross2016-06-05
* | Strip some trailing spacesGravatar Jason Gross2016-06-05
* | Removing "rename" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* | Removing "exact" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* | Removing "intro" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* | Removing "double induction" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* | Add a synonymous Set Debug Ltac for Set Ltac Debug, for uniformity.Gravatar Hugo Herbelin2016-06-02
* | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* | Put the "change" 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 "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
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
* | 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 useless generic arguments.Gravatar Pierre-Marie Pédrot2016-05-04
* | Interpretation function can return any untyped value.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
* | Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
* | Simplifying the code of Tacinterp.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
* | Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Gravatar Hugo Herbelin2016-04-27
* | Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Gravatar Hugo Herbelin2016-04-27
* | Revert "Passing around the precedence to the generic printer so as to solve"Gravatar Hugo Herbelin2016-04-27
* | Revert "When interpreting "match goal with ... end" in ltac, expand evars by"Gravatar Hugo Herbelin2016-04-27
* | Revert "Fixing space in an error message."Gravatar Hugo Herbelin2016-04-27
* | Revert "Revert "Honor parsing and printing levels for tactic entry in TACTIC ...Gravatar Hugo Herbelin2016-04-27
* | Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Gravatar Hugo Herbelin2016-04-27
* | Fixing space in an error message.Gravatar Hugo Herbelin2016-04-27
* | When interpreting "match goal with ... end" in ltac, expand evars byGravatar Hugo Herbelin2016-04-27
* | Passing around the precedence to the generic printer so as to solveGravatar Hugo Herbelin2016-04-27
* | Honor parsing and printing levels for tactic entry in TACTIC EXTEND andGravatar Hugo Herbelin2016-04-27
* | In the short term, stronger invariant on the syntax of TacAssert, whatGravatar Hugo Herbelin2016-04-27
* | Attempt to slightly improve abusive "Collision between boundGravatar Hugo Herbelin2016-04-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-27 10:24:48 +0000