aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* Fix call to broken unsafe_type_of in apply tactic.Gravatar Maxime Dénès2017-03-29
* Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\
| * [pp] [ide] Minor cleanups in pp code.Gravatar Emilio Jesus Gallego Arias2017-03-21
| * Remove a dead exception catching code.Gravatar Théo Zimmermann2017-03-13
| * [stm] Break stm/toplevel dependency loop.Gravatar Emilio Jesus Gallego Arias2017-02-15
* | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\|
* | Removing most nf_enter in tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* | Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Moving printing code from Evd to Termops.Gravatar Pierre-Marie Pédrot2017-02-14
* | Chasing a few unsafe constr coercions.Gravatar Pierre-Marie Pédrot2017-02-14
* | Do not ask for a normalized goal to get hypotheses and conclusions.Gravatar Pierre-Marie Pédrot2017-02-14
* | Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* | Introducing contexts parameterized by the inner term type.Gravatar Pierre-Marie Pédrot2017-02-14
* | Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* | Funind API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing compatibility layers in RetypingGravatar Pierre-Marie Pédrot2017-02-14
* | Quote API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Proofview.Goal primitive now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Eliminating parts of the right-hand side compatibility layerGravatar Pierre-Marie Pédrot2017-02-14
* | Rewrite API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Eqdecide API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Hints API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tacticals API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Clenv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tacmach API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Refine API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Goal API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Making judgment type generic over the type of inner constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Unification API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Pretyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Coercion API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tacred API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Constr_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Typing API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Evarconv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Retyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Nativenorm API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Vnorm API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| * Adding a printer for Proof.proof reflecting the focusing layout.Gravatar Hugo Herbelin2017-01-26
| * Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-30
| |\
| | * Fix some documentation typos.Gravatar Guillaume Melquiond2016-11-24
| * | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|/| | | |/
| * Use pf_get_type_of to avoid blowup in pose proof of large proof termsGravatar Matthieu Sozeau2016-11-08
| * Merge commit 'e6edb33' into v8.6Gravatar Maxime Dénès2016-11-07
| |\
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 05:56:29 +0000