aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Expand)Author
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
2006-05-31Replacing the old version of "functional induction" with the new one. jforest
2006-05-30Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...herbelin
2006-05-29The "clean integration of subtac" patch.msozeau
2006-05-29small changes jforest
2006-05-28- Déplacement des types paramétriques prod, sum, option, identity,herbelin
2006-05-26removing a warningjforest
2006-05-23Error during last commit (coq didn't compile)jforest
2006-05-23Correcting a bug with ocaml <= 3.08.3 (Map.fold changing)jforest
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-30 14:19:48 +0000