index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
Commit message (
Expand
)
Author
Age
*
Dir_path --> DirPath
letouzey
2013-02-19
*
Classops : avoid some use of Gmap
letouzey
2013-02-19
*
use List.rev_map whenever possible
letouzey
2013-02-18
*
Minor code cleanups, especially take advantage of Dir_path.is_empty
letouzey
2013-02-18
*
Extraction: same as commit 16203, hopefully without NotASort exns
letouzey
2013-02-18
*
Fix extraction of inductive types that Coq auto-detects to be in Prop
letouzey
2013-02-14
*
No reason a priori for using unfiltered env for printing
herbelin
2013-01-29
*
Fixed synchronicity of filter with evar context in new_goal_with.
herbelin
2013-01-29
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
New implementation of the conversion test, using normalization by evaluation to
mdenes
2013-01-22
*
Unset Asymmetric Patterns
pboutill
2013-01-18
*
Array.create is deprecated
pboutill
2012-12-19
*
Modulification of name
ppedrot
2012-12-18
*
Modulification of mod_bound_id
ppedrot
2012-12-18
*
Modulification of Label
ppedrot
2012-12-18
*
Extraction: qualified names in Extract Constant examples (fix #2878)
letouzey
2012-12-18
*
No more constant named "int" in Coq theories (cf bug #2878)
letouzey
2012-12-18
*
Extraction of projections: restrict a hack to ocaml only (fix #2941)
letouzey
2012-12-17
*
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
*
Ensure that a function declared with a label is used with it
letouzey
2012-12-08
*
Taking into account the type of a definition (if it exists), and the
herbelin
2012-11-17
*
More monomorphizations
ppedrot
2012-11-13
*
Added a CString module.
ppedrot
2012-11-13
*
Monomorphized a lot of equalities over OCaml integers, thanks to
ppedrot
2012-11-08
*
correcting a little bug in Function
jforest
2012-10-31
*
Extraction Implicit: consider the parameters of a constructor (fix #2905)
letouzey
2012-10-30
*
Extraction: avoid initial strange empty comments after Arnaud's hack
letouzey
2012-10-30
*
Fix Separate extraction when a module-as-file is aliased (#2917)
letouzey
2012-10-30
*
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
*
still some more dead code removal
letouzey
2012-10-06
*
remove useless hidden_flag in TacMutual(Co)Fix
letouzey
2012-10-06
*
remove dumptree.ml4
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
*
Moved Compat to parsing. This permits to break the dependency of the
ppedrot
2012-10-04
*
Remove some more "open" and dead code thanks to OCaml4 warnings
letouzey
2012-10-02
*
Ltac repeat is in fact already doing progress
letouzey
2012-10-01
*
Cleaning, renaming obscure functions and documenting in Hashcons.
ppedrot
2012-09-26
*
Fixing a bug introduced in Funind plugin when reorganizing the CList
ppedrot
2012-09-24
*
More cleaning in CArray...
ppedrot
2012-09-18
*
More cleanup of Util: utf8 aspects moved to a new file unicode.ml
letouzey
2012-09-18
*
Cleaning interface of Util.
ppedrot
2012-09-18
*
More cleaning on Utils and CList. Some parts of the code being
ppedrot
2012-09-17
*
Some documentation and cleaning of CList and Util interfaces.
ppedrot
2012-09-15
[next]