aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrintern.ml
Commit message (Expand)AuthorAge
* Warn about possible shadowing of a name occurring in a "in" clause.Gravatar Hugo Herbelin2016-04-27
* Not taking arguments given by name or position into account whenGravatar Hugo Herbelin2016-04-27
* Fixing a "This clause is redundant" error when interpreting the "in"Gravatar Hugo Herbelin2016-04-27
* Reformatting + removal of some useless data + some cut-eliminationGravatar Hugo Herbelin2016-04-27
* Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Gravatar Matthieu Sozeau2016-04-04
|\
* | Adopting the same rules for interpreting @, abbreviations andGravatar Hugo Herbelin2016-03-13
* | Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Gravatar Hugo Herbelin2016-03-13
* | A more explicit name to the asymmetric boolean flag.Gravatar Hugo Herbelin2016-03-12
* | Printing notations: Cleaning in anticipation of fixing #4592.Gravatar Hugo Herbelin2016-02-28
* | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\ \
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | | CLEANUP: removing unused fieldGravatar Matej Kosik2016-01-11
* | | mergeGravatar Matej Kosik2016-01-11
|\ \ \
| * | | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | | | Remove some unused functions.Gravatar Guillaume Melquiond2016-01-02
* | | | Do not compose List.length with List.filter.Gravatar Guillaume Melquiond2015-12-31
|/ / /
* / / CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedGravatar Matej Kosik2015-12-18
|/ /
* | Fixing bug #3554: Anomaly: Anonymous implicit argument.Gravatar Pierre-Marie Pédrot2015-11-11
* | 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
| * Move type_scope into user space, fix some output logsGravatar Jason Gross2015-08-14
|/
* Fixing #4305 (compatibility wrt 8.4 in not interpreting anGravatar Hugo Herbelin2015-07-27
* Fixing computation of implicit arguments by position in fixpoints (#4217).Gravatar Hugo Herbelin2015-05-01
* Fixing #3376 and #4191 (wrong index of maximally-inserted implicit argumentGravatar Hugo Herbelin2015-04-21
* Removing the unused field ltacrecvars of tactic internalization.Gravatar Pierre-Marie Pédrot2015-02-27
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fixing #3892: Ensure that notation variables do not capture namesGravatar Hugo Herbelin2014-12-30
* Tentatively more informative report of failure when inferringGravatar Hugo Herbelin2014-12-11
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* Parsing evar instances.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Parsing and printing of primitive projections, fix buggy behavior whenGravatar Matthieu Sozeau2014-09-10
* - Fix printing and parsing of primitive projections, including the SetGravatar Matthieu Sozeau2014-09-09
* Parsing of Type@{max(i,j)}.Gravatar Matthieu Sozeau2014-09-08
* Change internalization of primitive projections to allow parsing [p t] asGravatar Matthieu Sozeau2014-08-08
* Revert the change in Constrintern introduced by "Add a type of untyped term t...Gravatar Arnaud Spiwack2014-08-06
* Better fix of e5c025Gravatar Pierre Boutillier2014-08-05
* Fixing #3483 (graceful failing with notations to non-constructors in "match").Gravatar Hugo Herbelin2014-08-03
* Better struture for Ltac internalization environments in Constrintern.Gravatar Pierre-Marie Pédrot2014-08-02
* Faster uconstr.Gravatar Arnaud Spiwack2014-08-01
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
* Finish fixes on notations and primitive projections, add test-suite files for...Gravatar Matthieu Sozeau2014-07-31
* Add a type of untyped term to Ltac's value.Gravatar Arnaud Spiwack2014-07-29
* Fix treatment of notations containing applications of projections (fixes bug ...Gravatar Matthieu Sozeau2014-07-29
* Continue fix on argument scopes of primitive projections.Gravatar Matthieu Sozeau2014-06-17
* Fixing #3282 (two bugs in the presence of let-in's in "fix").Gravatar Hugo Herbelin2014-06-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 22:52:29 +0000