index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
Commit message (
Expand
)
Author
Age
*
Error during last commit (coq didn't compile)
jforest
2006-05-23
*
Correcting a bug with ocaml <= 3.08.3 (Map.fold changing)
jforest
2006-05-23
*
Clarification role de library_part : renommage en remove_section_part
herbelin
2006-05-23
*
cleanning code
jforest
2006-05-23
*
Nouvelle implantation du polymorphisme de sorte pour les familles inductives
herbelin
2006-05-23
*
Correcting a bug in identifiers manipulation
jforest
2006-05-22
*
LetTuple are now supported in Function
jforest
2006-05-22
*
Correcting an old bug during generation of generale recursive functions.
jforest
2006-05-09
*
+ correcting a bug in general recursive function (match e with _ => match f e...
jforest
2006-05-07
*
Correction in generate_graph (now handles fun _ => fix ....)
jforest
2006-05-05
*
Fixing two minor bugs in recdef and graph of function generation.
jforest
2006-05-03
*
Cleanning and factorizing code in funind. Spliting new_arg_principles into to...
jforest
2006-05-03
*
Extension syntaxique de rewrite in: au lieu de pouvoir faire
letouzey
2006-05-02
*
If function creates proof obligation, there are now printed once.
courtieu
2006-04-28
*
Standardisation du nom des méthodes de Evd
herbelin
2006-04-28
*
Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...
notin
2006-04-28
*
- Distinction explicite des parties paramètres et arguments dans le type
herbelin
2006-04-27
*
Message d'erreur plus informatif
herbelin
2006-04-27
*
Standardisation nom option_app en option_map
herbelin
2006-04-27
*
Replacing "GenFixpoint" with "Function" and "mes" with "measure"
jforest
2006-04-26
*
+ Handling "if" and cast in GenFixpoint
jforest
2006-04-24
*
decoration des Tdummy pour pouvoir tuer tous les args de types (cf MapAVL.empty)
letouzey
2006-04-20
*
Added code to support "Program Lemma/Example... etc"
msozeau
2006-04-16
*
Si un fixpoint a plusieurs arguments, mais un seul de type inductif,
letouzey
2006-04-14
*
Test files for subtac.
msozeau
2006-04-14
*
Simplifying the proof of principles
jforest
2006-04-12
*
Fixes for new unification, not used in default version as it really changes u...
msozeau
2006-04-10
*
+ Changing a little functional schemes types
jforest
2006-04-10
*
Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous...
msozeau
2006-04-10
*
- Documentation of the Program tactics.
msozeau
2006-04-07
*
appel Zenon sans prelude
filliatr
2006-03-27
*
utilisation de la VM pour la normalisation finale de romega
letouzey
2006-03-24
*
correctifs de bug pour romega:
letouzey
2006-03-23
*
Subtac fixes, single fixpoint definitions are working again. Added a toggle o...
msozeau
2006-03-22
*
Made pretyping a functor over a coercion implementation. Pretyping.Default us...
msozeau
2006-03-22
*
+ destruct now works as induction on multiple arguments :
jforest
2006-03-21
*
Adding "New Functional Scheme"
jforest
2006-03-20
*
Modification des propriétés (svn:executable)
notin
2006-03-17
*
Cleaning dead code
jforest
2006-03-16
*
+ Debugging and cleaning functional principle generation tactic
jforest
2006-03-14
*
Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.
msozeau
2006-03-13
*
-Debugging multiple induction, a bug appeared when having function
courtieu
2006-03-12
*
cleaning
jforest
2006-03-10
*
Coq did not compile in Ocaml 3.06 and 3.07 since Map.S did not contain is_emp...
jforest
2006-03-07
*
Exploitation du 'let rec' + présentation
herbelin
2006-03-05
*
New files for subtac
coq
2006-03-05
*
tactic haRVey pour appeler haRVey (contrib/dp)
filliatr
2006-03-02
*
Correction bug #842 (rename d'une hyp du contexte)
herbelin
2006-03-01
*
appel de Zenon
filliatr
2006-03-01
*
*** empty log message ***
filliatr
2006-02-28
[next]