index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
Commit message (
Expand
)
Author
Age
*
Extra check for indirect dependency when abstracting a term which is
Hugo Herbelin
2014-06-28
*
Made the subterm finding function make_abstraction independent of the
Hugo Herbelin
2014-06-28
*
Add an init_setoid check in rewrite to avoid trying to get undefined references.
Matthieu Sozeau
2014-06-27
*
Properly refresh the local hintdb database in case an external tactic changed
Matthieu Sozeau
2014-06-26
*
Incorrect folding of evars in let_tac_gen made remember fail to store
Matthieu Sozeau
2014-06-25
*
In rewrite, wrong computation of the sort of the term to be rewritten in
Matthieu Sozeau
2014-06-25
*
In exact check, use e_type_of to ensure that universe constraints necessary
Matthieu Sozeau
2014-06-25
*
Fix program cases and inversion tactic to correctly record universe constraints.
Matthieu Sozeau
2014-06-24
*
Clenvtac.clenv_refine in the new monad. Not satisfactory though, because it
Pierre-Marie Pédrot
2014-06-24
*
Clenvtac.res_pf is in the new tactic monad.
Pierre-Marie Pédrot
2014-06-24
*
Clenvtac.unify is in the new monad.
Pierre-Marie Pédrot
2014-06-23
*
Removing opens to Clenvtac to track its use more easily.
Pierre-Marie Pédrot
2014-06-23
*
Oops, I fixed the .ml's
Matthieu Sozeau
2014-06-23
*
Fix semantics of change p with c to typecheck c at each specific occurrence o...
Matthieu Sozeau
2014-06-23
*
Less goal-entering.
Pierre-Marie Pédrot
2014-06-22
*
Reindex section variables for typeclass resolution if their type changed.
Matthieu Sozeau
2014-06-21
*
Allow more relaxed conversion between the types of the two terms of a rewrite
Matthieu Sozeau
2014-06-20
*
Add an e_type_of to avoid losing universe constraints.
Matthieu Sozeau
2014-06-20
*
Adding a raw_goals primitive for Tacinterp.
Pierre-Marie Pédrot
2014-06-19
*
- Fix bug in unification, not only named metas are turned into evars (e.g. in...
Matthieu Sozeau
2014-06-19
*
Proofs now take and return an evar_universe_context, simplifying interfaces
Matthieu Sozeau
2014-06-18
*
Removing dead code.
Pierre-Marie Pédrot
2014-06-17
*
Improve hotspot in Auto.
Pierre-Marie Pédrot
2014-06-17
*
Check resolution of Metas turned into Evars by pose_all_metas_as_evars
Hugo Herbelin
2014-06-13
*
Passing some tactics to the new monad type.
Pierre-Marie Pédrot
2014-06-12
*
Fix bug #3291, stack overflow in rewrite.
Matthieu Sozeau
2014-06-11
*
Fix bug #3289
Matthieu Sozeau
2014-06-11
*
In generalized rewrite, avoid retyping completely and constantly the conclusi...
Matthieu Sozeau
2014-06-11
*
fix handling of side effects in abstract (fixes QArithSternBrocot)
Enrico Tassi
2014-06-11
*
Moving hook code from Future to Lemmas. This seemed to disrupt compilation of
Pierre-Marie Pédrot
2014-06-08
*
Enforce a correct exception handling in declaration_hooks
Enrico Tassi
2014-06-08
*
Adding a new Control file centralizing the control options of Coq.
Pierre-Marie Pédrot
2014-06-07
*
Preserve compatibility on examples such as "intros []." on goals such
Hugo Herbelin
2014-06-06
*
Fixes the lost evars when interpreting a change with pattern tactic.
Arnaud Spiwack
2014-06-06
*
Moving the [split] tactic out of the AST.
Pierre-Marie Pédrot
2014-06-06
*
Collecting in Namegen those conventional default names that are used in diffe...
Hugo Herbelin
2014-06-04
*
- Fix hashing of levels to get the "right" order in universe contexts etc...
Matthieu Sozeau
2014-06-04
*
The tactic interpreter now uses a new type of tactics, through
Pierre-Marie Pédrot
2014-06-03
*
Removing symmetry from the atomic tactics.
Pierre-Marie Pédrot
2014-06-02
*
More on injection over a projectable "existT". - Fixing syntax "injection ......
Hugo Herbelin
2014-05-31
*
Fixing introduction patterns * and ** when used in a branch so that they do n...
Hugo Herbelin
2014-05-31
*
Upgrade Matthieu's new_revert as the "revert" (a "unit tactic").
Hugo Herbelin
2014-05-31
*
Removing a tclSENSITIVE from rewrite.
Pierre-Marie Pédrot
2014-05-27
*
- Fix in kernel conversion not folding the universe constraints
Matthieu Sozeau
2014-05-26
*
Revert "Chasing the goal entering backward while interpreting tactics. This r...
Pierre-Marie Pédrot
2014-05-24
*
Chasing the goal entering backward while interpreting tactics. This required
Pierre-Marie Pédrot
2014-05-24
*
Moving the "specialize" tactic out of the AST. Also removed an obsolete
Pierre-Marie Pédrot
2014-05-22
*
Removing useless use of metaids in tactic AST.
Pierre-Marie Pédrot
2014-05-22
*
Removing decompose record / sum from the tactic AST.
Pierre-Marie Pédrot
2014-05-21
*
Allowing Ltac definitions that may be unusable because of a built-in
Pierre-Marie Pédrot
2014-05-21
[next]