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
*
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
*
Adding generic solvers to term holes. For now, no resolution mechanism nor
Pierre-Marie Pédrot
2013-11-27
*
Fixing bug #3165.
Pierre-Marie Pédrot
2013-11-23
*
Reverting the old LIFO behaviour of the notation finding algorithm.
ppedrot
2013-11-08
*
Do not generate useless argument arrays in whd_* functions.
ppedrot
2013-10-29
*
More monomorphic List.mem + List.assoc + ...
letouzey
2013-10-24
*
Restore my version of notation_ops.ml now that List.remove_assoc_f is fixed
letouzey
2013-10-24
*
Oups, repair the compilation (micromega + Morphism_prop)
letouzey
2013-10-24
*
Turn many List.assoc into List.assoc_f
letouzey
2013-10-24
*
cList: a few alternative to hashtbl-based uniquize, distinct, subset
letouzey
2013-10-23
*
cList.index is now cList.index_f, same for index0
letouzey
2013-10-23
*
cList: set-as-list functions are now with an explicit comparison
letouzey
2013-10-23
*
Some more hand-written comparison functions to avoid polymorphic comparison.
xclerc
2013-10-14
*
Get rid of the uses of deprecated OCaml elements (still remaining compatible ...
xclerc
2013-09-19
*
At least made the evar type opaque! There are still 5 remaining unsafe
ppedrot
2013-09-18
*
Removing more association lists in Constrintern.
ppedrot
2013-09-02
*
Actually using the domain function for maps.
ppedrot
2013-08-25
*
Nicer code concerning dirpaths and modpath around Lib
letouzey
2013-08-22
*
Misc changes around coqtop.ml :
letouzey
2013-08-22
*
Less "Coq" strings everywhere
letouzey
2013-08-22
*
Declarations.mli: reorganization of modular structures
letouzey
2013-08-20
*
Support Proof General
gareuselesinge
2013-08-08
*
Side effect free implementation of admit (Isabelle's oracle)
gareuselesinge
2013-08-08
*
Removing association lists in Constrintern.
ppedrot
2013-08-07
*
Replacing uses of association lists by maps in notations.
ppedrot
2013-08-03
*
Replacing an association list by a map in globalizing environment.
ppedrot
2013-08-03
*
Declaremods: major refactoring, stop duplicating libobjects in modules
letouzey
2013-07-17
*
More dynamic argument scopes
letouzey
2013-07-17
[next]