aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* Adding a delay to tclTIME.Gravatar Pierre-Marie Pédrot2014-07-14
* Adding a "time" tactical for benchmarking purposes. In case the tacticGravatar Hugo Herbelin2014-07-13
* Feedback: LoadedFile + GoalsGravatar Enrico Tassi2014-07-11
* check_for_interrupt: better (but slower) in threading modeGravatar Enrico Tassi2014-07-10
* Exporting Proof.split in proofview.Gravatar Pierre-Marie Pédrot2014-07-08
* Revert "time tac" (committed by mistake).Gravatar Hugo Herbelin2014-07-07
* time tacGravatar Hugo Herbelin2014-07-07
* Putting implicit arguments of Clenv.res_pf right.Gravatar Pierre-Marie Pédrot2014-06-25
* Force the final universe context of a proof only in poly || now case.Gravatar Matthieu Sozeau2014-06-24
* Clenvtac.clenv_refine in the new monad. Not satisfactory though, because itGravatar Pierre-Marie Pédrot2014-06-24
* Clenvtac.res_pf is in the new tactic monad.Gravatar Pierre-Marie Pédrot2014-06-24
* Clenvtac.unify is in the new monad.Gravatar Pierre-Marie Pédrot2014-06-23
* Adding a raw_goals primitive for Tacinterp.Gravatar Pierre-Marie Pédrot2014-06-19
* Proofs now take and return an evar_universe_context, simplifying interfacesGravatar Matthieu Sozeau2014-06-18
* Tentative optimization not to nf_evar too often in the compatibilityGravatar Pierre-Marie Pédrot2014-06-17
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* Safer entry point of primitive projections in the kernel, now it does recognizeGravatar Matthieu Sozeau2014-06-17
* Improving tclWITHHOLES which did not see undefined evars up toGravatar Hugo Herbelin2014-06-13
* Fixing "clear" in internal_cut_replace: forbid dependencies in theGravatar Hugo Herbelin2014-06-13
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Gravatar Matthieu Sozeau2014-06-10
* Adding a new Control file centralizing the control options of Coq.Gravatar Pierre-Marie Pédrot2014-06-07
* Collecting in Namegen those conventional default names that are used in diffe...Gravatar Hugo Herbelin2014-06-04
* The tactic interpreter now uses a new type of tactics, throughGravatar Pierre-Marie Pédrot2014-06-03
* Use of "H"-based names for propositional hypotheses obtained byGravatar Hugo Herbelin2014-06-01
* - Fix in kernel conversion not folding the universe constraintsGravatar Matthieu Sozeau2014-05-26
* Revert "Chasing the goal entering backward while interpreting tactics. This r...Gravatar Pierre-Marie Pédrot2014-05-24
* Chasing the goal entering backward while interpreting tactics. This requiredGravatar Pierre-Marie Pédrot2014-05-24
* Another try at close_proof that should behave better w.r.t. exception handling.Gravatar Matthieu Sozeau2014-05-16
* - Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ...Gravatar Matthieu Sozeau2014-05-08
* - Fix treatment of global universe constraints which should be passed alongGravatar Matthieu Sozeau2014-05-06
* Fix set_leq_sort refusing max(u,Set) <= Set when u is flexible.Gravatar Matthieu Sozeau2014-05-06
* - Fixes for canonical structure resolution (check that the initial term indee...Gravatar Matthieu Sozeau2014-05-06
* - Fix eq_constr_universes restricted to Sorts.equalGravatar Matthieu Sozeau2014-05-06
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Adapt universe polymorphic branch to new handling of futures for delayed proofs.Gravatar Matthieu Sozeau2014-05-06
* Fix issue #88: restrict_universe_context was wrongly forgetting about constra...Gravatar Matthieu Sozeau2014-05-06
* - Fix index-list to show computational relations for rewriting files.Gravatar Matthieu Sozeau2014-05-06
* - Fix comparison of universes.Gravatar Matthieu Sozeau2014-05-06
* Rewriting the proof monad mechanism. Now it uses pure OCaml code, withoutGravatar ppedrot2014-05-06
* Fix interface for template polymorphism, cleaning up code in all typing algor...Gravatar Matthieu Sozeau2014-05-06
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* Rework handling of universes on top of the STM, allowing for delayedGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Rewriting [lapply] tactic in the new monad.Gravatar Pierre-Marie Pédrot2014-04-27
* Fixing various backtrace recordings.Gravatar Pierre-Marie Pédrot2014-04-25
* Better representation of evar filters: we represent the vacuous filters ofGravatar Pierre-Marie Pédrot2014-04-23
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Removing tactic compatibility layer from Elim.Gravatar Pierre-Marie Pédrot2014-04-22
* Simplifying interface of elimination tactics. They used dummy clausenvs, andGravatar Pierre-Marie Pédrot2014-04-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 20:38:49 +0000