index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
/
funind
Commit message (
Expand
)
Author
Age
*
Ajout de eelim, ecase, edestruct et einduction (expérimental).
herbelin
2007-10-03
*
* Adding compability with ocaml 3.10 + camlp5 (rework of
letouzey
2007-09-15
*
correction bug d'efficacite dans Function
jforest
2007-08-31
*
Slight cleanup of refl_omega.ml : in particular it uses now list
letouzey
2007-07-11
*
extension of the rename tactic: the following is now allowed:
letouzey
2007-07-06
*
- Propagation des evars non résolues vers les with_bindings; permet par exemple
herbelin
2007-05-20
*
correction de bug dans Function et augmentation de la classe des fonctions su...
jforest
2007-05-17
*
Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.
herbelin
2007-04-28
*
Mise en place d'une nouvelle strategie plus efficace pour les preuves de Func...
jforest
2007-04-05
*
Add a parameter to QuestionMark evar kind to say it can be turned into an obl...
msozeau
2007-03-19
*
r11153@tannat: jforest | 2007-03-16 10:25:55 +0100
jforest
2007-03-16
*
Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de
herbelin
2007-02-13
*
Bug mineur dans la generation des principes d'induction pour Function
jforest
2007-02-12
*
Correction d'un bug dans la génération des principes d'induction
jforest
2007-02-11
*
Retour r9310 en attendant mieux
herbelin
2007-02-09
*
Meilleur anglais (cf 9619)
herbelin
2007-02-07
*
Contounement d'un probleme avec la VM dans Function
jforest
2007-01-26
*
Protection contre les warnings 'unused variable' de ocaml 3.09
herbelin
2007-01-19
*
Functional graph merging deals with letins.
courtieu
2006-11-24
*
Fixed the graph merging parameter order.
courtieu
2006-11-24
*
Fixing syntax and parameter order in functional graph merging.
courtieu
2006-11-23
*
Changing merging functional scheme syntax.
courtieu
2006-11-20
*
Small fix in functional graph merging.
courtieu
2006-11-16
*
Correction de la seconde partie du bug #1278
jforest
2006-11-13
*
Correction de la premiere partie du #1278 (but non referme en cas d'echec)
jforest
2006-11-13
*
Extension du polymorphisme de sorte au cas des définitions dans Type.
herbelin
2006-10-28
*
Fixes in experimental merging of functional graphs.
courtieu
2006-10-28
*
Fixes on functional graphs merging: put functional results at the end
courtieu
2006-10-27
*
Fixes on functional graphs merging: removed debug printing.
courtieu
2006-10-27
*
Fixes on functional graphs merging: names of constructors.
courtieu
2006-10-27
*
Some fixes in experimental merging of two functional graphs.
courtieu
2006-10-26
*
Experimental merging of two functional graphs.
courtieu
2006-10-26
*
Starting to add a function schemes merging command (not finished, not
courtieu
2006-10-20
*
r9778@tannat: jforest | 2006-10-13 11:36:37 +0200
jforest
2006-10-13
*
Detection des paramettres pour les Functions bien fondees
jforest
2006-09-27
*
Declarative Proof Language: main commit
corbinea
2006-09-20
*
Gestion des arguments implicites dans les Functions bien fondees
jforest
2006-09-19
*
correction of bug #1220
jforest
2006-09-18
*
Message modification in Function
jforest
2006-09-16
*
mise en conformite des messages d'erreur de Function avec la doc.
jforest
2006-09-14
*
Ajout possibilité clause "where" dans co-points fixes
herbelin
2006-09-01
*
two minor bug corrections in General Recursive Functions
jforest
2006-08-25
*
Amelioration des messages d'erreur de Fucntion
jforest
2006-08-24
*
+ timide essai pour le traitement des as dans les patterns lors de la generat...
jforest
2006-08-16
*
working on functional induction automation (tactic finduction and
courtieu
2006-08-15
*
Bug corrections in Function.
jforest
2006-08-11
*
In the old version, recursive functions cannot be declared inside a section
bertot
2006-08-08
*
Code cleaning in Function
jforest
2006-07-18
*
Code cleaning in Function
jforest
2006-07-18
*
bug correction when defining graph of fixpoints/definitions not generated by ...
jforest
2006-07-13
[next]