aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Expand)Author
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
2006-05-23Clarification role de library_part : renommage en remove_section_partherbelin
2006-05-23cleanning code jforest
2006-05-23Nouvelle implantation du polymorphisme de sorte pour les familles inductivesherbelin
2006-05-22Correcting a bug in identifiers manipulation jforest
2006-05-22LetTuple are now supported in Functionjforest
2006-05-09Correcting an old bug during generation of generale recursive functions.jforest
2006-05-07+ correcting a bug in general recursive function (match e with _ => match f e...jforest
2006-05-05Correction in generate_graph (now handles fun _ => fix ....)jforest
2006-05-03Fixing two minor bugs in recdef and graph of function generation. jforest
2006-05-03Cleanning and factorizing code in funind. Spliting new_arg_principles into to...jforest
2006-05-02Extension syntaxique de rewrite in: au lieu de pouvoir faire letouzey
2006-04-28If function creates proof obligation, there are now printed once.courtieu
2006-04-28Standardisation du nom des méthodes de Evdherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 19:12:38 +0000