aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Expand)Author
2006-08-25two minor bug corrections in General Recursive Functions jforest
2006-08-24Amelioration des messages d'erreur de Fucntion jforest
2006-08-22making otags working jforest
2006-08-22+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and nojforest
2006-08-16+ timide essai pour le traitement des as dans les patterns lors de la generat...jforest
2006-08-15working on functional induction automation (tactic finduction andcourtieu
2006-08-11Bug corrections in Function.jforest
2006-08-08In the old version, recursive functions cannot be declared inside a sectionbertot
2006-07-18Correction bug #1192notin
2006-07-18Code cleaning in Functionjforest
2006-07-18Code cleaning in Functionjforest
2006-07-13bug correction when defining graph of fixpoints/definitions not generated by ...jforest
2006-07-11Ajout de quelques Arguments Scope pour simuler la récursivité du scope rome...herbelin
2006-07-10+functional inversion now takes the function to invert as an optional argument. jforest
2006-07-07Correction bug 1172 + correction en passant de la taille des paramètres de f...herbelin
2006-07-06Suite remplacement VernacDebug par VernacSetOptionherbelin
2006-07-05Use typing informations while defining graphs for Function. jforest
2006-07-04functional inversion now takes a quatified hypothesis as first argumentjforest
2006-07-04adding comments and cleaning code jforest
2006-07-04- completely new version of "functional inversion" using inversion onjforest
2006-07-03Extension des motifs disjonctifs au cas de disjonction de motifs multiplesherbelin
2006-06-29forgot a file jforest
2006-06-29bug correctionjforest
2006-06-23Passage des graphes de Function dans Type jforest
2006-06-23Fix wrong order of existentials in eterm.msozeau
2006-06-23Suite passage ident -> hyp dans syntaxe de 'replace with in'herbelin
2006-06-22Mutually structurally recursive defs and rec using measures added.msozeau
2006-06-20Wellfounded recursion using subtac working again.msozeau
2006-06-20Progress in new wf def typing.msozeau
2006-06-20Rewrite of the recursive defs handling in progress.msozeau
2006-06-16Ajout de tactiques expérimentales basée sur functional induction.courtieu
2006-06-13ajout d'un argument with_clean a Indfun.functional_induction permettant de ch...jforest
2006-06-13rearrangement du code: deplacement du code effectuant functionalcourtieu
2006-06-12changed comments.courtieu
2006-06-09Bug suite déplacement Int.v dans ZArithherbelin
2006-06-09oups: il faut penser a fermer la porte en partant (d'un fixpoint)letouzey
2006-06-09changements de dernieres minutes pour la 8.1 beta: letouzey
2006-06-08Changement du type d'argument 'TacticArgType X' en un typeherbelin
2006-06-08reparation bug 1006letouzey
2006-06-08Détection bug rawwit suitecorrection trou de typage create_argherbelin
2006-06-07Correction trou de subject-reduction de create_arg dans genarg.mliherbelin
2006-06-07functional induction can now be used with jforest
2006-06-06this time it's good jforest
2006-06-06Error in last commit jforest
2006-06-06protecting an uncaught exception Not_found jforest
2006-06-06+ ameliorating the tactic "functional induction"jforest
2006-06-02debut de reparation du test d'extractionletouzey
2006-06-01Fix some nasty bug with the evars-to-dependent sum encoding.msozeau
2006-06-01bug in alpha-conversionjforest
2006-06-01reparation bug #1128letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-18 23:10:44 +0000