index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
...
*
Reorder search path order, so the standard library is search last.
herbelin
2011-04-14
*
Extraction: opaque terms are not traversed anymore by default
letouzey
2011-04-13
*
Revert "Add [Polymorphic] flag for defs"
msozeau
2011-04-13
*
Put dependent subgoals first so as to allow backtracking on them, might chang...
msozeau
2011-04-13
*
- Make typeclass transparency information directly available
msozeau
2011-04-13
*
- Remove create_evar_defs
msozeau
2011-04-13
*
Fix merge.
msozeau
2011-04-13
*
- Improve unification (beta-reduction, and same heuristic as evarconv for red...
msozeau
2011-04-13
*
Fix scripts relying on unification not doing any beta reduction.
msozeau
2011-04-13
*
Unify meta types with the right flags, add betaiotazeta reduction to unificat...
msozeau
2011-04-13
*
Proper typing of metavariables, type errors were completely ignored before......
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
*
remove old traces of SearchIsos (never ported to 7.x nor 8.x)
letouzey
2011-04-12
*
Catch NotArity exception and transform it into an anomaly in retyping.
msozeau
2011-04-11
*
ocamlbuild: support again camlp5 in addition to camlp4
letouzey
2011-04-08
*
Applying Tom Prince's patch to coqdep not correctly applying the -R visibility
herbelin
2011-04-08
*
A kind of reply to bug 2444
pboutill
2011-04-08
*
weak dependency of coqtop for coqide and coqc (bug 2390)
pboutill
2011-04-08
*
A module out of Program to have list notations (bug 2463)
pboutill
2011-04-08
*
@ in index of refman (last request of bug 2494)
pboutill
2011-04-08
*
Add "make full-stdlib" to make all the doc in pdf as ask by bug 2395
pboutill
2011-04-08
*
More up to date About in coqide
pboutill
2011-04-08
*
Macos integration step2 : shutdown
pboutill
2011-04-08
*
coqide shutdown process change (and out the main function)
pboutill
2011-04-08
*
Applying Tom Prince's patch for build_constant_by_tactic not able to
herbelin
2011-04-08
*
Made warning about ending comments in string less intrusive so as to support
herbelin
2011-04-08
*
Applying and reworking Tom Prince's patch for test-suite/failure/universes2.v
herbelin
2011-04-08
*
Replaced printing number of ill-typed branch by printing name of constructor
herbelin
2011-04-08
*
Fixed "Eval ... in t" when t has still metavariables.
herbelin
2011-04-08
*
Fixing multiple printing bugs with "Notation f x := ..."
herbelin
2011-04-08
*
Extraction: unfolds the let-in created by Program when handling "match"
letouzey
2011-04-07
*
Extraction: avoid some useless Obj.magic by fixing my ML type unifier
letouzey
2011-04-07
*
Fixing bug #2475 (ability to use binders in the syntax of fields was not in doc)
herbelin
2011-04-06
*
A few extra combinators about rel_declaration/named_declaration + a bit of doc
herbelin
2011-04-06
*
Fix dev/base_include after change of constant_body
letouzey
2011-04-06
*
Fixes the weird bug of the declarative proof mode (Czar) both in emacs and coqc.
aspiwack
2011-04-06
*
Add 'Existing Instances' declaration to declare multiple instances at once.
letouzey
2011-04-06
*
Update documentation concerning proofs loading (cf last commit)
letouzey
2011-04-03
*
Fix last commit about coqdep: not everyone has a user-contrib dir
letouzey
2011-04-03
*
Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks
letouzey
2011-04-03
*
Quickly avoid global axioms in Loic new files about ring
letouzey
2011-04-03
*
Adjust coqdep so that it behaves like coqtop with respect to the user-contrib...
gmelquio
2011-04-01
*
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
*
Did that adding a rule for printing applications as "f(x)" works.
herbelin
2011-03-31
*
As remarked by Enrico, we'd better use eq_constr than structural equality
herbelin
2011-03-31
*
Extraction: customized inductives are always standard
glondu
2011-03-31
*
Cyclic: a small optimisation with nice effect on BigN.mul (thinks Benjamin)
letouzey
2011-03-30
[prev]
[next]