index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
term.ml
Commit message (
Expand
)
Author
Age
...
*
kernel/Term:
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
*
Fixing bug #2817 (occur check was not done up to instantiation of
herbelin
2012-06-20
*
Reorganizing the structure of evarutil.ml (only restructuration, no
herbelin
2012-03-20
*
Noise for nothing
pboutill
2012-03-02
*
Term: properly ignore Casts between Apps in constr_ord
puech
2011-11-29
*
Term: useless conversion to list in constr_ord deleted
puech
2011-11-29
*
Term: Fix hash_constr behavior for Cast lnterleaved in application spines.
puech
2011-11-28
*
Typo
herbelin
2011-11-21
*
More on r14536 (an unused pattern-matching remained in the commit).
herbelin
2011-10-11
*
Hash-cons the statically allocated Rels (1 to 16) to themselves
letouzey
2011-10-10
*
Hash-cons of constr : avoid some useless allocations
letouzey
2011-10-10
*
Hash-consing of constr could share more
letouzey
2011-10-02
*
Polishing commits r14492, r14448 and r14407 (tactics propagate
herbelin
2011-09-25
*
Remove specific hash-consing of Term.types (was unused anyway)
letouzey
2011-09-22
*
Hash-consing: attempt to stop hash-consing separately constr in declare.ml
letouzey
2011-09-22
*
More twicks on hash-consing
letouzey
2011-09-08
*
Having added a special Cast for remembering the use of conversion
herbelin
2011-09-04
*
Propagated information from the reduction tactics to the kernel so
herbelin
2011-08-10
*
Term: fix hash_constr to hash modulo casts & names (like compare_constr)
puech
2011-08-08
*
Esubst: make types of substitutions & lifts private
puech
2011-08-08
*
Term: simplify compare_constr by removing calls to decompose_app
puech
2011-08-01
*
Extraction: replace generic = on mutual_inductive_body by mib_equal
puech
2011-07-29
*
Term: moved function constr_ord (a.k.a compare_constr) from Sequent to Term
puech
2011-07-29
*
Ccalgo, Ccproof: multiple generic Hashtbl on constr and term replaced by Cons...
puech
2011-07-29
*
Hahtbl_alt: separate generic combine functions
puech
2011-07-29
*
Term: added function eq_named_declaration
puech
2011-07-29
*
Term: slight reorganization of the file
puech
2011-07-29
*
Term: Refactoring of hashconsing
puech
2011-07-29
*
argument renaming in liftn (match with usual terminology)
puech
2011-07-29
*
A few extra combinators about rel_declaration/named_declaration + a bit of doc
herbelin
2011-04-06
*
* Kernel/Term:
regisgia
2010-12-01
*
* Kernel/Term
regisgia
2010-12-01
*
* Kernel/Term
regisgia
2010-12-01
*
Remove suspiciously named "implicit" stuff from Term
glondu
2010-11-03
*
Reintroduce kind_of_type (used by Presburger contrib)
glondu
2010-10-05
*
Remove kind_of_type, kind_of_term2 (dead code)
glondu
2010-09-28
*
Partial review of removed dead code (r13460)
herbelin
2010-09-24
*
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 a few informations about file lineages (for the most part in kernel)
herbelin
2010-05-09
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
fixed confusion between number of cstr arguments and number of pattern variab...
barras
2010-03-12
*
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
*
Minor unification changes:
msozeau
2009-05-18
*
Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->
herbelin
2008-12-31
*
Optimisation de clenv.ml pour que meta_instance ne soit pas appelé
herbelin
2008-10-18
[prev]
[next]