aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac
Commit message (Expand)AuthorAge
...
* | Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
| * Goal selectors now use the keyword [only].Gravatar Cyprien Mangin2016-06-30
|/
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* LtacProf reports structured results (pr/209)Gravatar CJ Bell2016-06-20
* Do not evar-normalize goals when interpreting some hardwired genargs.Gravatar Pierre-Marie Pédrot2016-06-20
* Backporting c064fb933 from 8.5 (another regression with Ltac trace report).Gravatar Hugo Herbelin2016-06-18
* Adding an "as" clause to specialize.Gravatar Hugo Herbelin2016-06-18
* Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18
* 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
* par: like all: but in parallelGravatar Enrico Tassi2016-06-17
* Revise syntax of Hint CutGravatar Matthieu Sozeau2016-06-16
* Purely refactoring and code/API cleanup.Gravatar Matthieu Sozeau2016-06-16
* bteauto: a Proofview.tactic for multiple goalsGravatar Matthieu Sozeau2016-06-16
* Implement limited proof search and iterative deepening.Gravatar Matthieu Sozeau2016-06-16
* Typeclasses eauto based on new proof engine,Gravatar Matthieu Sozeau2016-06-16
* Typo in comment.Gravatar Hugo Herbelin2016-06-16
* Fixing space in an error message.Gravatar Hugo Herbelin2016-06-16
* Fixing printing of Register retroknowledge.Gravatar Hugo Herbelin2016-06-16
* Fixing Add Parametric Relation by adding printer for binders.Gravatar Hugo Herbelin2016-06-16
* Fixing missing substitution / printing cases of TacSelect.Gravatar Pierre-Marie Pédrot2016-06-16
* Fixing parsing of constr argument of ltac functions at level 8 in theGravatar Hugo Herbelin2016-06-16
* A stronger invariant on the syntax of TacAssert, what allows for aGravatar Hugo Herbelin2016-06-16
* Merge PR #195: Complete is_* family of term-examining tactics.Gravatar Pierre-Marie Pédrot2016-06-16
|\
* \ Merge 'pr/191' into trunkGravatar Enrico Tassi2016-06-16
|\ \
* \ \ Merge PR #211: Fix a printing typo in LtacProf.Gravatar Pierre-Marie Pédrot2016-06-16
|\ \ \
* \ \ \ Merge PR #100: fresh now accepts more things than just identifiers.Gravatar Pierre-Marie Pédrot2016-06-16
|\ \ \ \
| | | | * Add is_constGravatar Jason Gross2016-06-16
| | * | | Fix another missing newlineGravatar Jason Gross2016-06-16
| | * | | Fix a printing typoGravatar Jason Gross2016-06-16
| |/ / / |/| | |
* | | | Merge remote-tracking branch 'origin/pr/173' into trunkGravatar Enrico Tassi2016-06-14
|\ \ \ \
| | | * | Ident selectors cannot be used inside an Ltac expression.Gravatar Cyprien Mangin2016-06-14
| | | * | Goal selectors are now tacticals and can be used as such.Gravatar Cyprien Mangin2016-06-14
| | | * | Remove the need for brackets in goal selectors.Gravatar Cyprien Mangin2016-06-14
| | | * | Fix usage of Pervasives in goal selectors.Gravatar Cyprien Mangin2016-06-14
| | | * | Fix the pretty-printing of goal range selectors.Gravatar Cyprien Mangin2016-06-14
| | | * | Add goal range selectors.Gravatar Cyprien Mangin2016-06-14
| |_|/ / |/| | |
* | | | Merge branch "LtacProf for trunk" (PR #165).Gravatar Pierre-Marie Pédrot2016-06-14
|\ \ \ \
| * | | | Commenting out debugging code.Gravatar Pierre-Marie Pédrot2016-06-14
| * | | | Correct use of printing primitives.Gravatar Pierre-Marie Pédrot2016-06-14
| * | | | Better coding style (semantics).Gravatar Pierre-Marie Pédrot2016-06-14
| * | | | Better coding style (syntax).Gravatar Pierre-Marie Pédrot2016-06-14
| * | | | Adding Coq headers.Gravatar Pierre-Marie Pédrot2016-06-14
| * | | | Moving back Ltac profiling to the Ltac folder.Gravatar Pierre-Marie Pédrot2016-06-14
| * | | | Revert "Strip some trailing spaces"Gravatar Pierre-Marie Pédrot2016-06-13
* | | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-09
| | | | * Add is_ind, is_constructor, is_projGravatar Jason Gross2016-06-07
| |_|_|/ |/| | |
* | | | About printing of traces of failures while calling ltac code.Gravatar Hugo Herbelin2016-06-06
| | * | STM: proof block detection for par:Gravatar Enrico Tassi2016-06-06
| | * | STM: proof block detection/error resilience APIGravatar Enrico Tassi2016-06-06
| |/ / |/| |