index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
auto_ind_decl.ml
Commit message (
Expand
)
Author
Age
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Avoid type checking private_constants (side_eff) again during Qed (#4357).
Enrico Tassi
2015-10-28
*
Fix after rebase...
Matthieu Sozeau
2015-10-02
*
Univs: fix environment handling in scheme building.
Matthieu Sozeau
2015-10-02
*
Hopefully better names to constructors of internal_flag, as discussed
Hugo Herbelin
2015-09-23
*
Give a way to control if the decidable-equality schemes are built like
Hugo Herbelin
2015-09-23
*
Removing the generalization of the body of inductive schemes from
Hugo Herbelin
2015-09-23
*
Reverting 16 last commits, committed mistakenly using the wrong push command.
Hugo Herbelin
2015-08-02
*
Give a way to control if the decidable-equality schemes are built like
Hugo Herbelin
2015-08-02
*
Removing the generalization of the body of inductive schemes from
Hugo Herbelin
2015-08-02
*
Fixing bug #3736 (anomaly instead of error/warning/silence on
Hugo Herbelin
2015-07-27
*
Safer typing primitives.
Pierre-Marie Pédrot
2015-05-13
*
Remove almost all the uses of string concatenation when building error messages.
Guillaume Melquiond
2015-04-23
*
Using tclZEROMSG instead of tclZERO in several places.
Pierre-Marie Pédrot
2015-04-23
*
Update headers.
Maxime Dénès
2015-01-12
*
Fixing Scheme Equality, after bug introduced in bf018569405c.
Hugo Herbelin
2014-11-13
*
This commit introduces changes in induction and destruct.
Hugo Herbelin
2014-10-25
*
Renaming goal-entering functions.
Pierre-Marie Pédrot
2014-09-06
*
Reorganisation of intropattern code
Hugo Herbelin
2014-08-18
*
Reorganization of tactics:
Hugo Herbelin
2014-08-18
*
Experimentally adding an option for automatically erasing an
Hugo Herbelin
2014-08-05
*
Proofs now take and return an evar_universe_context, simplifying interfaces
Matthieu Sozeau
2014-06-18
*
Renaming new_induct -> induction; new_destruct -> destruct.
Hugo Herbelin
2014-05-08
*
- Fix bug preventing apply from unfolding Fixpoints.
Matthieu Sozeau
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Removing useless try-with clauses in Goal.enter variants.
Pierre-Marie Pédrot
2014-04-25
*
Removing dead code in Tactics.
Pierre-Marie Pédrot
2014-03-31
*
Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.
Pierre-Marie Pédrot
2014-03-26
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Proofview.Notations: Now that (>>=) is free, use it for tclBIND.
Arnaud Spiwack
2014-02-27
*
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 a warning.
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
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Making the behavior of "injection ... as ..." more natural:
herbelin
2013-06-02
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Restrict (try...with...) to avoid catching critical exn (part 13)
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 10)
letouzey
2013-03-13
*
use List.rev_map whenever possible
letouzey
2013-02-18
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Array.create is deprecated
pboutill
2012-12-19
*
Modulification of Label
ppedrot
2012-12-18
*
Modulification of identifier
ppedrot
2012-12-14
[next]