aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.ml
Commit message (Expand)AuthorAge
* A fix for #5390 (a useful error on used introduction names was masked).Gravatar Hugo Herbelin2017-05-17
* Remove an unused open introduced by the previous commit.Gravatar Maxime Dénès2017-05-11
* Merge PR#201: Transparent abstractGravatar Maxime Dénès2017-05-11
|\
* \ Merge PR#582: Fix warningsGravatar Maxime Dénès2017-05-02
|\ \
* \ \ Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...Gravatar Maxime Dénès2017-04-28
|\ \ \
| | * | Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
| | * | Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| |/ / |/| |
| | * transparent abstract: Respond to review commentGravatar Jason Gross2017-04-25
| | * transparent abstract: Respond to review commentGravatar Jason Gross2017-04-25
| | * Make opaque optional only for tclABSTRACTGravatar Jason Gross2017-04-25
| | * Generalize cache_term_by_tactic_thenGravatar Jason Gross2017-04-25
| | * Add support for transparent abstract (no syntax)Gravatar Jason Gross2017-04-25
* | | Fix the API of the new pf_constr_of_global.Gravatar Pierre-Marie Pédrot2017-04-24
* | | Porting generalize_dep to the new tactic engine.Gravatar Pierre-Marie Pédrot2017-04-24
| |/ |/|
| * Fixing #5420 as well as many related bugs due to miscounting let-ins.Gravatar Hugo Herbelin2017-04-09
* | Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
|\|
| * Merge PR#508: Optimize pending evarsGravatar Maxime Dénès2017-04-06
| |\
* | | Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
* | | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\| |
| * | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-23
| |\ \
| | | * Fast path for implicit tactic solving.Gravatar Pierre-Marie Pédrot2017-03-23
| | | * Ensuring static invariants about handling of pending evars in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
| | |/ | |/|
| * | Attempt to improve error message when "apply in" fail.Gravatar Hugo Herbelin2017-03-15
| | * Show unused-intro-pattern warning.Gravatar Théo Zimmermann2017-03-14
* | | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\| |
* | | Removing most nf_enter in tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Chasing a few unsafe constr coercions.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Do not ask for a normalized goal to get hypotheses and conclusions.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Introducing contexts parameterized by the inner term type.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Removing compatibility layers from TacticalsGravatar Pierre-Marie Pédrot2017-02-14
* | | Cleaning up interfaces.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Removing compatibility layers related to printing.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Removing compatibility layers in RetypingGravatar Pierre-Marie Pédrot2017-02-14
* | | Removing some return type compatibility layers in Termops.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Proofview.Goal primitive now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Eliminating parts of the right-hand side compatibility layerGravatar Pierre-Marie Pédrot2017-02-14
* | | Tactic_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Class_tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Leminv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Inv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Hipattern API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Clenv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Tacmach API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 20:32:14 +0000