aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-05-19Allowing to include Coq terms in Ltac2 using the constr:(...) syntax.Pierre-Marie Pédrot
2017-05-19Embedding generic arguments in Ltac2 AST.Pierre-Marie Pédrot
2017-05-19Introduction of the Ltac2 plugin.Pierre-Marie Pédrot
2017-05-19Re-adding explicit dependency of misc universe test into all_stdlib.v.Hugo Herbelin
2017-05-19Fixing an extra bug with pattern_of_constr.Hugo Herbelin
2017-05-19Removing unused warnings.Pierre-Marie Pédrot
2017-05-19Merge branch 'master' into ltac2-hooksPierre-Marie Pédrot
2017-05-18Fix a typoJason Gross
2017-05-18Add .dir-locals.el to pluginsJason Gross
2017-05-18Adding a trespasser warning to the Nametab API.Pierre-Marie Pédrot
2017-05-18[stm] Tweak debug options.Emilio Jesus Gallego Arias
2017-05-18[toplevel] [stm] Avoid edit_at in batch mode (bug #5520)Emilio Jesus Gallego Arias
2017-05-18[ide] Disable `print_ast` call.Emilio Jesus Gallego Arias
2017-05-17A fix for #5390 (a useful error on used introduction names was masked).Hugo Herbelin
2017-05-17Merge PR#633: An extension of EXTEND and notations to make standard parsing t...Maxime Dénès
2017-05-17Documenting relaxing of constraints on injection.Hugo Herbelin
2017-05-17Stopping injection not to work on discriminable atoms (see #4890).Hugo Herbelin
2017-05-17Fixing bug #5526,allow nonlinear variables in Notation patternsPaul Steckler
2017-05-17Merge PR#457: Adding an even more compact goal hyps mode.Maxime Dénès
2017-05-17Merge PR#607: Make congruence reuse discriminate instead of rolling its own.Maxime Dénès
2017-05-17fix swapping of ids in tuples, bug 5486Paul Steckler
2017-05-17[toplevel] Restore 8.6 goal printing behavior.Emilio Jesus Gallego Arias
2017-05-17Merge branch 'v8.6'Pierre-Marie Pédrot
2017-05-17Merge PR#620: Reorganization of the layout for miscellaneous testsMaxime Dénès
2017-05-17Merge PR#614: Improve TravisMaxime Dénès
2017-05-17Travis: add -warn-error targets (standard and 4.04.1 ocaml)Gaetan Gilbert
2017-05-17Merge PR#630: [interp] [ast] Make raw_cases_pattern_expr private + small cleanupMaxime Dénès
2017-05-17Travis: deduplicate package list for coqide+documentation targetsGaetan Gilbert
2017-05-17Travis: do not run the tests if building Coq failsGaetan Gilbert
2017-05-17Merge PR#635: Fixing #5522 (anomaly with free vars of pat)Maxime Dénès
2017-05-17Merge PR#636: Miscellaneous typos, dead code, etc.Maxime Dénès
2017-05-17Merge PR#639: Stop using auto with * in two proofs.Maxime Dénès
2017-05-16Stop using auto with * in two proofs.Théo Zimmermann
2017-05-16Fix bug #5360: anomalies in typeclass resolution outputMatthieu Sozeau
2017-05-16Fixing grammar for "evar" by exporting the test_lpar_id_colon trick to EXTEND.Hugo Herbelin
2017-05-16Adding support for using grammar entries returning no value in EXTEND.Hugo Herbelin
2017-05-16Simplified compaction criterion + tests.Pierre Courtieu
2017-05-16Fixing bug #5222 (anomaly with "`pat" in the presence of scope delimiters).Hugo Herbelin
2017-05-16Fixing a bug with nested "as" clauses in "match".Hugo Herbelin
2017-05-16Merge PR#624: Switch bedrock to mit-plv baseMaxime Dénès
2017-05-16Merge PR#626: Add documentation for Set Ltac Batch DebugMaxime Dénès
2017-05-16Merge PR#629: A couple of simple updates for TravisMaxime Dénès
2017-05-15Dead code in coqdep.Hugo Herbelin
2017-05-15Fix #5255: [Context (x : T := y)] should mean [Let x := y].Pierre-Marie Pédrot
2017-05-15[interp] Rework check for casts inside patterns.Emilio Jesus Gallego Arias
2017-05-15[interp] [ast] Make raw_cases_pattern_expr private.Emilio Jesus Gallego Arias
2017-05-15Typo in comments of constrintern.Hugo Herbelin
2017-05-14Removing a line warned unused.Hugo Herbelin
2017-05-14Removing a variable warned unused.Hugo Herbelin
2017-05-13[travis] Update OCaml to 4.04.1Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-02 16:12:29 +0000