aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
Commit message (Expand)AuthorAge
* Univs: allowing notations to take univ instancesGravatar Matthieu Sozeau2016-06-27
* Forbidding silently dropped universes instances inGravatar Matthieu Sozeau2016-06-27
* Fix bug #4777: Printing time is impacted by large terms that don't print.Gravatar Pierre-Marie Pédrot2016-06-07
* Increase the size of the dumpglob buffer for cooking notations (bug #4708).Gravatar Guillaume Melquiond2016-05-04
* Fix bug #3825: Universe annotations on notations should pass through or be re...Gravatar Pierre-Marie Pédrot2016-05-03
* Fixing #4677 (collision of a global variable and of a local variableGravatar Hugo Herbelin2016-04-19
* Fixing bug #4105: poor escaping in the protocol between CoqIDE and coqtop.Gravatar Pierre-Marie Pédrot2016-03-03
* Do not give a name to anonymous evars anymore. See bug #4547.Gravatar Pierre-Marie Pédrot2016-02-13
* Implement support for universe binder lists in Instance and Program Fixpoint/...Gravatar Matthieu Sozeau2016-01-23
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Fixing #4467 (continued).Gravatar Hugo Herbelin2016-01-13
* Fixing #4467 (missing shadowing of variables in cases pattern).Gravatar Hugo Herbelin2016-01-12
* Do not dump a glob reference when its location is ghost. (Fix bug #4469)Gravatar Guillaume Melquiond2015-12-31
* Fix a bug in externalisation which prevented printing of projectionsGravatar Matthieu Sozeau2015-12-02
* Make the pretty printer resilient to incomplete nametab (progress on #4363).Gravatar Enrico Tassi2015-11-26
* Fixing bug #3554: Anomaly: Anonymous implicit argument.Gravatar Pierre-Marie Pédrot2015-11-11
* Documenting a bit more interpretation functions in passing.Gravatar Hugo Herbelin2015-10-26
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* Properly handle {|...|} patterns when patterns are not asymmetric. (Fix bug #...Gravatar Guillaume Melquiond2015-09-16
* Fixing #4318 (anomaly when applying args to a recursive notation in patterns).Gravatar Hugo Herbelin2015-08-21
* Fixing bug #3811: "Universe annotations confused inside generalizing binders".Gravatar Pierre-Marie Pédrot2015-07-29
* Fixing #4305 (compatibility wrt 8.4 in not interpreting anGravatar Hugo Herbelin2015-07-27
* Make sure that scope classes are displayed by Print Scopes. (Fix bug #4262)Gravatar Guillaume Melquiond2015-07-08
* Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Gravatar Lionel Rieg2015-06-26
* Fix bug #4159Gravatar Matthieu Sozeau2015-05-27
* Fixing computation of implicit arguments by position in fixpoints (#4217).Gravatar Hugo Herbelin2015-05-01
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Fixing #3376 and #4191 (wrong index of maximally-inserted implicit argumentGravatar Hugo Herbelin2015-04-21
* Function now supports puniveresGravatar jforest2015-04-14
* grammar: export hypidentGravatar Enrico Tassi2015-03-30
* Normalize scope names before storing them in vo files. (Fix for bug #4162)Gravatar Guillaume Melquiond2015-03-27
* Fixing equality of notation_constrs. Fixes bug #4136.Gravatar Pierre-Marie Pédrot2015-03-24
* Revert "Useless check when loading notations through import."Gravatar Pierre-Marie Pédrot2015-03-24
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* Removing the unused field ltacrecvars of tactic internalization.Gravatar Pierre-Marie Pédrot2015-02-27
* Continuing experimentation on what part of the instance of an evarGravatar Hugo Herbelin2015-02-21
* Univs: fix bug #3978: carry around the universe context used toGravatar Matthieu Sozeau2015-02-12
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fixing #3892: Ensure that notation variables do not capture namesGravatar Hugo Herbelin2014-12-30
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Tentatively more informative report of failure when inferringGravatar Hugo Herbelin2014-12-11
* Reactivating option "Set Printing Existential Instances" for asking printing ...Gravatar Hugo Herbelin2014-12-04
* Reverting the following block of three commits:Gravatar Hugo Herbelin2014-11-27
* Experimenting always forcing convertibility on strict implicit argumentsGravatar Hugo Herbelin2014-11-26
* Printing function for [uconstr].Gravatar Arnaud Spiwack2014-11-19
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
* Fixing what really looks like a bug in the initial implementation ofGravatar Hugo Herbelin2014-10-22
* A patch for printing "match" when constructors are defined with let-inGravatar Hugo Herbelin2014-10-20
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 22:39:10 +0000