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
*
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2017-01-23
|
\
|
*
Excluding explicitly coinductive types in Scheme Equality (#5284).
Hugo Herbelin
2016-12-23
|
*
Fixing anomaly EqUnknown in Equality Scheme (#5278).
Hugo Herbelin
2016-12-22
*
|
Fix bug #5069: Scheme Equality gives anomalies in sections.
Pierre-Marie Pédrot
2016-10-02
*
|
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
|
merging conflicts with the original "trunk__CLEANUP__Context__2" branch
Matej Kosik
2016-02-15
|
\
\
*
|
|
Moving conversion functions to the new tactic API.
Pierre-Marie Pédrot
2016-02-15
|
*
|
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
|
/
/
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
*
|
Stronger invariants on the use of the introduction pattern (pat1,...,patn).
Hugo Herbelin
2016-01-21
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
*
|
Moving extended_rel_vect/extended_rel_list to the kernel.
Hugo Herbelin
2015-12-05
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-29
|
\
|
|
*
Avoid type checking private_constants (side_eff) again during Qed (#4357).
Enrico Tassi
2015-10-28
*
|
Boxing the Goal.enter primitive into a record type.
Pierre-Marie Pédrot
2015-10-20
|
/
*
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
[next]