aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* 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
* instanciation is French, instantiation is EnglishGravatar Jason Gross2014-08-25
* Clean up a comment in plugins/romega/ReflOmegaCoreGravatar Jason Gross2014-08-25
* Grammar: "allowing to" is not proper EnglishGravatar Jason Gross2014-08-25
* Correct a spelling mistakeGravatar Jason Gross2014-08-25
* Lazy interpretation of patterns so that expressions such as "intros H H'/H"Gravatar Hugo Herbelin2014-08-18
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
* A reorganization of the "assert" tactics (hopefully uniform namingGravatar Hugo Herbelin2014-08-18
* Reorganisation of intropattern codeGravatar Hugo Herbelin2014-08-18
* Reorganization of tactics:Gravatar Hugo Herbelin2014-08-18
* Moving the TacExtend node from atomic to plain tactics.Gravatar Pierre-Marie Pédrot2014-08-18
* A couple of fixes/improvements in -beautify, but backtracking onGravatar Hugo Herbelin2014-08-12
* Experimentally adding an option for automatically erasing anGravatar Hugo Herbelin2014-08-05
* Adding a syntax "enough" for the variant of "assert" with the order ofGravatar Hugo Herbelin2014-08-05
* More proofs independent of the names generated by induction/elim overGravatar Hugo Herbelin2014-08-05
* STM: new "par:" goal selector, like "all:" but in parallelGravatar Enrico Tassi2014-08-05
* Ring: prevent an error message to show in case of success.Gravatar Arnaud Spiwack2014-08-05
* Better fix of e5c025Gravatar Pierre Boutillier2014-08-05
* STM: VtQuery holds the id of the state it refers toGravatar Carst Tankink2014-08-04
* Fix to make Coq compile, I think this should still be accepted.Gravatar Matthieu Sozeau2014-08-03
* Better struture for Ltac internalization environments in Constrintern.Gravatar Pierre-Marie Pédrot2014-08-02
* micromega : vm_compute; reflexivity -> vm_cast_no_check (eq_refl true)Gravatar Frédéric Besson2014-08-01
* Compatibility for compilation with ocaml 3.12 (at least).Gravatar Hugo Herbelin2014-08-01
* micromega : improve efficiency/termination of type-checkingGravatar Frédéric Besson2014-08-01
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
* Removing some tactic compatibility layer.Gravatar Pierre-Marie Pédrot2014-08-01
* micromega : refification recognises @eq T for T convertible with Z or RGravatar Frédéric Besson2014-07-31
* Add a type of untyped term to Ltac's value.Gravatar Arnaud Spiwack2014-07-29
* Qualified ML tactic names. The plugin name is used to discriminateGravatar Pierre-Marie Pédrot2014-07-27
* Derive plugin: add some comments.Gravatar Arnaud Spiwack2014-07-23
* Derive plugin: code reorganisation for clarity.Gravatar Arnaud Spiwack2014-07-23
* Derive plugin: small refactoring.Gravatar Arnaud Spiwack2014-07-23
* Derive plugin: a more general interface.Gravatar Arnaud Spiwack2014-07-23
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
* Fix semantics of change p with c to typecheck c at each specific occurrence o...Gravatar Matthieu Sozeau2014-06-23
* Proofs now take and return an evar_universe_context, simplifying interfacesGravatar Matthieu Sozeau2014-06-18
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* - Fix xml plugin treatment of inductives.Gravatar Matthieu Sozeau2014-06-15
* Deprecate options -dont, -lazy, -force-load-proofs.Gravatar Guillaume Melquiond2014-06-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-23 19:02:19 +0000