aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* 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
* Adding a [map] primitive to the tactic monad. Hopefully this should beGravatar Pierre-Marie Pédrot2014-04-20
* Transfering the initial goals from the proofview to the proof object.Gravatar Pierre-Marie Pédrot2014-04-07
* Removing unused functions in Refiner.Gravatar Pierre-Marie Pédrot2014-04-06
* Actually using the [modify] primitive.Gravatar Pierre-Marie Pédrot2014-04-06
* Adding an [modify] function to the tactic monad. It allows to modifyGravatar Pierre-Marie Pédrot2014-04-06
* Evars introduced by Proofview refining are flagged as GoalEvar. For someGravatar Pierre-Marie Pédrot2014-04-01
* Removing the Change_evar refiner rule.Gravatar Pierre-Marie Pédrot2014-03-31
* Lighter interface for creating refining tactics.Gravatar Pierre-Marie Pédrot2014-03-28
* Removing tactic compatibility layer from Eqdecide.Gravatar Pierre-Marie Pédrot2014-03-27
* Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.Gravatar Pierre-Marie Pédrot2014-03-26
* Removing Tacmach compatibility layer in Inv.Gravatar Pierre-Marie Pédrot2014-03-26
* Moving some tactic code to the new engine.Gravatar Pierre-Marie Pédrot2014-03-26
* Using non-normalized goals in tactic interpretation.Gravatar Pierre-Marie Pédrot2014-03-19
* Adding phantom types to discriminate normalized goals, and adding a way toGravatar Pierre-Marie Pédrot2014-03-19
* Potentially unused computation in Goal.Gravatar Pierre-Marie Pédrot2014-03-07
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 12:14:19 +0000