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
*
Embedded exns in LtacLocated and EvaluatedError satisfy Errors.noncritical
letouzey
2013-03-14
*
Restrict (try...with...) to avoid catching critical exn (part 13)
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 11)
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 10)
letouzey
2013-03-13
*
Hipattern : consider jmeq only when Logic.JMeq is loaded
letouzey
2013-03-12
*
Equality: avoid an anomaly about inj_pair2_eq_dec
letouzey
2013-03-12
*
invalid_arg instead of raise (Invalid_argement ...)
letouzey
2013-03-12
*
Added a Local Definition vernacular command. This type of definition
ppedrot
2013-03-11
*
kernel/declarations becomes a pure mli
letouzey
2013-02-26
*
Dir_path --> DirPath
letouzey
2013-02-19
*
Removing Exc_located and using the new exception enrichement
ppedrot
2013-02-18
*
Minor code cleanups, especially take advantage of Dir_path.is_empty
letouzey
2013-02-18
*
Revised the Ltac trace mechanism so that trace breaking due to
herbelin
2013-02-17
*
Fixed #2970 (made that remember's eqn name is interpretable as an ltac var).
herbelin
2013-01-29
*
Fixed synchronicity of filter with evar context in new_goal_with.
herbelin
2013-01-29
*
Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_env
herbelin
2013-01-29
*
Actually adding backtrace handling.
ppedrot
2013-01-28
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Added backtrace information to anomalies
ppedrot
2013-01-28
*
New implementation of the conversion test, using normalization by evaluation to
mdenes
2013-01-22
*
Yet a new reduction tactic in Coq : cbn
pboutill
2012-12-21
*
Modulification of name
ppedrot
2012-12-18
*
Modulification of Label
ppedrot
2012-12-18
*
Fixed a little inefficiency of "set/destruct" over a pattern. Now
herbelin
2012-12-18
*
Modulification of dir_path
ppedrot
2012-12-14
*
Modulification of identifier
ppedrot
2012-12-14
*
Moved Stringset and Stringmap to String namespace.
ppedrot
2012-12-14
*
Moved Intset and Intmap to Int namespace.
ppedrot
2012-12-14
*
Using library string functions.
ppedrot
2012-12-13
*
Renamed Option.Misc.compare to the more uniform Option.equal.
ppedrot
2012-12-13
*
Finish patch for Hint Resolve, stopping to generate new constant names for
msozeau
2012-12-08
*
Monomorphization (tactics)
ppedrot
2012-11-25
*
Taking into account the type of a definition (if it exists), and the
herbelin
2012-11-17
*
Added a CString module.
ppedrot
2012-11-13
*
Monomorphized a lot of equalities over OCaml integers, thanks to
ppedrot
2012-11-08
*
Change [Hints Resolve] to still accept constrs as arguments
msozeau
2012-10-31
*
Removed many calls to OCaml generic equality. This was done by
ppedrot
2012-10-29
*
Change Hint Resolve, Immediate to take a global reference as argument
msozeau
2012-10-26
*
Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp
letouzey
2012-10-16
*
Continue killing hidden tactics : no more generated h_xxx
letouzey
2012-10-15
*
still some more dead code removal
letouzey
2012-10-06
*
remove useless hidden_flag in TacMutual(Co)Fix
letouzey
2012-10-06
*
cosmetic concerning interp of TacShowHyps
letouzey
2012-10-06
*
remove Refiner.abstract_tactic and similar
letouzey
2012-10-06
*
Adapt pieces of code needing -rectypes
letouzey
2012-10-06
*
Clean-up : removal of Proof_type.tactic_expr
letouzey
2012-10-06
*
Clean-up of proof_type.ml : no more Nested nor abstract_tactic_box
letouzey
2012-10-06
*
Revert r15851 "En cours pour bug 2836".
herbelin
2012-10-04
*
Improving error message when abtraction over goal (abstract_list_all
herbelin
2012-10-04
*
En cours pour bug 2836
herbelin
2012-10-04
[next]