aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.ml
Commit message (Expand)AuthorAge
* Refining 0c320e79ba30 in fixing interpretation of constr under bindersGravatar Hugo Herbelin2015-10-11
* Univs: fix bug #3807Gravatar Matthieu Sozeau2015-10-08
* Univs: add Strict Universe Declaration option (on by default)Gravatar Matthieu Sozeau2015-10-07
* Univs (pretyping): call vm_compute/native_compute with the currentGravatar Matthieu Sozeau2015-10-06
* Univs: fix bug #4251, handling of template polymorphic constants.Gravatar Matthieu Sozeau2015-10-02
* Univs (pretyping): allow parsing and decl of Top.nGravatar Matthieu Sozeau2015-10-02
* Continuing 817308ab (use ltac env for terms in ltac context) + fixGravatar Hugo Herbelin2015-08-02
* Fixing #4221 (interpreting bound variables using ltac env was possiblyGravatar Hugo Herbelin2015-08-02
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Fix some typos in comments.Gravatar Guillaume Melquiond2015-02-23
* Remove some dead code and add test-suite file.Gravatar Matthieu Sozeau2015-02-16
* Update headers.Gravatar Maxime Dénès2015-01-12
* When pretyping [uconstr] closures, don't use the local Ltac variable environm...Gravatar Arnaud Spiwack2014-12-19
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Tentatively more informative report of failure when inferringGravatar Hugo Herbelin2014-12-11
* uconstr: fix bug in interpretation of Ltac-bound name in let-tuple and patter...Gravatar Arnaud Spiwack2014-11-19
* Fixing bug #3792.Gravatar Pierre-Marie Pédrot2014-11-09
* Fixing confused code for interpretations of evar instances.Gravatar Hugo Herbelin2014-11-03
* Fixing inefficiency in typeclass resolution.Gravatar Pierre-Marie Pédrot2014-11-03
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Build unfolded versions of the primitive projection in let (a, p) := ...Gravatar Matthieu Sozeau2014-10-07
* Fixing interpretation of constr under binders which was broken afterGravatar Hugo Herbelin2014-10-02
* 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
* Fixes in Ltac pattern-matching on primitive projectionsGravatar Matthieu Sozeau2014-09-19
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
* Fix: when interpreting a identifier in pretying, use the Ltac identifier subs...Gravatar Arnaud Spiwack2014-09-15
* Fix a bug in the naming of binders.Gravatar Arnaud Spiwack2014-09-15
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Checking typability of evar instances. Using ";" to separate bindingsGravatar Hugo Herbelin2014-09-13
* 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 of Type@{max(i,j)}.Gravatar Matthieu Sozeau2014-09-08
* The pretyping of [uconstr] in [refine] uses the identifier of the ltac contex...Gravatar Arnaud Spiwack2014-09-05
* Adds an identifier context in pretying's Ltac context.Gravatar Arnaud Spiwack2014-09-05
* Change the way primitive projections are declared to the kernel.Gravatar Matthieu Sozeau2014-08-28
* Better structure for Ltac pretyping environments.Gravatar Pierre-Marie Pédrot2014-08-07
* [uconstr]: use a closure instead of eager substitution.Gravatar Arnaud Spiwack2014-08-06
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
* Add toplevel commands to declare global universes and constraints.Gravatar Matthieu Sozeau2014-07-01
* Quickly fixing bug #2996: typing functions now check when referring toGravatar Hugo Herbelin2014-06-28
* Change interface of refresh universes to get a pbty argument instead ofGravatar Matthieu Sozeau2014-06-26
* Fix for bug 1951, allowing at least fully-applied inductives types to be usedGravatar Matthieu Sozeau2014-06-23
* Fixed some HoTT bugs, provide a proper error message when giving an ill-formedGravatar Matthieu Sozeau2014-06-20
* Cleanup treatment of template universe polymorphism (thanks to E. TassiGravatar Matthieu Sozeau2014-06-20
* 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 type inference of the record argument of a projection to catch ill-typedGravatar Matthieu Sozeau2014-06-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 05:27:01 +0000