index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
proofs
Commit message (
Expand
)
Author
Age
*
Restrict (try...with...) to avoid catching critical exn (part 12)
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 5)
letouzey
2013-03-13
*
invalid_arg instead of raise (Invalid_argement ...)
letouzey
2013-03-12
*
Allowing different types of, not to be mixed, generic Stores through
ppedrot
2013-03-12
*
Removing Exc_located and using the new exception enrichement
ppedrot
2013-02-18
*
Added propagation of evars unification failure reasons for better
herbelin
2013-02-17
*
Revised the Ltac trace mechanism so that trace breaking due to
herbelin
2013-02-17
*
No reason a priori for using unfiltered env for printing
herbelin
2013-01-29
*
Fixing bug #2969 (admit failing after Grab Existential Variables due
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
*
Reductionops: whd_state_gen can take and answers a cst_stack too
pboutill
2013-01-24
*
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
*
Fixed a little inefficiency of "set/destruct" over a pattern. Now
herbelin
2012-12-18
*
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
*
Renamed Option.Misc.compare to the more uniform Option.equal.
ppedrot
2012-12-13
*
Monomorphization (proof)
ppedrot
2012-11-25
*
Monomorphized a lot of equalities over OCaml integers, thanks to
ppedrot
2012-11-08
*
Fix bug #2892
letouzey
2012-10-22
*
still some more dead code removal
letouzey
2012-10-06
*
remove Refiner.abstract_tactic and similar
letouzey
2012-10-06
*
Clean-up : removal of Proof_type.tactic_expr
letouzey
2012-10-06
*
Proof_type: rule now degenerates to prim_rule
letouzey
2012-10-06
*
Clean-up : no more Proof_type.proof_tree
letouzey
2012-10-06
*
Clean-up of proof_type.ml : no more Nested nor abstract_tactic_box
letouzey
2012-10-06
*
Remove the unused "intel" field in Proof.proof_state
letouzey
2012-10-02
*
Remove some more "open" and dead code thanks to OCaml4 warnings
letouzey
2012-10-02
*
Use the library function List.substract in prev commit
letouzey
2012-10-02
*
Added a new tactical infoH tac, that displays the names of hypothesis created...
courtieu
2012-10-01
*
As r15801: putting everything from Util.array_* to CArray.*.
ppedrot
2012-09-14
*
Partial revert of Yann commit in order to use CLib.List when opening
ppedrot
2012-09-14
*
Moving Utils.list_* to a proper CList module, which includes stdlib
ppedrot
2012-09-14
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
The new ocaml compiler (4.00) has a lot of very cool warnings,
regisgia
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
Reductionops refactoring
pboutill
2012-07-20
*
Severe reorganisation of the code of tactics in Proofview.
aspiwack
2012-07-11
*
Small change in the printing of proofs for use by coqide.
aspiwack
2012-07-10
*
Change how the number of open goals is printed.
aspiwack
2012-07-04
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
Forward-port fixes from 8.4 (15358, 15353, 15333).
msozeau
2012-06-04
*
Cleaning Pp.ppnl use
ppedrot
2012-06-01
*
Getting rid of Pp.msgnl and Pp.message.
ppedrot
2012-06-01
[next]