aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrintern.ml
Commit message (Expand)AuthorAge
* 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
* cList: set-as-list functions are now with an explicit comparisonGravatar letouzey2013-10-23
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* Removing more association lists in Constrintern.Gravatar ppedrot2013-09-02
* Actually using the domain function for maps.Gravatar ppedrot2013-08-25
* Support Proof GeneralGravatar gareuselesinge2013-08-08
* Removing association lists in Constrintern.Gravatar ppedrot2013-08-07
* Replacing uses of association lists by maps in notations.Gravatar ppedrot2013-08-03
* Useless use of maps in constr internalizing.Gravatar ppedrot2013-06-25
* Using the whole tactic environment while Pretyping.Gravatar ppedrot2013-06-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 14:33:47 +0000