aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-04-04Fix after merge, the revert of Bind Scope applies to trunk only.Matthieu Sozeau
2016-04-04Merge remote-tracking branch 'origin/pr/78' into trunk:Maxime Dénès
2016-04-04Merge branch 'trunk' of git+ssh://scm.gforge.inria.fr/gitroot/coq/coq into trunkMatej Kosik
2016-04-04Merging "https://github.com/coq/coq/pull/94", i.e. "Traversal of inductive de...Matej Kosik
2016-04-04Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Matthieu Sozeau
2016-04-04Merge branch 'linear-comparison' of https://github.com/aspiwack/coq into aspi...Matthieu Sozeau
2016-04-01Getting rid of the "_mods" parsing entry.Pierre-Marie Pédrot
2016-03-31Providing an API to access the parsing engine summary in a first-class way.Pierre-Marie Pédrot
2016-03-31Adding a test for bug #1850.Pierre-Marie Pédrot
2016-03-31Moving the code handling tactic notations to Tacentries.Pierre-Marie Pédrot
2016-03-31Abstracting away the Summary-synchronized grammar-modifying commands.Pierre-Marie Pédrot
2016-03-31Moving the Tactic Notation entry parser from Pcoq to Tacentries.Pierre-Marie Pédrot
2016-03-30Ensuring that the type of base generic arguments contain triples.Pierre-Marie Pédrot
2016-03-30Removing dead code in Genarg.Pierre-Marie Pédrot
2016-03-30Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-29Update version number for 8.5pl1Maxime Dénès
2016-03-28Fixing an incorrect use of prod_appvect on a term which was not aHugo Herbelin
2016-03-28Updating .gitignore.Pierre-Marie Pédrot
2016-03-28Fixing an evar leak in Rewrite introduced by 968dfdb15.Pierre-Marie Pédrot
2016-03-28Was too restrictive in syntactic definitions, not imagining that theyHugo Herbelin
2016-03-25Univs: fix get_current_context (bug #4603, part I)Matthieu Sozeau
2016-03-25Moving back some tactics not essentially related to Ltac into the tactics/ fo...Pierre-Marie Pédrot
2016-03-25Moving Autorewrite back to tactics/.Pierre-Marie Pédrot
2016-03-25Making Autorewrite independent from Ltac.Pierre-Marie Pédrot
2016-03-25Moving Eqdecide to tactics/.Pierre-Marie Pédrot
2016-03-25Making Eqdecide independent of Extratactics.Pierre-Marie Pédrot
2016-03-25Moving Eauto and Class_tactics to tactics/.Pierre-Marie Pédrot
2016-03-25Moving type_uconstr to Pretyping.Pierre-Marie Pédrot
2016-03-25Test suite file for a bug in BigQ arithmetic fixed a while ago.Maxime Dénès
2016-03-25Test suite file for a bug in int31 arithmetic fixed a while ago.Maxime Dénès
2016-03-25Remove int64 emulation in bytecode interpreter.Maxime Dénès
2016-03-25Fix a bug in Program coercion codeMatthieu Sozeau
2016-03-24Fix handling of arity of definitional classes.Matthieu Sozeau
2016-03-24use printf instead of sequenced calls to print.Gregory Malecha
2016-03-24add a .merlin target to the makefileGregory Malecha
2016-03-23Revert "refine: do check all unif problems are solved (Close: #4415, #4532)"Enrico Tassi
2016-03-23refine: do check all unif problems are solved (Close: #4415, #4532)Enrico Tassi
2016-03-22A patch renaming equal into eq in the module dealing withHugo Herbelin
2016-03-22Adding eq/compare/hash for syntactic view atHugo Herbelin
2016-03-21Creating a dedicated ltac/ folder for Hightactics.Pierre-Marie Pédrot
2016-03-21Moving the last parts of the Ltac engine to hightactics.Pierre-Marie Pédrot
2016-03-20Moving Tacsubst to hightactics.Pierre-Marie Pédrot
2016-03-20Relying on generic arguments to represent Extern hints.Pierre-Marie Pédrot
2016-03-20Adding a new Ltac generic argument for forced tactics returing unit.Pierre-Marie Pédrot
2016-03-20Moving Tacenv to Hightactics.Pierre-Marie Pédrot
2016-03-20Moving Tactic_debug to Hightactic.Pierre-Marie Pédrot
2016-03-20Moving the lowest parts of pretyping/ (Evarutil & Proofview) to engine/.Pierre-Marie Pédrot
2016-03-20Documenting changes.Pierre-Marie Pédrot
2016-03-20Moving Evarutil and Proofview to engine/Pierre-Marie Pédrot
2016-03-20Making Evarutil independent from Reductionops.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 19:26:30 +0000