aboutsummaryrefslogtreecommitdiff
path: root/pretyping/pretyping.ml
AgeCommit message (Expand)Author
2016-06-15Allow `Pretyping.search_guard` to not check guardArnaud Spiwack
2016-06-14Assume totality: dedicated type rather than boolArnaud Spiwack
2016-04-05Revert "Prevent pretyping from checking well-guardedness unnecessarily."Arnaud Spiwack
2015-09-25Prevent pretyping from checking well-guardedness unnecessarily.Arnaud Spiwack
2015-06-26Add a flag to deactivate guard checking in the kernel.Arnaud Spiwack
2015-05-13Safer typing primitives.Pierre-Marie Pédrot
2015-02-23Fix some typos in comments.Guillaume Melquiond
2015-02-16Remove some dead code and add test-suite file.Matthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-12-19When pretyping [uconstr] closures, don't use the local Ltac variable environm...Arnaud Spiwack
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-12-11Tentatively more informative report of failure when inferringHugo Herbelin
2014-11-19uconstr: fix bug in interpretation of Ltac-bound name in let-tuple and patter...Arnaud Spiwack
2014-11-09Fixing bug #3792.Pierre-Marie Pédrot
2014-11-03Fixing confused code for interpretations of evar instances.Hugo Herbelin
2014-11-03Fixing inefficiency in typeclass resolution.Pierre-Marie Pédrot
2014-10-25This commit introduces changes in induction and destruct.Hugo Herbelin
2014-10-07Build unfolded versions of the primitive projection in let (a, p) := ...Matthieu Sozeau
2014-10-02Fixing interpretation of constr under binders which was broken afterHugo Herbelin
2014-09-30Add syntax for naming new goals in refine: writing ?[id] instead of _Hugo Herbelin
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-09-19Fixes in Ltac pattern-matching on primitive projectionsMatthieu Sozeau
2014-09-17Revert specific syntax for primitive projections, avoiding uglyMatthieu Sozeau
2014-09-15Fix: when interpreting a identifier in pretying, use the Ltac identifier subs...Arnaud Spiwack
2014-09-15Fix a bug in the naming of binders.Arnaud Spiwack
2014-09-13Providing a -type-in-type option for collapsing the universe hierarchy.Hugo Herbelin
2014-09-13Checking typability of evar instances. Using ";" to separate bindingsHugo Herbelin
2014-09-12Uniformisation of the order of arguments env and sigma.Hugo Herbelin
2014-09-12Parsing evar instances.Hugo Herbelin
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-09-08Parsing of Type@{max(i,j)}.Matthieu Sozeau
2014-09-05The pretyping of [uconstr] in [refine] uses the identifier of the ltac contex...Arnaud Spiwack
2014-09-05Adds an identifier context in pretying's Ltac context.Arnaud Spiwack
2014-08-28Change the way primitive projections are declared to the kernel.Matthieu Sozeau
2014-08-07Better structure for Ltac pretyping environments.Pierre-Marie Pédrot
2014-08-06[uconstr]: use a closure instead of eager substitution.Arnaud Spiwack
2014-08-03Move to a representation of universe polymorphic constants using indices for ...Matthieu Sozeau
2014-08-01A tentative uniform naming policy in module Inductiveops.Hugo Herbelin
2014-07-01Add toplevel commands to declare global universes and constraints.Matthieu Sozeau
2014-06-28Quickly fixing bug #2996: typing functions now check when referring toHugo Herbelin
2014-06-26Change interface of refresh universes to get a pbty argument instead ofMatthieu Sozeau
2014-06-23Fix for bug 1951, allowing at least fully-applied inductives types to be usedMatthieu Sozeau
2014-06-20Fixed some HoTT bugs, provide a proper error message when giving an ill-formedMatthieu Sozeau
2014-06-20Cleanup treatment of template universe polymorphism (thanks to E. TassiMatthieu Sozeau
2014-06-17Fixing #3282 (two bugs in the presence of let-in's in "fix").Hugo Herbelin
2014-06-17Removing dead code.Pierre-Marie Pédrot
2014-06-17Fix type inference of the record argument of a projection to catch ill-typedMatthieu Sozeau
2014-06-11In generalized rewrite, avoid retyping completely and constantly the conclusi...Matthieu Sozeau
2014-06-04Collecting in Namegen those conventional default names that are used in diffe...Hugo Herbelin
2014-06-04- Fix hashing of levels to get the "right" order in universe contexts etc...Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 13:26:44 +0000