| Age | Commit message (Expand) | Author |
|---|---|---|
| 2017-06-13 | Dualize the unsafe flag of refine into typecheck and make it mandatory. | Pierre-Marie Pédrot |
| 2017-06-13 | Turn the default behaviour of the refine primitive into the safe one. | Pierre-Marie Pédrot |
| 2017-06-06 | Remove the Sigma (monotonous state) API. | Maxime Dénès |
| 2017-05-19 | Removing unused warnings. | Pierre-Marie Pédrot |
| 2017-05-03 | Generalizing the refine primitive so as to accept tactic arguments. | Pierre-Marie Pédrot |
| 2017-02-14 | Merge branch 'master'. | Pierre-Marie Pédrot |
| 2017-02-14 | Refine API using EConstr. | Pierre-Marie Pédrot |
| 2017-02-14 | Making judgment type generic over the type of inner constrs. | Pierre-Marie Pédrot |
| 2016-10-22 | Unification constraint handling (#4763, #5149) | Matthieu Sozeau |
| 2016-09-16 | Adding variants enter_one and refine_one which assume that exactly one | Hugo Herbelin |
| 2016-06-09 | Adding a bit of documentation in the mli. | Pierre-Marie Pédrot |
| 2016-03-20 | Moving Refine to its proper module. | Pierre-Marie Pédrot |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |