index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
Commit message (
Expand
)
Author
Age
*
Rely on kernel to know if a name is already used so as to be consistent with it.
herbelin
2011-10-08
*
Fixing critical inductive polymorphism bug found by Bruno.
herbelin
2011-10-05
*
It happens that the type inference algorithm (pretyping) did not check
herbelin
2011-10-05
*
Hash-consing of constr could share more
letouzey
2011-10-02
*
Polishing commits r14492, r14448 and r14407 (tactics propagate
herbelin
2011-09-25
*
Completing r14448 and thus continuing r14407 (using Cast to propagate
herbelin
2011-09-24
*
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
*
Names.make_mbid and co : convert from/to identifier (avoid some String.copy)
letouzey
2011-09-15
*
More twicks on hash-consing
letouzey
2011-09-08
*
Fix the hconsing of universes
letouzey
2011-09-07
*
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
*
fixed bug 2580. Quick fix: copy emitcodes before patching it
barras
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
*
Environ: generic equality on named_context replaced by named_context_equal
puech
2011-07-29
*
Term: added function eq_named_declaration
puech
2011-07-29
*
Indtypes: remove useless and wrong generic equality test on constr array
puech
2011-07-29
*
Term: slight reorganization of the file
puech
2011-07-29
*
Term_typing, Typeops: replace some generic '=' on constr by eq_constr
puech
2011-07-29
*
Term: Refactoring of hashconsing
puech
2011-07-29
*
argument renaming in liftn (match with usual terminology)
puech
2011-07-29
*
Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml
letouzey
2011-07-04
*
Modops: the strengthening functions can work without any env argument
letouzey
2011-05-17
*
Print Module (Type) M now tries to print more details
letouzey
2011-05-11
*
Fix thumb2-related build error
glondu
2011-04-19
*
Revert "Add [Polymorphic] flag for defs"
msozeau
2011-04-13
*
- Remove create_evar_defs
msozeau
2011-04-13
*
Fix merge.
msozeau
2011-04-13
*
- Do not make constants with an assigned type polymorphic (wrong unfoldings).
msozeau
2011-04-13
*
Add [Polymorphic] flag for defs
msozeau
2011-04-13
*
Subtyping: align coqtop behavior concerning opaque csts on coqchk's one
letouzey
2011-04-12
*
Replaced printing number of ill-typed branch by printing name of constructor
herbelin
2011-04-08
*
A few extra combinators about rel_declaration/named_declaration + a bit of doc
herbelin
2011-04-06
*
Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks
letouzey
2011-04-03
*
CHANGES: a word about recent changes in coqide, about Ctrl-C in vm
letouzey
2011-04-01
*
Checks for signals in VM, allowing it to be interrupted by Ctrl-C (experimental)
letouzey
2011-04-01
*
Tentative to make unification check types at every instanciation of an
msozeau
2011-03-11
*
adding eta in the vm
bgregoir
2011-03-08
*
Moving printing of module typing errors upwards to himsg.ml so as to
herbelin
2011-03-05
*
Starting being more explicit on the reasons why module subtyping fails.
herbelin
2011-03-05
*
Fixed a "feature" about subtyping records: one was expected not only
herbelin
2011-03-05
*
Mod_subst: improving sharing of subst_mps
letouzey
2011-02-24
*
Some more simplification in Mod_subst
letouzey
2011-02-23
[next]