aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-12-17Revert and correctly fix "#4843 part 2 : The .cmxs files for plugins must hav...Pierre Boutillier
2014-12-16#3828 is solved.Hugo Herbelin
2014-12-16Moving #2447 (congruence) to fixed.Hugo Herbelin
2014-12-16In CHANGES, alerting about stronger check on notation level modifiers.Hugo Herbelin
2014-12-16More printers for ltac signatures.Hugo Herbelin
2014-12-16Test for #3654.Hugo Herbelin
2014-12-16fix bug #2447 in congruencePierre Corbineau
2014-12-16fix bug #2447 in congruencePierre Corbineau
2014-12-16Fixing CAMLP4 compilation.Pierre-Marie Pédrot
2014-12-16msg_info now puts infomsg tag in emacs mode.Pierre Courtieu
2014-12-16Proper thread-safe implementation for Exninfo.Pierre-Marie Pédrot
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-12-16Error messages of Searchxxx are coherent with goal selector.Pierre Courtieu
2014-12-16Fix for #3154: use CUnix.sys_command to call native compiler.Maxime Dénès
2014-12-15Changed bullet informations to warning for better display in PG.Pierre Courtieu
2014-12-15Adapted test file for About.Pierre Courtieu
2014-12-15Tentatively starting to use heuristics for evar-evar resolution: firstHugo Herbelin
2014-12-15Failing on unbound notation variable in notation level modifiersHugo Herbelin
2014-12-15New try on Fixing an evar_map bug revealed by commit 603b66f81 onHugo Herbelin
2014-12-15Tests for #3848 and #3854.Hugo Herbelin
2014-12-15Documenting check_record + changing a possibly undefined int into int option.Hugo Herbelin
2014-12-15About now accepts hypothesis names and goal selector.Pierre Courtieu
2014-12-15Fix treatment of universe context in typecheck inductive (was addedMatthieu Sozeau
2014-12-15Tests for Searchxxx commands added and modified.Pierre Courtieu
2014-12-15Fixing bug #3865.Pierre-Marie Pédrot
2014-12-14Util.un_op -> Option.defaultPierre Boutillier
2014-12-14Fix merging of name maps in union of universe contexts.Matthieu Sozeau
2014-12-14Fixing bug #3858 and #3817 in one stroke.Pierre-Marie Pédrot
2014-12-14Revert "Fixing bug #3817."Pierre-Marie Pédrot
2014-12-12Add Ltac syntax for the [tclIFCATCH] primitive.Arnaud Spiwack
2014-12-12Make sure the goals on the shelve are identified as goal and unresolvable for...Arnaud Spiwack
2014-12-12Searchxxx now interpret patterns in goal environment if any.Pierre Courtieu
2014-12-12#4843 part 2 : The .cmxs files for plug-ins must have execute permissionPierre Boutillier
2014-12-12Fix #3163 and #3843 part 1 : Cygwin DLLs have extension ".so", not ".dll"Pierre Boutillier
2014-12-12Fix #3800 : cmxs need execution priviledges under windowsPierre Boutillier
2014-12-12An option SimplIsCbnPierre Boutillier
2014-12-12Extend the syntax of simpl with a delta flag.Arnaud Spiwack
2014-12-12Searchxxx now search also the hypothesis and support goal selector.Pierre Courtieu
2014-12-12Two fixes in unification (bugs #3782 and #3709)Matthieu Sozeau
2014-12-12In discrimination nets, do not index lambdas if they're part of a betaMatthieu Sozeau
2014-12-11handling Functional Scheme for required but not imported modulesJulien Forest
2014-12-11List.v: sequel to Sebastien's commit (some cosmetics + a few shorter proofs)Pierre Letouzey
2014-12-11First series of results on lists.Sébastien Hinderer
2014-12-11Commit not ready. Sorry.Hugo Herbelin
2014-12-11Added a CannotSolveConstraint unification error and made experimentsHugo Herbelin
2014-12-11Fine-tuning unification error (using OccurCheck in evarconv).Hugo Herbelin
2014-12-11Tentatively more informative report of failure when inferringHugo Herbelin
2014-12-11Fixing an evar_map bug revealed by commit 603b66f81 on unification flags.Hugo Herbelin
2014-12-11Test suite: keep message in sync with actual file deletions.Xavier Clerc
2014-12-11Ignore *.vi files, just like *.vo files.Xavier Clerc
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 23:19:54 +0000