Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | | | Auto API using EConstr. | 2017-02-14 | ||
* | | | | Hints API using EConstr. | 2017-02-14 | ||
* | | | | Leminv API using EConstr. | 2017-02-14 | ||
* | | | | Inv API using EConstr. | 2017-02-14 | ||
* | | | | Contradiction API using EConstr. | 2017-02-14 | ||
* | | | | Equality API using EConstr. | 2017-02-14 | ||
* | | | | Elim API using EConstr. | 2017-02-14 | ||
* | | | | Tactics API using EConstr. | 2017-02-14 | ||
* | | | | Hipattern API using EConstr. | 2017-02-14 | ||
* | | | | Tacticals API using EConstr. | 2017-02-14 | ||
* | | | | Clenv API using EConstr. | 2017-02-14 | ||
* | | | | Tacmach API using EConstr. | 2017-02-14 | ||
* | | | | Refine API using EConstr. | 2017-02-14 | ||
* | | | | Goal API using EConstr. | 2017-02-14 | ||
* | | | | Cleaning up opening of the EConstr module in pretyping folder. | 2017-02-14 | ||
* | | | | Making judgment type generic over the type of inner constrs. | 2017-02-14 | ||
* | | | | Unification API using EConstr. | 2017-02-14 | ||
* | | | | Pretyping API using EConstr. | 2017-02-14 | ||
* | | | | Cases API using EConstr. | 2017-02-14 | ||
* | | | | Typeclasses API using EConstr. | 2017-02-14 | ||
* | | | | Tacred API using EConstr. | 2017-02-14 | ||
* | | | | Constr_matching API using EConstr. | 2017-02-14 | ||
* | | | | Patternops API using EConstr. | 2017-02-14 | ||
* | | | | Typing API using EConstr. | 2017-02-14 | ||
* | | | | Evarconv API using EConstr. | 2017-02-14 | ||
* | | | | Evarsolve API using EConstr. | 2017-02-14 | ||
* | | | | Find_subterm API using EConstr. | 2017-02-14 | ||
* | | | | Retyping API using EConstr. | 2017-02-14 | ||
* | | | | Reductionops API using EConstr. | 2017-02-14 | ||
* | | | | Termops API using EConstr. | 2017-02-14 | ||
| * | | | Proofview: tclINDEPENDENTL | 2017-02-10 | ||
| * | | | Fixing injection in the presence of let-in in constructors. | 2016-12-22 | ||
| * | | | Merge remote-tracking branch 'github/pr/172' into trunk | 2016-12-19 | ||
| |\ \ \ | ||||
| * \ \ \ | Merge branch 'v8.6' | 2016-12-07 | ||
| |\ \ \ \ | | | |/ / | | |/| | | ||||
| | * | | | Merge remote-tracking branch 'github/pr/381' into v8.6 | 2016-12-02 | ||
| | |\ \ \ | ||||
| | | * | | | Fix shelving order in typeclasses eauto. | 2016-11-30 | ||
| | | * | | | Fix typeclasses eauto shelving. | 2016-11-30 | ||
| | * | | | | Fix bug #5232: proper globalization of hints paths | 2016-11-30 | ||
| | |/ / / | ||||
| * | | | | Tests for info/debug auto/eauto. | 2016-11-19 | ||
| * | | | | Merge branch 'v8.6' | 2016-11-18 | ||
|/| | | | | |/ / / | ||||
| * | | | Minor debug printing bug, | 2016-11-16 | ||
| * | | | Revert more of a477dc for good measure | 2016-11-16 | ||
| * | | | Revert part of a477dc, disallow_shelved | 2016-11-15 | ||
| * | | | Merge remote-tracking branch 'github/pr/339' into v8.6 | 2016-11-07 | ||
| |\ \ \ | ||||
| | * | | | Fixes to compile with ocaml 4.01 | 2016-11-07 | ||
| * | | | | Merge commit 'e6edb33' into v8.6 | 2016-11-07 | ||
| |\ \ \ \ | ||||
| | * | | | | More explicit name for status of unification constraints. | 2016-11-07 | ||
| * | | | | | More precise refine compatibility | 2016-11-05 | ||
| * | | | | | Fix #3441 Use pf_get_type_of to avoid blowup | 2016-11-04 | ||
| * | | | | | Fix refine in compatibility mode | 2016-11-04 |