| Age | Commit message (Expand) | Author |
|---|
| 2006-06-07 | functional induction can now be used with | jforest |
| 2006-06-06 | 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-02 | debut de reparation du test d'extraction | letouzey |
| 2006-06-01 | Fix some nasty bug with the evars-to-dependent sum encoding. | msozeau |
| 2006-06-01 | bug in alpha-conversion | jforest |
| 2006-06-01 | reparation bug #1128 | letouzey |
| 2006-05-31 | Replacing the old version of "functional induction" with the new one. | jforest |
| 2006-05-30 | Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme... | herbelin |
| 2006-05-29 | The "clean integration of subtac" patch. | msozeau |
| 2006-05-29 | small changes | jforest |
| 2006-05-28 | - Déplacement des types paramétriques prod, sum, option, identity, | herbelin |
| 2006-05-26 | removing a warning | jforest |
| 2006-05-23 | 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 | Clarification role de library_part : renommage en remove_section_part | herbelin |
| 2006-05-23 | cleanning code | jforest |
| 2006-05-23 | Nouvelle implantation du polymorphisme de sorte pour les familles inductives | herbelin |
| 2006-05-22 | Correcting a bug in identifiers manipulation | jforest |
| 2006-05-22 | LetTuple are now supported in Function | jforest |
| 2006-05-09 | Correcting 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-05 | Correction in generate_graph (now handles fun _ => fix ....) | jforest |
| 2006-05-03 | 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-02 | Extension syntaxique de rewrite in: au lieu de pouvoir faire | letouzey |
| 2006-04-28 | If function creates proof obligation, there are now printed once. | courtieu |
| 2006-04-28 | Standardisation du nom des méthodes de Evd | herbelin |
| 2006-04-28 | Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '... | notin |
| 2006-04-27 | - Distinction explicite des parties paramètres et arguments dans le type | herbelin |
| 2006-04-27 | Message d'erreur plus informatif | herbelin |
| 2006-04-27 | Standardisation nom option_app en option_map | herbelin |
| 2006-04-26 | Replacing "GenFixpoint" with "Function" and "mes" with "measure" | jforest |
| 2006-04-24 | + Handling "if" and cast in GenFixpoint | jforest |
| 2006-04-20 | decoration des Tdummy pour pouvoir tuer tous les args de types (cf MapAVL.empty) | letouzey |
| 2006-04-16 | Added code to support "Program Lemma/Example... etc" | msozeau |
| 2006-04-14 | Si un fixpoint a plusieurs arguments, mais un seul de type inductif, | letouzey |
| 2006-04-14 | Test files for subtac. | msozeau |
| 2006-04-12 | Simplifying the proof of principles | jforest |
| 2006-04-10 | Fixes for new unification, not used in default version as it really changes u... | msozeau |
| 2006-04-10 | + Changing a little functional schemes types | jforest |
| 2006-04-10 | Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous... | msozeau |
| 2006-04-07 | - Documentation of the Program tactics. | msozeau |
| 2006-03-27 | appel Zenon sans prelude | filliatr |
| 2006-03-24 | utilisation de la VM pour la normalisation finale de romega | letouzey |
| 2006-03-23 | correctifs de bug pour romega: | letouzey |
| 2006-03-22 | Subtac fixes, single fixpoint definitions are working again. Added a toggle o... | msozeau |
| 2006-03-22 | Made pretyping a functor over a coercion implementation. Pretyping.Default us... | msozeau |
