| Age | Commit message (Expand) | Author |
|---|
| 2014-07-24 | Adding a tail-rec tclONCE. | Pierre-Marie Pédrot |
| 2014-07-24 | New implementation of the tactic monad. | Pierre-Marie Pédrot |
| 2014-07-23 | When closing a proof, make sure that the types have their evar substituted. | Arnaud Spiwack |
| 2014-07-23 | Proof_global: an unused variable replaced by a wildcard. | Arnaud Spiwack |
| 2014-07-23 | Proof_global.start_dependent_proof: properly threads the sigma through the te... | Arnaud Spiwack |
| 2014-07-23 | Change the interface of proof_global to take an evar_map instead of a univers... | Arnaud Spiwack |
| 2014-07-14 | Adding a delay to tclTIME. | Pierre-Marie Pédrot |
| 2014-07-13 | Adding a "time" tactical for benchmarking purposes. In case the tactic | Hugo Herbelin |
| 2014-07-11 | Feedback: LoadedFile + Goals | Enrico Tassi |
| 2014-07-10 | check_for_interrupt: better (but slower) in threading mode | Enrico Tassi |
| 2014-07-08 | Exporting Proof.split in proofview. | Pierre-Marie Pédrot |
| 2014-07-07 | Revert "time tac" (committed by mistake). | Hugo Herbelin |
| 2014-07-07 | time tac | Hugo Herbelin |
| 2014-06-25 | Putting implicit arguments of Clenv.res_pf right. | Pierre-Marie Pédrot |
| 2014-06-24 | 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-23 | Clenvtac.unify is in the new monad. | Pierre-Marie Pédrot |
| 2014-06-19 | Adding a raw_goals primitive for Tacinterp. | Pierre-Marie Pédrot |
| 2014-06-18 | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau |
| 2014-06-17 | 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-13 | 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-10 | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau |
| 2014-06-07 | Adding a new Control file centralizing the control options of Coq. | Pierre-Marie Pédrot |
| 2014-06-04 | Collecting in Namegen those conventional default names that are used in diffe... | Hugo Herbelin |
| 2014-06-03 | The tactic interpreter now uses a new type of tactics, through | Pierre-Marie Pédrot |
| 2014-06-01 | Use of "H"-based names for propositional hypotheses obtained by | Hugo Herbelin |
| 2014-05-26 | - Fix in kernel conversion not folding the universe constraints | Matthieu Sozeau |
| 2014-05-24 | 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-16 | Another try at close_proof that should behave better w.r.t. exception handling. | Matthieu Sozeau |
| 2014-05-08 | - Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ... | Matthieu Sozeau |
| 2014-05-06 | - 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 |
