index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
interp
Commit message (
Expand
)
Author
Age
*
A tentative uniform naming policy in module Inductiveops.
Hugo Herbelin
2014-08-01
*
Finish fixes on notations and primitive projections, add test-suite files for...
Matthieu Sozeau
2014-07-31
*
Consistent pretty-printing of primitive projections and their expanded forms.
Matthieu Sozeau
2014-07-31
*
Add a type of untyped term to Ltac's value.
Arnaud Spiwack
2014-07-29
*
Fix treatment of notations containing applications of projections (fixes bug ...
Matthieu Sozeau
2014-07-29
*
smartlocate: look for the head symbol for real
Enrico Tassi
2014-07-14
*
Export type_of_global_ref (useful for external users of glob files)
Enrico Tassi
2014-07-11
*
Arith: full integration of the "Numbers" modular framework
Pierre Letouzey
2014-07-09
*
all coqide specific files moved into ide/
Enrico Tassi
2014-06-25
*
Continue fix on argument scopes of primitive projections.
Matthieu Sozeau
2014-06-17
*
Fix HoTT bug #84, binding scopes to projections.
Matthieu Sozeau
2014-06-17
*
Fixing #3292 (locations of notations shifted by 1 in glob files in trunk).
Hugo Herbelin
2014-06-17
*
Fixing #3282 (two bugs in the presence of let-in's in "fix").
Hugo Herbelin
2014-06-17
*
Removing dead code.
Pierre-Marie Pédrot
2014-06-17
*
Fix bug #3289
Matthieu Sozeau
2014-06-11
*
Collecting in Namegen those conventional default names that are used in diffe...
Hugo Herbelin
2014-06-04
*
- Fix hashing of levels to get the "right" order in universe contexts etc...
Matthieu Sozeau
2014-06-04
*
Removing useless use of metaids in tactic AST.
Pierre-Marie Pédrot
2014-05-22
*
- Fix bug preventing apply from unfolding Fixpoints.
Matthieu Sozeau
2014-05-06
*
Fix printing of projections with implicits.
Matthieu Sozeau
2014-05-06
*
Fix inversion of notations for projections.
Matthieu Sozeau
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Removing dead code, thanks to new OCaml warnings and a bit of scripting.
Pierre-Marie Pédrot
2014-04-23
*
Closing bug #3260
Julien Forest
2014-04-14
*
Have the feedback bus as a backend for dumping globs.
Carst Tankink
2014-04-10
*
Dumpglob: factor out reference dumping.
Carst Tankink
2014-04-10
*
Better error message when found more than once object of name ...
Pierre Boutillier
2014-04-02
*
Fixing interpretation of tactics in terms. It was forgetting part of the
Pierre-Marie Pédrot
2014-03-06
*
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
*
Fixing generic hashes and replacing them with proper ones.
Pierre-Marie Pédrot
2014-03-03
*
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 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
*
Useless check when loading notations through import.
Pierre-Marie Pédrot
2014-03-01
*
Fix grammatical mistake in error message (bug #3238)
xclerc
2014-02-24
*
Adding a default object to generic argument registering mechanism.
Pierre-Marie Pédrot
2014-01-19
*
Fixing an interpretation bug with tactics in notations. For some obscure
Pierre-Marie Pédrot
2014-01-19
*
Disable GlobRef feedback (CoqIDE does nothing with them)
Enrico Tassi
2014-01-05
*
Notation variables are now taken into account as possible ltac bound variables
Pierre-Marie Pédrot
2013-12-22
*
Notations now accept the $(...)$ tactic-in-term syntax. They are resolved at
Pierre-Marie Pédrot
2013-12-22
*
Notations can now accept dummy arguments. If ever a bound variable is not
Pierre-Marie Pédrot
2013-12-22
*
Removing the useless pattern ident genarg.
Pierre-Marie Pédrot
2013-12-19
*
Removing the need of evarmaps in constr internalization.
Pierre-Marie Pédrot
2013-12-17
*
Removing RefArgType generic argument.
Pierre-Marie Pédrot
2013-12-01
*
Getting rid of casted_open_constr. It was only used by the
Pierre-Marie Pédrot
2013-11-30
*
Adding the necessary hooks to handle tactics in terms.
Pierre-Marie Pédrot
2013-11-27
[next]