aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrintern.ml
Commit message (Expand)AuthorAge
* 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 #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
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* Fix bug #3289Gravatar Matthieu Sozeau2014-06-11
* Collecting in Namegen those conventional default names that are used in diffe...Gravatar Hugo Herbelin2014-06-04
* - Fix hashing of levels to get the "right" order in universe contexts etc...Gravatar Matthieu Sozeau2014-06-04
* Fix printing of projections with implicits.Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Fixing interpretation of tactics in terms. It was forgetting part of theGravatar Pierre-Marie Pédrot2014-03-06
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Fix grammatical mistake in error message (bug #3238)Gravatar xclerc2014-02-24
* Fixing an interpretation bug with tactics in notations. For some obscureGravatar Pierre-Marie Pédrot2014-01-19
* Disable GlobRef feedback (CoqIDE does nothing with them)Gravatar Enrico Tassi2014-01-05
* Notation variables are now taken into account as possible ltac bound variablesGravatar Pierre-Marie Pédrot2013-12-22
* Notations now accept the $(...)$ tactic-in-term syntax. They are resolved atGravatar Pierre-Marie Pédrot2013-12-22
* Notations can now accept dummy arguments. If ever a bound variable is notGravatar Pierre-Marie Pédrot2013-12-22
* Removing the need of evarmaps in constr internalization.Gravatar Pierre-Marie Pédrot2013-12-17
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
* Fixing bug #3165.Gravatar Pierre-Marie Pédrot2013-11-23
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* cList.index is now cList.index_f, same for index0Gravatar letouzey2013-10-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 02:29:33 +0000