aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* coqworkmgrGravatar Enrico Tassi2014-09-02
* Fix Declaremods.end_library (Closes: #3536)Gravatar Enrico Tassi2014-09-02
* Removing the 'inductive' parameter from tacexpr AST.Gravatar Pierre-Marie Pédrot2014-09-01
* Moving the decompose tactic out of the AST.Gravatar Pierre-Marie Pédrot2014-09-01
* In evarconv, do first-order unification of LetIn's properly, ensuring we comp...Gravatar Matthieu Sozeau2014-09-01
* Coqide prints succesive hyps of the same type on 1 lineGravatar Pierre Boutillier2014-09-01
* Code cleaning in Tacintern.Gravatar Pierre-Marie Pédrot2014-09-01
* Getting rid of atomic tactics in Tacenv.Gravatar Pierre-Marie Pédrot2014-08-31
* Moving code of tactic interpretation from Tacenv to Vernacentries.Gravatar Pierre-Marie Pédrot2014-08-31
* Simplify even further the declaration of primitive projections,Gravatar Matthieu Sozeau2014-08-30
* Type-safe version of genarg list / pair / opt functions.Gravatar Pierre-Marie Pédrot2014-08-29
* Simplification of Genarg unpackers.Gravatar Pierre-Marie Pédrot2014-08-29
* Not using a "cut" in descend_in_conjunctions induced more success. WeGravatar Hugo Herbelin2014-08-29
* Fixing commit 50237af2.Gravatar Pierre-Marie Pédrot2014-08-29
* Add test-suite file. Compute the name for the record binder in theGravatar Matthieu Sozeau2014-08-29
* Fix bug when defining primitive projections mixing defined and abstracts fields.Gravatar Matthieu Sozeau2014-08-29
* Fixing bug #3528.Gravatar Pierre-Marie Pédrot2014-08-28
* Simplification of the tclCHECKINTERRUPT tactic.Gravatar Pierre-Marie Pédrot2014-08-28
* Change the way primitive projections are declared to the kernel.Gravatar Matthieu Sozeau2014-08-28
* Fix bugs #3484 and #3546.Gravatar Matthieu Sozeau2014-08-28
* There are some occurs-check cases that can be handled by imitation (using pru...Gravatar Matthieu Sozeau2014-08-28
* Fixing an unnatural selection of subterms larger than expected in theGravatar Hugo Herbelin2014-08-28
* Cleaning and documenting a bit the Proofview.Refine module.Gravatar Pierre-Marie Pédrot2014-08-28
* Adding test-suite for bug #3212.Gravatar Pierre-Marie Pédrot2014-08-28
* Fixing bug #3541.Gravatar Pierre-Marie Pédrot2014-08-28
* Protect against "it's unifiable, if you solve some unsolvable constraints" be...Gravatar Matthieu Sozeau2014-08-27
* Removing spurious tclWITHHOLES.Gravatar Pierre-Marie Pédrot2014-08-27
* Fixing bug #3493.Gravatar Pierre-Marie Pédrot2014-08-27
* Add a regression test for 3427Gravatar Jason Gross2014-08-26
* Prove forall extensionalityGravatar Jason Gross2014-08-26
* Add t-jagro to .mailmapGravatar Jason Gross2014-08-26
* Distributed binaries under MacOS are signed.Gravatar Pierre Boutillier2014-08-26
* Configure.ml creates metadata to annotate MacOS binariesGravatar Pierre Boutillier2014-08-26
* Debug RAKAMGravatar Pierre Boutillier2014-08-26
* sed s'/_one_var/_on/g'Gravatar Jason Gross2014-08-26
* Generalize EqdepFactsGravatar Jason Gross2014-08-26
* Do not pass "-batch" or "-load-vernac-source" to slaves, avoiding errors inGravatar Matthieu Sozeau2014-08-26
* Make evarconv and unification able to handle eta for records in presenceGravatar Matthieu Sozeau2014-08-26
* Fix compilation error due to commented code in previous commit by Hugo.Gravatar Matthieu Sozeau2014-08-26
* Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possibleGravatar Matthieu Sozeau2014-08-25
* Fix computation of dangling constraints at the end of a proof (bug #3531).Gravatar Matthieu Sozeau2014-08-25
* Fixing the essence of naming bug #3204: use same strategy for namingGravatar Hugo Herbelin2014-08-25
* Add an is_cofix tacticGravatar Jason Gross2014-08-25
* Prerequisite to fix stm test-suite when not in -localGravatar Pierre Boutillier2014-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: "avoiding to" isn't proper, eitherGravatar Jason Gross2014-08-25
* Grammar: "allowing to" is not proper EnglishGravatar Jason Gross2014-08-25
* Correct a spelling mistakeGravatar Jason Gross2014-08-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 16:14:24 +0000