aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Expand)Author
2016-10-27Fixing #5161 (case of a notation with unability to detect a recursive binder).Hugo Herbelin
2016-10-17Merge PR #310 into v8.5Pierre-Marie Pédrot
2016-10-12Fixing a collision about the meta-variable ".." in recursive notations.Hugo Herbelin
2016-10-06Revert "Make the pretty printer resilient to incomplete nametab (progress on ...Théo Zimmermann
2016-09-12Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.Hugo Herbelin
2016-08-18Fix incorrect glob data for module symbols (bug #2336).Guillaume Melquiond
2016-06-27Univs: allowing notations to take univ instancesMatthieu Sozeau
2016-06-27Forbidding silently dropped universes instances inMatthieu Sozeau
2016-06-07Fix bug #4777: Printing time is impacted by large terms that don't print.Pierre-Marie Pédrot
2016-05-04Increase the size of the dumpglob buffer for cooking notations (bug #4708).Guillaume Melquiond
2016-05-03Fix bug #3825: Universe annotations on notations should pass through or be re...Pierre-Marie Pédrot
2016-04-19Fixing #4677 (collision of a global variable and of a local variableHugo Herbelin
2016-03-03Fixing bug #4105: poor escaping in the protocol between CoqIDE and coqtop.Pierre-Marie Pédrot
2016-02-13Do not give a name to anonymous evars anymore. See bug #4547.Pierre-Marie Pédrot
2016-01-23Implement support for universe binder lists in Instance and Program Fixpoint/...Matthieu Sozeau
2016-01-20Update copyright headers.Maxime Dénès
2016-01-13Fixing #4467 (continued).Hugo Herbelin
2016-01-12Fixing #4467 (missing shadowing of variables in cases pattern).Hugo Herbelin
2015-12-31Do not dump a glob reference when its location is ghost. (Fix bug #4469)Guillaume Melquiond
2015-12-02Fix a bug in externalisation which prevented printing of projectionsMatthieu Sozeau
2015-11-26Make the pretty printer resilient to incomplete nametab (progress on #4363).Enrico Tassi
2015-11-11Fixing bug #3554: Anomaly: Anonymous implicit argument.Pierre-Marie Pédrot
2015-10-26Documenting a bit more interpretation functions in passing.Hugo Herbelin
2015-10-13Fix some typos.Guillaume Melquiond
2015-09-16Properly handle {|...|} patterns when patterns are not asymmetric. (Fix bug #...Guillaume Melquiond
2015-08-21Fixing #4318 (anomaly when applying args to a recursive notation in patterns).Hugo Herbelin
2015-07-29Fixing bug #3811: "Universe annotations confused inside generalizing binders".Pierre-Marie Pédrot
2015-07-27Fixing #4305 (compatibility wrt 8.4 in not interpreting anHugo Herbelin
2015-07-08Make sure that scope classes are displayed by Print Scopes. (Fix bug #4262)Guillaume Melquiond
2015-06-26Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Lionel Rieg
2015-05-27Fix bug #4159Matthieu Sozeau
2015-05-01Fixing computation of implicit arguments by position in fixpoints (#4217).Hugo Herbelin
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-04-21Fixing #3376 and #4191 (wrong index of maximally-inserted implicit argumentHugo Herbelin
2015-04-14Function now supports puniveresjforest
2015-03-30grammar: export hypidentEnrico Tassi
2015-03-27Normalize scope names before storing them in vo files. (Fix for bug #4162)Guillaume Melquiond
2015-03-24Fixing equality of notation_constrs. Fixes bug #4136.Pierre-Marie Pédrot
2015-03-24Revert "Useless check when loading notations through import."Pierre-Marie Pédrot
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2015-02-27Removing the unused field ltacrecvars of tactic internalization.Pierre-Marie Pédrot
2015-02-21Continuing experimentation on what part of the instance of an evarHugo Herbelin
2015-02-12Univs: fix bug #3978: carry around the universe context used toMatthieu Sozeau
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-12-30Fixing #3892: Ensure that notation variables do not capture namesHugo Herbelin
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-12-11Tentatively more informative report of failure when inferringHugo Herbelin
2014-12-04Reactivating option "Set Printing Existential Instances" for asking printing ...Hugo Herbelin
2014-11-27Reverting the following block of three commits:Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 23:29:17 +0000