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
*
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
*
+functional inversion now takes the function to invert as an optional argument.
jforest
2006-07-10
*
Use typing informations while defining graphs for Function.
jforest
2006-07-05
*
functional inversion now takes a quatified hypothesis as first argument
jforest
2006-07-04
*
adding comments and cleaning code
jforest
2006-07-04
*
- completely new version of "functional inversion" using inversion on
jforest
2006-07-04
*
forgot a file
jforest
2006-06-29
*
bug correction
jforest
2006-06-29
*
Passage des graphes de Function dans Type
jforest
2006-06-23
*
Ajout de tactiques expérimentales basée sur functional induction.
courtieu
2006-06-16
*
ajout d'un argument with_clean a Indfun.functional_induction permettant de ch...
jforest
2006-06-13
*
rearrangement du code: deplacement du code effectuant functional
courtieu
2006-06-13
*
changed comments.
courtieu
2006-06-12
*
functional induction can now be used with
jforest
2006-06-07
*
this time it's good
jforest
2006-06-06
*
Error in last commit
jforest
2006-06-06
*
protecting an uncaught exception Not_found
jforest
2006-06-06
*
+ ameliorating the tactic "functional induction"
jforest
2006-06-06
*
bug in alpha-conversion
jforest
2006-06-01
*
Replacing the old version of "functional induction" with the new one.
jforest
2006-05-31
*
Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...
herbelin
2006-05-30
*
small changes
jforest
2006-05-29
*
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
*
LetTuple are now supported in Function
jforest
2006-05-22
*
+ 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
*
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
*
Standardisation nom option_app en option_map
herbelin
2006-04-27
*
Replacing "GenFixpoint" with "Function" and "mes" with "measure"
jforest
2006-04-26
[next]