aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* Fixing Functional Induction when applied to an alias (reference manualGravatar Hugo Herbelin2014-11-07
* Removing the legacy intro tactic code.Gravatar Pierre-Marie Pédrot2014-11-07
* Writing the raw introduction tactic in the new monad.Gravatar Pierre-Marie Pédrot2014-11-05
* Writing rename_hyps in the new monad.Gravatar Pierre-Marie Pédrot2014-11-03
* Don't raise an error when printing intro-patterns in [functional induction].Gravatar Arnaud Spiwack2014-11-01
* Feedback message: hold extra info to help routingGravatar Enrico Tassi2014-10-31
* Haskell extraction: use explicit -XMagicHash instead of -fglasgow-extsGravatar Nickolai Zeldovich2014-10-28
* Haskell extraction: put unsafeCoerce type declaration laterGravatar Nickolai Zeldovich2014-10-28
* Removing an Evd.merge in Newring.Gravatar Pierre-Marie Pédrot2014-10-27
* Fix some typos in comments.Gravatar Guillaume Melquiond2014-10-27
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Change reduction_of_red_expr to return an e_reduction_function returningGravatar Matthieu Sozeau2014-10-24
* Bugfix 3604 : more robust Unix.lockfGravatar Frédéric Besson2014-10-22
* Proofview: split [V82] module into [Unsafe] and [V82].Gravatar Arnaud Spiwack2014-10-22
* Remove the deprecated open-constr based refine.Gravatar Arnaud Spiwack2014-10-22
* Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Gravatar Arnaud Spiwack2014-10-22
* Revert "Fixing a loop in proof reconstruction for congruence (#2447)."Gravatar Hugo Herbelin2014-10-17
* Fixing a loop in proof reconstruction for congruence (#2447).Gravatar Hugo Herbelin2014-10-17
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* Restoring plugins/xml/README erased by mistake.Gravatar Hugo Herbelin2014-10-09
* A version of convert_concl and convert_hyp in new proof engine.Gravatar Hugo Herbelin2014-10-09
* Splitting out of auto.ml a file hints.ml dedicated to hints so as toGravatar Hugo Herbelin2014-10-07
* decl_mode: stay in declarative modeGravatar Enrico Tassi2014-10-06
* Simpl less (so that cbn will not simpl too much)Gravatar Pierre Boutillier2014-10-01
* Fix cbn behavior wrt simpl no matchGravatar Pierre Boutillier2014-10-01
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Keyed unification option, compiling the whole standard libraryGravatar Matthieu Sozeau2014-09-27
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Revert changes of commit 4e1135fb315eab7 over file "plugins/micromega/sos.ml",Gravatar Xavier Clerc2014-09-25
* Remove some 'deprecated' warnings.Gravatar Xavier Clerc2014-09-25
* Correction of error message (bug 3359)Gravatar Julien Forest2014-09-22
* Fixing bug 3951Gravatar Julien Forest2014-09-22
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
* Add a "Hint Mode ref (+ | -)*" hint for setting a global modeGravatar Matthieu Sozeau2014-09-15
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Discontinued xml plugin: improve the README.Gravatar Arnaud Spiwack2014-09-12
* Removing the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* Parsing of Type@{max(i,j)}.Gravatar Matthieu Sozeau2014-09-08
* Renaming goal-entering functions.Gravatar Pierre-Marie Pédrot2014-09-06
* Removing the old implementation of clear_body.Gravatar Pierre-Marie Pédrot2014-09-05
* Revert the two previous commits. I was testing in the wrong branch.Gravatar Pierre-Marie Pédrot2014-09-04
* Removing the old implementation of clear_body.Gravatar Pierre-Marie Pédrot2014-09-04
* Typing.sort_of does not leak evarmaps anymore.Gravatar Pierre-Marie Pédrot2014-09-04
* Remove [Infer] option of records.Gravatar Arnaud Spiwack2014-09-04
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
* Change the way primitive projections are declared to the kernel.Gravatar Matthieu Sozeau2014-08-28
* Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possibleGravatar Matthieu Sozeau2014-08-25
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 08:54:54 +0000