| Commit message (Expand) | Author | Age |
|---|
| * | Putting implicit arguments of Clenv.res_pf right. |  Pierre-Marie Pédrot | 2014-06-25 |
| * | Force the final universe context of a proof only in poly || now case. |  Matthieu Sozeau | 2014-06-24 |
| * | Clenvtac.clenv_refine in the new monad. Not satisfactory though, because it | Pierre-Marie Pédrot | 2014-06-24 |
| * | Clenvtac.res_pf is in the new tactic monad. | Pierre-Marie Pédrot | 2014-06-24 |
| * | Clenvtac.unify is in the new monad. | Pierre-Marie Pédrot | 2014-06-23 |
| * | Adding a raw_goals primitive for Tacinterp. | Pierre-Marie Pédrot | 2014-06-19 |
| * | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau | 2014-06-18 |
| * | Tentative optimization not to nf_evar too often in the compatibility | Pierre-Marie Pédrot | 2014-06-17 |
| * | Removing dead code. | Pierre-Marie Pédrot | 2014-06-17 |
| * | Safer entry point of primitive projections in the kernel, now it does recognize | Matthieu Sozeau | 2014-06-17 |
| * | Improving tclWITHHOLES which did not see undefined evars up to |  Hugo Herbelin | 2014-06-13 |
| * | Fixing "clear" in internal_cut_replace: forbid dependencies in the | Hugo Herbelin | 2014-06-13 |
| * | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau | 2014-06-10 |
| * | Adding a new Control file centralizing the control options of Coq. | Pierre-Marie Pédrot | 2014-06-07 |
| * | Collecting in Namegen those conventional default names that are used in diffe... | Hugo Herbelin | 2014-06-04 |
| * | The tactic interpreter now uses a new type of tactics, through | Pierre-Marie Pédrot | 2014-06-03 |
| * | Use of "H"-based names for propositional hypotheses obtained by | Hugo Herbelin | 2014-06-01 |
| * | - Fix in kernel conversion not folding the universe constraints | Matthieu Sozeau | 2014-05-26 |
| * | Revert "Chasing the goal entering backward while interpreting tactics. This r... | Pierre-Marie Pédrot | 2014-05-24 |
| * | Chasing the goal entering backward while interpreting tactics. This required | Pierre-Marie Pédrot | 2014-05-24 |
| * | Another try at close_proof that should behave better w.r.t. exception handling. | Matthieu Sozeau | 2014-05-16 |
| * | - Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ... | Matthieu Sozeau | 2014-05-08 |
| * | - Fix treatment of global universe constraints which should be passed along | Matthieu Sozeau | 2014-05-06 |
| * | Fix set_leq_sort refusing max(u,Set) <= Set when u is flexible. | Matthieu Sozeau | 2014-05-06 |
| * | - Fixes for canonical structure resolution (check that the initial term indee... | Matthieu Sozeau | 2014-05-06 |
| * | - Fix eq_constr_universes restricted to Sorts.equal | Matthieu Sozeau | 2014-05-06 |
| * | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau | 2014-05-06 |
| * | Adapt universe polymorphic branch to new handling of futures for delayed proofs. | Matthieu Sozeau | 2014-05-06 |
| * | Fix issue #88: restrict_universe_context was wrongly forgetting about constra... | Matthieu Sozeau | 2014-05-06 |
| * | - Fix index-list to show computational relations for rewriting files. | Matthieu Sozeau | 2014-05-06 |
| * | - Fix comparison of universes. | Matthieu Sozeau | 2014-05-06 |
| * | Rewriting the proof monad mechanism. Now it uses pure OCaml code, without |  ppedrot | 2014-05-06 |
| * | Fix interface for template polymorphism, cleaning up code in all typing algor... | Matthieu Sozeau | 2014-05-06 |
| * | Initial work on reintroducing old-style polymorphism for compatibility (the s... | Matthieu Sozeau | 2014-05-06 |
| * | Correct rebase on STM code. Thanks to E. Tassi for help on dealing with | Matthieu Sozeau | 2014-05-06 |
| * | Rework handling of universes on top of the STM, allowing for delayed | Matthieu Sozeau | 2014-05-06 |
| * | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
| * | Rewriting [lapply] tactic in the new monad. | Pierre-Marie Pédrot | 2014-04-27 |
| * | Fixing various backtrace recordings. | Pierre-Marie Pédrot | 2014-04-25 |
| * | Better representation of evar filters: we represent the vacuous filters of | Pierre-Marie Pédrot | 2014-04-23 |
| * | Removing dead code, thanks to new OCaml warnings and a bit of scripting. | Pierre-Marie Pédrot | 2014-04-23 |
| * | Removing tactic compatibility layer from Elim. | Pierre-Marie Pédrot | 2014-04-22 |
| * | Simplifying interface of elimination tactics. They used dummy clausenvs, and | Pierre-Marie Pédrot | 2014-04-22 |
| * | Adding a [map] primitive to the tactic monad. Hopefully this should be | Pierre-Marie Pédrot | 2014-04-20 |
| * | Transfering the initial goals from the proofview to the proof object. | Pierre-Marie Pédrot | 2014-04-07 |
| * | Removing unused functions in Refiner. | Pierre-Marie Pédrot | 2014-04-06 |
| * | Actually using the [modify] primitive. | Pierre-Marie Pédrot | 2014-04-06 |
| * | Adding an [modify] function to the tactic monad. It allows to modify | Pierre-Marie Pédrot | 2014-04-06 |
| * | Evars introduced by Proofview refining are flagged as GoalEvar. For some | Pierre-Marie Pédrot | 2014-04-01 |
| * | Removing the Change_evar refiner rule. | Pierre-Marie Pédrot | 2014-03-31 |
Pierre-Marie Pédrot
Matthieu Sozeau
Hugo Herbelin
ppedrot