8000 Commits · ppedrot/unicoq · GitHub

More Web Proxy on the site http://driver.im/

Commits

Commits on Apr 25, 2018

mainly avoid aborting on undefined evars in to_constr, also some renaming of evd with sigma to make it clearer
Beta Ziliani
committed

Commits on Apr 24, 2018

updated to changes in EConstr
Beta Ziliani
committed

Commits on Apr 18, 2018

ported to current master (after 8.8). most notably, falling to evarconv for things like universes
Beta Ziliani
committed

Commits on Apr 4, 2018

one type of warning is left (40), with an explanation why
beta-ziliani
committed

Commits on Feb 7, 2018

adding support for cumul inductives
Beta Ziliani
committed

Commits on Dec 24, 2017

a few things fixed, most notably the recursion of the decomposition of head element
Beta Ziliani
committed

Commits on Nov 12, 2017

Allow to be polymorphic.
Janno
committed

Commits on Nov 10, 2017

Rebase v1.2 and make it compile.
Janno
committed
added interface for running mtac functions

Beta Ziliani
authored and
Janno
committed
Switch back to .mllib to produce .cmxa file.
Janno
committed

Commits on Nov 4, 2017

casts are erased
Beta Ziliani
committed

Commits on Nov 3, 2017

Ported to Coq 8.7, not working yet.
ejgallego
committed

Commits on Feb 20, 2017

Commits on Jan 9, 2017

ported to 8.6 but without using the new sigma interface
Beta Ziliani
committed

Commits on Nov 4, 2016

removed occurs check since pruning is doing it
Beta Ziliani
committed

Commits on Oct 28, 2016

the whole set of unification problems in MathComp in one tex file. not for compiling (is it 1.3Gb when uncompressed) but useful to search for patterns of usage
Beta Ziliani
committed

Commits on Oct 24, 2016

removed unification of types prior to unification of definitions in Let-Same
Beta Ziliani
committed

Commits on Aug 7, 2016

Correct unification of polymorphic const/inds/constrs
mattam82
committed

Commits on Aug 4, 2016

unification without reduction
Beta Ziliani
committed

Commits on Jul 8, 2016

comment for unify_match
Beta Ziliani
committed
cleaning up some code and commenting
Beta Ziliani
committed

Commits on May 4, 2016

matching was potentially instantiating evars outside the given evar set
Beta Ziliani
committed
little refactoring
Beta Ziliani
committed

Commits on May 3, 2016

the parameters for equating a type were wrong. now it allows reducing and instantiating on either side (but only those evars in the set)
Beta Ziliani
committed
parameters adjuted for instantiation
Beta Ziliani
committed
Applied patch by @yurug to make recursive modules work
Beta Ziliani
committed

Commits on Apr 29, 2016

still trying get recursive modules to work...
Beta Ziliani
committed

Commits on Apr 20, 2016

trying to make a recursive module...
Beta Ziliani
committed

Commits on Apr 13, 2016

little refactor for clarity
Beta Ziliani
committed
Added option to just dump equalities as they show up, and added ismatch
Beta Ziliani
committed

Commits on Apr 12, 2016

Some of the parameters of the function are now parametrized in a module (for the moment, only the transparent state, but soon there will be more)
Beta Ziliani
committed

Commits on Apr 11, 2016

closed section
Beta Ziliani
committed
removed unused var
Beta Ziliani
committed

Commits on Apr 1, 2016

fixed bug introduced in 67de83031366432c4ee40d92e1e0ee3b2f6319af
Beta Ziliani
committed

0