| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | More explicit name for status of unification constraints. |  Maxime Dénès | 2016-11-07 |
| | | |||
| * | Unification constraint handling (#4763, #5149) |  Matthieu Sozeau | 2016-10-22 |
| | | | | | | | | | | | | | | | | 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. | ||
| * | admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032) |  Enrico Tassi | 2015-03-11 |
| | | | | | | | | | | | | | | | | - no more inconsistent Axiom in the Prelude - STM can now process Admitted proofs asynchronously - the quick chain can stock "Admitted" jobs in .vio files - the vio2vo step checks the jobs but does not stock the result in the opaque tables (they have no slot) - Admitted emits a warning if the proof is complete - Admitted uses the (partial) proof term to infer section variables used (if not given with Proof using), like for Qed - test-suite: extra line Require TestSuite.admit to each file making use of admit - test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to find TestSuite.admit | ||
| * | Add several reproduction files for bugs. |  Xavier Clerc | 2014-09-25 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |