index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2014-03-07
Fixing generic equality in Auto.
Pierre-Marie Pédrot
2014-03-06
Inductive maps in Environ now use HMap.
Pierre-Marie Pédrot
2014-03-06
make install-coqlight installs DLLCOQRUN and LIBCOQRUN
Pierre Boutillier
2014-03-06
Lets coqtop use a slash
Virgile Prevosto
2014-03-06
Uses slashes for install and config directories
Virgile Prevosto
2014-03-06
remove trailing '\r' from file names returned by coqtop
Virgile Prevosto
2014-03-05
Fix typo in comment.
Maxime Dénès
2014-03-06
Fixing interpretation of tactics in terms. It was forgetting part of the
Pierre-Marie Pédrot
2014-03-05
Using HMaps in Safe_env.environments, hopefully improving performances.
Pierre-Marie Pédrot
2014-03-05
Canary testing absence of generic equality for KerNames
Pierre-Marie Pédrot
2014-03-05
Lazily computed hash in KerName.t.
Pierre-Marie Pédrot
2014-03-05
Adding a canary library. This canary is imperfect. It allows serialization
Pierre-Marie Pédrot
2014-03-05
Fixing compilation on OCaml 4.01.
Pierre-Marie Pédrot
2014-03-05
Fixing previous commit. Forgot to include some code.
Pierre-Marie Pédrot
2014-03-05
Added a new module HMap. It works (almost) like Map, except that it expects
Pierre-Marie Pédrot
2014-03-05
Remove some dead-code (thanks to ocaml warnings)
Pierre Letouzey
2014-03-05
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
Correct handling of hashconsing of constraint sets. The previous implementation
Pierre-Marie Pédrot
2014-03-05
Adding a CSet module in Coq lib.
Pierre-Marie Pédrot
2014-03-04
Fixing pervasives equalities in Vconv.
Pierre-Marie Pédrot
2014-03-04
Move error and job display to the lower right pane.
Guillaume Melquiond
2014-03-04
STM: fix Show Script
Enrico Tassi
2014-03-04
STM: when finish a task hcons universe constraints
Enrico Tassi
2014-03-03
Fixing some generic equalities in Micromega.
Pierre-Marie Pédrot
2014-03-03
Fixing Pervasives.equality in extraction.
Pierre-Marie Pédrot
2014-03-03
Fixing pervasive equalities. In particular, I removed the code that deleted
Pierre-Marie Pédrot
2014-03-03
Removing generic hashes in kernel.
Pierre-Marie Pédrot
2014-03-03
Getting rid of generic hashes in cc plugin.
Pierre-Marie Pédrot
2014-03-03
Kernel names are implemented using records.
Pierre-Marie Pédrot
2014-03-03
Goptions do not rely anymore on generic equality.
Pierre-Marie Pédrot
2014-03-03
Term dnets do no need to contain the afferent constr pattern in their nodes.
Pierre-Marie Pédrot
2014-03-03
Removing Termdn, and putting the relevant code in Btermdn. The current Termdn
Pierre-Marie Pédrot
2014-03-03
Extruding code not depending of the functor argument in Termdn.
Pierre-Marie Pédrot
2014-03-03
Replacing arguments of Trie by a cancellable monoid.
Pierre-Marie Pédrot
2014-03-03
Fixing generic hashes and replacing them with proper ones.
Pierre-Marie Pédrot
2014-03-02
Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)
Pierre Letouzey
2014-03-02
Set officially the minimal OCaml requirement to 3.12.1
Pierre Letouzey
2014-03-02
Makefile: the initial build of grammar.cma is now directory-driven
Pierre Letouzey
2014-03-02
Migrate back g_obligations in toplevel
Pierre Letouzey
2014-03-02
Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code
Pierre Letouzey
2014-03-02
Removing generic equality in Syntax plugin.
Pierre-Marie Pédrot
2014-03-02
Adding an equality function over glob_constr
Pierre-Marie Pédrot
2014-03-02
Fixing generic Hashtbl.hash in Constr.
Pierre-Marie Pédrot
2014-03-02
Fix syntax highlighting of "Implicit Arguments" for gtksourceview.
Guillaume Melquiond
2014-03-01
Fixing pervasive comparisons
Pierre-Marie Pédrot
2014-03-01
Better behaviour for sets of reserved names.
Pierre-Marie Pédrot
2014-03-01
Never suppress the typing constraint of bound variables whose name was
Pierre-Marie Pédrot
2014-03-01
Fixing bad comparison in Detyping.
Pierre-Marie Pédrot
2014-03-01
Useless check when loading notations through import.
Pierre-Marie Pédrot
2014-03-01
Hunting pervasive equality in native compiler. It seems they were used for
Pierre-Marie Pédrot
[next]