index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
tactics
/
extratactics.ml4
Age
Commit message (
Expand
)
Author
2016-03-21
Creating a dedicated ltac/ folder for Hightactics.
Pierre-Marie Pédrot
2016-03-20
Moving Refine to its proper module.
Pierre-Marie Pédrot
2016-03-17
Removing the special status of generic arguments defined by Coq itself.
Pierre-Marie Pédrot
2016-03-17
Removing the special status of generic entries defined by Coq itself.
Pierre-Marie Pédrot
2016-03-17
Removing the registering of default values for generic arguments.
Pierre-Marie Pédrot
2016-02-24
Getting rid of the "<:tactic< ... >>" quotations.
Pierre-Marie Pédrot
2016-02-22
The tactic generic argument now returns a value rather than a glob_expr.
Pierre-Marie Pédrot
2016-02-15
Using monotonic types for conversion functions.
Pierre-Marie Pédrot
2016-01-21
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2016-01-11
merge
Matej Kosik
2016-01-11
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2015-12-28
Eradicating uses of open_constr in TACTIC EXTEND in favour of uconstr.
Pierre-Marie Pédrot
2015-12-27
Factorizing code for untyped constr evaluation.
Pierre-Marie Pédrot
2015-12-27
Tentative API fix for tactic arguments to be fed to tclWITHHOLES.
Pierre-Marie Pédrot
2015-12-21
Changing the toplevel type of the int_or_var generic type to int.
Pierre-Marie Pédrot
2015-12-17
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-16
FIx parsing of tactic "simple refine".
Maxime Dénès
2015-12-16
Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".
Guillaume Melquiond
2015-12-15
Refine tactic now shelves unifiable holes.
Pierre-Marie Pédrot
2015-12-15
Changing the order of the goals generated by unshelve.
Pierre-Marie Pédrot
2015-12-11
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-09
Fixing parsing of the unshelve tactical.
Pierre-Marie Pédrot
2015-12-09
Adding an unshelve tactical.
Pierre-Marie Pédrot
2015-12-05
Removing redundant versions of generalize.
Hugo Herbelin
2015-12-05
Moving extended_rel_vect/extended_rel_list to the kernel.
Hugo Herbelin
2015-12-05
Moving three related small half-general half-ad-hoc utility functions
Hugo Herbelin
2015-11-29
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-27
Fix [Polymorphic Hint Rewrite].
Matthieu Sozeau
2015-10-29
Removing the evar_map argument from s_enter.
Pierre-Marie Pédrot
2015-10-20
Proofview.Goal.sigma returns an indexed evarmap.
Pierre-Marie Pédrot
2015-10-20
Boxing the Goal.enter primitive into a record type.
Pierre-Marie Pédrot
2015-10-20
Renaming Goal.enter field into s_enter.
Pierre-Marie Pédrot
2015-10-19
Removing tclEVARS in various places.
Pierre-Marie Pédrot
2015-10-18
Constraining refine to monotonic functions.
Pierre-Marie Pédrot
2015-10-17
Clarifying and documenting the UState API.
Pierre-Marie Pédrot
2015-10-02
Univs: refined handling of assumptions
Matthieu Sozeau
2015-10-02
Univs: fix evar_map handling in Hint processing.
Matthieu Sozeau
2015-10-02
Univs: fix many evar_map initializations and leaks.
Matthieu Sozeau
2015-09-23
Hopefully better names to constructors of internal_flag, as discussed
Hugo Herbelin
2015-05-27
Fix bug #4159
Matthieu Sozeau
2015-05-13
Safer typing primitives.
Pierre-Marie Pédrot
2015-04-23
Using tclZEROMSG instead of tclZERO in several places.
Pierre-Marie Pédrot
2015-04-22
Tactical `progress` compares term up to potentially equalisable universes.
Arnaud Spiwack
2015-03-11
admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)
Enrico Tassi
2015-02-10
More expressive API for tclWITHHOLES.
Pierre-Marie Pédrot
2015-02-10
Revert "Removing spurious tclWITHHOLES."
Pierre-Marie Pédrot
2015-01-12
Update headers.
Maxime Dénès
2014-12-16
Getting rid of Exninfo hacks.
Pierre-Marie Pédrot
2014-12-07
Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.
Hugo Herbelin
[next]
