index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
termops.ml
Commit message (
Expand
)
Author
Age
*
avoid (Int.equal (cmp ...) 0) when a boolean equality exists
letouzey
2013-02-19
*
Dir_path --> DirPath
letouzey
2013-02-19
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Array.create is deprecated
pboutill
2012-12-19
*
Modulification of name
ppedrot
2012-12-18
*
Modulification of dir_path
ppedrot
2012-12-14
*
Modulification of identifier
ppedrot
2012-12-14
*
Moved Intset and Intmap to Int namespace.
ppedrot
2012-12-14
*
Removed some FIXME related to equality on universes.
ppedrot
2012-11-26
*
Small cleaning of interface in Univ
ppedrot
2012-11-26
*
Monomorphization (pretyping)
ppedrot
2012-11-22
*
Added a CString module.
ppedrot
2012-11-13
*
Monomorphized a lot of equalities over OCaml integers, thanks to
ppedrot
2012-11-08
*
More cleaning in CArray...
ppedrot
2012-09-18
*
More cleaning on Utils and CList. Some parts of the code being
ppedrot
2012-09-17
*
As r15801: putting everything from Util.array_* to CArray.*.
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
*
locus.mli for occurrences+clauses, misctypes.mli for various little things
letouzey
2012-05-29
*
Noise for nothing
pboutill
2012-03-02
*
Reorganizing Unification.unify_0 so as to more easily share code
herbelin
2011-12-17
*
Backtrack on synchronizing universe counter with reset
herbelin
2011-12-06
*
Registering universe and meta/evar counters as summaries so as to
herbelin
2011-12-05
*
Fixed a small regression in pattern-matching compilation introduced in
herbelin
2011-12-04
*
Fixing buggy abberant code for Evarutil.expand_evar
herbelin
2011-10-10
*
Added support for referring to subterms of the goal by pattern.
herbelin
2011-09-26
*
Generalizing subst_term_occ so that it supports an arbitrary matching
herbelin
2011-09-26
*
Adding subst_term up to conv
herbelin
2011-09-26
*
Added full pattern-unification on Meta for tactic unification.
herbelin
2011-06-13
*
Tentative to make unification check types at every instanciation of an
msozeau
2011-03-11
*
An experimental support for open constrs in hints and in "using"
herbelin
2010-10-31
*
Remove "init" label from Termops.it_mk* specialized functions
glondu
2010-09-28
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).
herbelin
2010-06-22
*
Added rudimentary support for using constructors from the explicit
herbelin
2010-06-12
*
Fix bug 2307
pboutill
2010-05-20
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Continuing r12485-12486 and r12549 (cleaning around name generation)
herbelin
2009-12-02
*
Continuing r12485-12486 (cleaning around name generation)
herbelin
2009-12-01
*
Added support for definition of fixpoints using tactics.
herbelin
2009-11-27
*
A bit of cleaning around name generation + creation of dedicated file namegen.ml
herbelin
2009-11-09
*
This big commit addresses two problems:
soubiran
2009-10-21
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Ensures that let-in's in arities of inductive types work well. Maybe not
herbelin
2009-08-11
*
- Cleaning phase of the interfaces of libnames.ml and nametab.ml
herbelin
2009-08-06
*
- Fixing bug #2084 (unification not checking sort constraints), hoping
herbelin
2009-04-08
*
- Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixing
herbelin
2009-04-08
[next]