index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
Commit message (
Expand
)
Author
Age
*
Extraction : fix Extract Inlined Constant for Haskell and Scheme (#2469)
letouzey
2011-01-07
*
ARGUMENT EXTEND: forbid TYPED simultaneously with {RAW,GLOB}_TYPED
glondu
2010-12-25
*
Rename mkR* smart constructors (mostly in funind)
glondu
2010-12-25
*
s/raw/glob/g in decl_interp.ml for more consistency
glondu
2010-12-24
*
More {raw => glob} changes for consistency
glondu
2010-12-24
*
Rename files in funind to respect new conventions
glondu
2010-12-24
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-23
*
Prepare change of nomenclature rawconstr -> glob_constr
glondu
2010-12-23
*
Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)
letouzey
2010-12-21
*
Remove an unused function with a Evd.fold in subtac
letouzey
2010-12-13
*
Dp: minor fix suggested by Virgile Prevosto
letouzey
2010-11-25
*
Some more revision of {P,N,Z}Arith + bitwise ops in Ndigits
letouzey
2010-11-18
*
Use full path for unknown stuff in omega
glondu
2010-11-16
*
Integer division: quot and rem (trunc convention) in addition to div and mod
letouzey
2010-11-10
*
Delayed the evar normalization in error messages to the last minute
herbelin
2010-11-07
*
Add information of localisation when an error involving an "implicit
herbelin
2010-11-07
*
Move stuff about positive into a distinct PArith subdir
letouzey
2010-11-02
*
An experimental support for open constrs in hints and in "using"
herbelin
2010-10-31
*
Cleaning the use of parentheses around evd and evdref (cosmetic commit).
herbelin
2010-10-31
*
Solve name conflict about pow introduced by commit 13546.
letouzey
2010-10-21
*
Still some more Cpow in Type rather than Set (cf. r13542)
letouzey
2010-10-21
*
Reparation du parseur/printer de nombres BigN
letouzey
2010-10-14
*
Ring : Cpow in Type rather than Set (type of power coeffs in power_theory)
letouzey
2010-10-14
*
Fix bug #2393: allow let-ins inside telescopes (only fails when there's
msozeau
2010-10-12
*
Fix bug# 2392
msozeau
2010-10-07
*
Extraction: allow to use Extraction Inline / NoInline even from under a section.
letouzey
2010-10-06
*
Remove unused unshare_proof_tree from xml plugin
glondu
2010-10-06
*
Remove open_subgoals field of proof_tree
glondu
2010-10-06
*
Auto-inlining of f_terminate in Function
jforest
2010-10-05
*
Added multiple implicit arguments rules per name.
herbelin
2010-10-03
*
Simplify tactic(_)-bound arguments in TACTIC EXTEND rules
glondu
2010-09-30
*
Fix bug #2321, allowing "_" named projections in classes. Not realizing
msozeau
2010-09-28
*
Remove some occurrences of "open Termops"
glondu
2010-09-28
*
Remove "init" label from Termops.it_mk* specialized functions
glondu
2010-09-28
*
Dead code in extraction
letouzey
2010-09-24
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
Report fix bug 2345 from v8.3 (Bad error message when functional
courtieu
2010-09-21
*
Added eta-expansion in kernel, type inference and tactic unification,
herbelin
2010-09-20
*
Extraction: re-introduce some eta-expansions in rare situations leading to '_...
letouzey
2010-09-20
*
Reverting partial fix for #2335 committed by mistake in r13435. Sorry.
herbelin
2010-09-19
*
Patch solving the bug but leaving open design choices
herbelin
2010-09-19
*
Extraction: multiple fixes related with the Not_found encountered by X. Leroy
letouzey
2010-09-17
*
Fix likely semantic typos
glondu
2010-09-15
*
Fix unescaped end-of-lines (OCaml warning 29)
glondu
2010-09-13
*
commit 13400 and 13409.
soubiran
2010-09-13
*
fixed bug #2375 (congruence)
corbinea
2010-09-02
*
Fix [clenv_missing] to compute a better approximation of missing
msozeau
2010-08-02
*
unification des tactiques nsatz pour R Z avec celle des anneaux integres
pottier
2010-07-28
*
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13338 85f007b7-540e-0...
pottier
2010-07-28
[next]