index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
inv.ml
Commit message (
Expand
)
Author
Age
*
Fix program cases and inversion tactic to correctly record universe constraints.
Matthieu Sozeau
2014-06-24
*
Add an e_type_of to avoid losing universe constraints.
Matthieu Sozeau
2014-06-20
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Giving true proof-terms in inversion instead of metas.
Pierre-Marie Pédrot
2014-04-27
*
Removing dead code, thanks to new OCaml warnings and a bit of scripting.
Pierre-Marie Pédrot
2014-04-23
*
Using the new monad tactic in Inv.
Pierre-Marie Pédrot
2014-04-22
*
Removing tactic compatibility layer from Elim.
Pierre-Marie Pédrot
2014-04-22
*
Simplifying interface of elimination tactics. They used dummy clausenvs, and
Pierre-Marie Pédrot
2014-04-22
*
Define Tactics.bring_hyps in the new monad.
Pierre-Marie Pédrot
2014-03-28
*
Removing Tacmach compatibility layer in Inv.
Pierre-Marie Pédrot
2014-03-26
*
Removing tactic compatibility layer from Inv.
Pierre-Marie Pédrot
2014-03-26
*
Moving some tactic code to the new engine.
Pierre-Marie Pédrot
2014-03-26
*
Proofview.Notations: Now that (>>=) is free, use it for tclBIND.
Arnaud Spiwack
2014-02-27
*
Fixing dependent inversion. Some exceptions were not caught by the tactic
Pierre-Marie Pédrot
2014-01-28
*
Remove some occurrences of obsolete operators
Stephane Glondu
2013-11-22
*
Less use of the list-based interface for goal-bound tactics.
aspiwack
2013-11-02
*
Tachmach.New is now in Proofview.Goal.enter style.
aspiwack
2013-11-02
*
More Proofview.Goal.enter.
aspiwack
2013-11-02
*
Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).
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
*
Get rid of the uses of deprecated OCaml elements (still remaining compatible ...
xclerc
2013-09-19
*
Revising r16550 about providing intro patterns for applying injection:
herbelin
2013-07-09
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Minor code cleaning in CArray / CList.
ppedrot
2013-03-23
*
Restrict (try...with...) to avoid catching critical exn (part 10)
letouzey
2013-03-13
*
Modulification of identifier
ppedrot
2012-12-14
*
Monomorphization (tactics)
ppedrot
2012-11-25
*
Improving error message when abtraction over goal (abstract_list_all
herbelin
2012-10-04
*
Remove some more "open" and dead code thanks to OCaml4 warnings
letouzey
2012-10-02
*
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
*
The new ocaml compiler (4.00) has a lot of very cool warnings,
regisgia
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
Tacexpr as a mli-only, the few functions there are now in Tacops
letouzey
2012-05-29
*
locus.mli for occurrences+clauses, misctypes.mli for various little things
letouzey
2012-05-29
*
Noise for nothing
pboutill
2012-03-02
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Made intros_until and onInductionArg a bit stricter and robust
herbelin
2010-06-13
*
Fixed bug #2135 (second-order unification was raising cryptic message)
herbelin
2010-06-12
*
Fixing spelling: pr_coma -> pr_comma
herbelin
2010-06-12
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
A bit of cleaning around name generation + creation of dedicated file namegen.ml
herbelin
2009-11-09
*
Fixing XML doc (COQ_XML not working as an environment variable).
herbelin
2009-10-24
*
Fixed a bug in the interaction between dEqThen and inject_at_positions
herbelin
2009-09-27
*
Delay the choice of eliminator in destruct/induction until we know if
herbelin
2009-09-27
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
- Added two new introduction patterns with the following temptative syntaxes:
herbelin
2009-06-07
[next]