aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-05-22romega: use N instead of nat for TvarPierre Letouzey
2017-05-22romega: shorter trace (no more term lengths)Pierre Letouzey
2017-05-22refl_omega: refactoring of normalize_equationPierre Letouzey
2017-05-22ReflOmegaCore: lots of dead code + a few refactored proofsPierre Letouzey
2017-05-22romega: if it bugs again, at least do it with a short and quick errorPierre Letouzey
2017-05-22refl_omega: comment the lack of lifts when dealing with arrowsPierre Letouzey
2017-05-22romega: discard constructor D_mono (shorter trace + fix a bug)Pierre Letouzey
2017-05-22refl_omega: more refactoring (e.g. IntSets instead of sorted lists)Pierre Letouzey
2017-05-22refl_omega: refactoring (e.g. useless args in destructurate_pos_hyp)Pierre Letouzey
2017-05-22ReflOmegaCore: discard useless cosntructor P_NOPPierre Letouzey
2017-05-22ReflOmegaCore: revised proofs (mostly bullets instead of ;[|||])Pierre Letouzey
2017-05-22Compatibility fix while waiting for integration of Pierre Courtieu's PR #449.Hugo Herbelin
2017-05-22Using type classes in the interpretation of "specialize" and "contradiction".Hugo Herbelin
2017-05-22Clarifying the interpretation path for the "constr_with_binding" argument.Hugo Herbelin
2017-05-20Added a test for #4765 (an example of printing abbreviation with binders).Hugo Herbelin
2017-05-20Deprecate -nodoc.Théo Zimmermann
2017-05-20[coqdoc] Add keywords in bug 2884.Emilio Jesus Gallego Arias
2017-05-20Change wrong bullet message.Théo Zimmermann
2017-05-20Revised behavior on ill-formed identifiers.Hugo Herbelin
2017-05-20Merge PR#276: Stopping injection not to work on discriminable atoms (see #4890).Maxime Dénès
2017-05-20Mention ./configure in INSTALL.docThéo Zimmermann
2017-05-20Merge PR#654: Travis: do not cache opam logs (+prettier spacing)Maxime Dénès
2017-05-20Merge PR#653: Bug #5535, test for Show with -emacsMaxime Dénès
2017-05-20Merge PR#643: [ide] Disable `print_ast` call.Maxime Dénès
2017-05-20Merge PR#474: A fix for #5390 (a useful error on used introduction names was ...Maxime Dénès
2017-05-20[test-suite] Add tests for goal printing.Emilio Jesus Gallego Arias
2017-05-20Merge PR#627: Obligations shrinking: shrink abstraction tooMaxime Dénès
2017-05-20Merge PR#644: [toplevel] [stm] Avoid edit_at in batch mode (bug #5520)Maxime Dénès
2017-05-20Merge PR#648: Allow interactive editing of `plugins/` by adding .dir-locals.elMaxime Dénès
2017-05-20Merge PR#649: Fix a typoMaxime Dénès
2017-05-20Merge PR#651: Re-adding explicit dependency of misc universe test into all_st...Maxime Dénès
2017-05-20Merge PR#641: Fix bug #5486, don't reverse ids in tuplesMaxime Dénès
2017-05-20Merge PR#640: [toplevel] Restore 8.6 goal printing behavior.Maxime Dénès
2017-05-19Exporting some functions of vars.ml as functions operating on EConstr.Hugo Herbelin
2017-05-19In EConstr, defining some "cast" functions earlier.Hugo Herbelin
2017-05-19Moving "sym" on "eq" type to lib/util.ml.Hugo Herbelin
2017-05-19Travis: do not cache opam logs (+prettier spacing)Gaetan Gilbert
2017-05-19add test for Show with -emacs, bug 5535Paul Steckler
2017-05-19Adding new tactic notation scopes.Pierre-Marie Pédrot
2017-05-19Extending the Coq API in Ltac2.Pierre-Marie Pédrot
2017-05-19Removing dead code in Ltac2, and cleaning up a bit.Pierre-Marie Pédrot
2017-05-19Introducing tactic notations in Ltac2.Pierre-Marie Pédrot
2017-05-19Allow raw terms to contain references to absolute definitions.Pierre-Marie Pédrot
2017-05-19Stdlib functions now return Ltac2 exceptions.Pierre-Marie Pédrot
2017-05-19Proper handling of exception definition in Ltac2.Pierre-Marie Pédrot
2017-05-19Merging GTacTuple and GTacCst nodes.Pierre-Marie Pédrot
2017-05-19Towards a proper printing of Ltac2 data structures.Pierre-Marie Pédrot
2017-05-19Allow the embedding of Ltac2 terms in constrs via the ltac2:(...) syntax.Pierre-Marie Pédrot
2017-05-19Fixing a precedence issue in type parameters.Pierre-Marie Pédrot
2017-05-19Proper handling of record types.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-02 12:55:08 +0000