| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-02-14 | Introducing contexts parameterized by the inner term type. | Pierre-Marie Pédrot | |
| This allows the decoupling of the notions of context containing kernel terms and context containing tactic-level terms. | |||
| 2017-02-14 | Evar-normalizing functions now act on EConstrs. | Pierre-Marie Pédrot | |
| 2017-02-14 | Removing various compatibility layers of tactics. | Pierre-Marie Pédrot | |
| 2017-02-14 | Funind API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Ltac now uses evar-based constrs. | Pierre-Marie Pédrot | |
| 2017-02-14 | Removing compatibility layers in Retyping | Pierre-Marie Pédrot | |
| 2017-02-14 | Quote API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Reductionops now return EConstrs. | Pierre-Marie Pédrot | |
| 2017-02-14 | Proofview.Goal primitive now return EConstrs. | Pierre-Marie Pédrot | |
| 2017-02-14 | Eliminating parts of the right-hand side compatibility layer | Pierre-Marie Pédrot | |
| 2017-02-14 | Rewrite API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Eqdecide API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Hints API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Tactics API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Tacticals API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Clenv API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Tacmach API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Refine API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Goal API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Making judgment type generic over the type of inner constrs. | Pierre-Marie Pédrot | |
| This allows to factorize code and prevents the unnecessary use of back and forth conversions between the various types of terms. Note that functions from typing may now raise errors as PretypeError rather than TypeError, because they call the proper wrapper. I think that they were wrongly calling the kernel because of an overlook of open modules. | |||
| 2017-02-14 | Unification API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Pretyping API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Coercion API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Tacred API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Constr_matching API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Typing API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Evarconv API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Retyping API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Nativenorm API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Vnorm API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Reductionops API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Termops API using EConstr. | Pierre-Marie Pédrot | |
| 2017-01-26 | Adding a printer for Proof.proof reflecting the focusing layout. | Hugo Herbelin | |
| This is a modest contribution serving before all the purpose of displaying the focus stack and the shelf and give_up list. It does not print the sigma (while it could). Any improvements are welcome. | |||
| 2016-11-30 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-11-24 | Fix some documentation typos. | Guillaume Melquiond | |
| Note: "dependant" does exist, but it is a noun and it means a person that is somehow financially dependent on someone else. | |||
| 2016-11-18 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-11-08 | Use pf_get_type_of to avoid blowup in pose proof of large proof terms | Matthieu Sozeau | |
| 2016-11-07 | Merge commit 'e6edb33' into v8.6 | Maxime Dénès | |
| Was PR#331: Solve_constraints and Set Use Unification Heuristics | |||
| 2016-11-07 | More explicit name for status of unification constraints. | Maxime Dénès | |
| 2016-11-04 | Fix #3441 Use pf_get_type_of to avoid blowup | Matthieu Sozeau | |
| ... in pose proof of large proof terms | |||
| 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.6' | Pierre-Marie Pédrot | |
| 2016-10-12 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-10-12 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-10-12 | Merge remote-tracking branch 'git/bug5123' into v8.5 | Matthieu Sozeau | |
| 2016-10-11 | Fix bug #5123: mark all shelved evars unresolvable | Matthieu Sozeau | |
| Previously, some splipped through and were caught by unrelated calls to typeclass resolution. | |||
| 2016-10-11 | Fix for bug #4863, update the Proofview's env with | Matthieu Sozeau | |
| side_effects. Partial solution to the handling of side effects in proofview. | |||
| 2016-10-10 | Fix #4416: - Incorrect "Error: Incorrect number of goals" | Arnaud Spiwack | |
| In `Ftactic` the number of results could desynchronise with the number of goals when some goals were solved by side effect in a different branch of a `DISPATCH`. See [coq-bugs#4416](https://coq.inria.fr/bugs/show_bug.cgi?id=4416). | |||
| 2016-10-05 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |