index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
leminv.ml
Commit message (
Expand
)
Author
Age
*
Univs: local names handling.
Matthieu Sozeau
2015-10-28
*
Fix some typos.
Guillaume Melquiond
2015-10-13
*
Univs: Add universe binding lists to definitions
Matthieu Sozeau
2015-09-14
*
Fix bug #2775: Correct handling of universes in leminv.
Matthieu Sozeau
2015-02-12
*
Update headers.
Maxime Dénès
2015-01-12
*
Switch the few remaining iso-latin-1 files to utf8
Pierre Letouzey
2014-12-09
*
Uniformisation of the order of arguments env and sigma.
Hugo Herbelin
2014-09-12
*
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-09-12
*
Renaming goal-entering functions.
Pierre-Marie Pédrot
2014-09-06
*
Clenvtac.res_pf is in the new tactic monad.
Pierre-Marie Pédrot
2014-06-24
*
Proofs now take and return an evar_universe_context, simplifying interfaces
Matthieu Sozeau
2014-06-18
*
- Fix bug preventing apply from unfolding Fixpoints.
Matthieu Sozeau
2014-05-06
*
Rework handling of universes on top of the STM, allowing for delayed
Matthieu Sozeau
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Removing dead code, thanks to new OCaml warnings and a bit of scripting.
Pierre-Marie Pédrot
2014-04-23
*
Removing the compatibility layer from Leminv. Also removed an undocumented
Pierre-Marie Pédrot
2014-04-22
*
Define Tactics.bring_hyps in the new monad.
Pierre-Marie Pédrot
2014-03-28
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Qed: feedback when type checking is done
Enrico Tassi
2013-12-24
*
Allowing proofs starting with a non-empty evarmap.
ppedrot
2013-11-04
*
Tachmach.New is now in Proofview.Goal.enter style.
aspiwack
2013-11-02
*
More Proofview.Goal.enter.
aspiwack
2013-11-02
*
The tactic [admit] exits with the "unsafe" status.
aspiwack
2013-11-02
*
Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.
aspiwack
2013-11-02
*
Getting rid of Goal.here, and all the related exceptions and combinators.
aspiwack
2013-11-02
*
Makes the new Proofview.tactic the basic type of Ltac.
aspiwack
2013-11-02
*
More monomorphic List.mem + List.assoc + ...
letouzey
2013-10-24
*
Moving side effects into evar_map. There was no reason to keep another
ppedrot
2013-10-05
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Merging Context and Sign.
ppedrot
2013-04-29
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Added a Local Definition vernacular command. This type of definition
ppedrot
2013-03-11
*
New implementation of the conversion test, using normalization by evaluation to
mdenes
2013-01-22
*
Modulification of identifier
ppedrot
2012-12-14
*
Moving Utils.list_* to a proper CList module, which includes stdlib
ppedrot
2012-09-14
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
Noise for nothing
pboutill
2012-03-02
*
Proof using ...
gareuselesinge
2011-12-12
*
Moved allow_K to a unification flag
herbelin
2011-06-10
*
Revert "Add [Polymorphic] flag for defs"
msozeau
2011-04-13
*
Add [Polymorphic] flag for defs
msozeau
2011-04-13
*
Remove the "Boxed" syntaxes and the const_entry_boxed field
letouzey
2011-01-28
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Fixed bug #2314 (inversion using not checking the correctness of its arguments
herbelin
2010-06-13
*
Fixing Derive Inversion for new proof engine
herbelin
2010-05-26
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Here comes the commit, announced long ago, of the new tactic engine.
aspiwack
2010-04-22
*
A bit of cleaning around name generation + creation of dedicated file namegen.ml
herbelin
2009-11-09
[next]