| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2006-03-21 | + destruct now works as induction on multiple arguments : | jforest |
| 2006-03-20 | Adding "New Functional Scheme" | jforest |
| 2006-03-17 | Modification des propriétés (svn:executable) | notin |
| 2006-03-16 | Cleaning dead code | jforest |
| 2006-03-14 | + Debugging and cleaning functional principle generation tactic | jforest |
| 2006-03-13 | Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}. | msozeau |
| 2006-03-12 | -Debugging multiple induction, a bug appeared when having function | courtieu |
| 2006-03-10 | cleaning | jforest |
| 2006-03-07 | Coq did not compile in Ocaml 3.06 and 3.07 since Map.S did not contain is_emp... | jforest |
| 2006-03-05 | Exploitation du 'let rec' + présentation | herbelin |
| 2006-03-05 | New files for subtac | coq |
| 2006-03-02 | tactic haRVey pour appeler haRVey (contrib/dp) | filliatr |
| 2006-03-01 | Correction bug #842 (rename d'une hyp du contexte) | herbelin |
| 2006-03-01 | appel de Zenon | filliatr |
| 2006-02-28 | *** empty log message *** | filliatr |
| 2006-02-27 | dp: sortie Why | filliatr |
| 2006-02-22 | Work on recursive definitions | coq |
| 2006-02-22 | Add vernacular file for subtac | coq |
| 2006-02-22 | Julien: | bertot |
| 2006-02-21 | Work with binder lists, problem of tycons | coq |
| 2006-02-21 | Latest fixes, should work fine now for non recursive definitions, although st... | coq |
| 2006-02-20 | Fix minor bug | coq |
| 2006-02-20 | Forgot a file | coq |
| 2006-02-20 | Monday work, working with coercions and implicit args | coq |
| 2006-02-20 | Forgot another file... | coq |
| 2006-02-20 | Forgot one file | coq |
| 2006-02-20 | Rewrite of the subtac tactic, needs some work on implicit arguments. | coq |
| 2006-02-17 | bug correction | bertot |
| 2006-02-17 | Julien: | bertot |
| 2006-02-17 | changed the decomposition of an induction scheme | coq |
