| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-10-22 | Renamings to avoid confusion deprecating old names | Matthieu Sozeau | |
| reconsider_conv_pbs -> reconsider_unif_constraints consider_remaining_unif_problems -> solve_unif_constraints_with_heuristics | |||
| 2016-10-22 | Unification constraint handling (#4763, #5149) | Matthieu Sozeau | |
| Refine fix for bug #4763, fixing #5149 Tactic [Refine.solve_constraints] and global option Adds a new multi-goal tactic [Refine.solve_constraints] that forces solving of unification constraints and evar candidates to be solved. run_tactic now calls [solve_constraints] at every [.], preserving (mostly) the 8.4/8.5 behavior of tactics. The option allows to unset the forced solving unification constraints at each ".", letting the user control the places where the use of heuristics is done. Fix test-suite files too. | |||
| 2016-10-12 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-09-16 | Adding variants enter_one and refine_one which assume that exactly one | Hugo Herbelin | |
| goal is under focus and which support returning a relevant output. | |||
| 2016-09-02 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-05-08 | Removing dead code and unused opens. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Refine to its proper module. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |