| Commit message (Expand) | Author | Age |
* | 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-28 |
* | - 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-27 |
* | Replacing "GenFixpoint" with "Function" and "mes" with "measure" | jforest | 2006-04-26 |
* | + Handling "if" and cast in GenFixpoint | jforest | 2006-04-24 |
* | decoration des Tdummy pour pouvoir tuer tous les args de types (cf MapAVL.empty) | letouzey | 2006-04-20 |
* | Added code to support "Program Lemma/Example... etc" | msozeau | 2006-04-16 |
* | Si un fixpoint a plusieurs arguments, mais un seul de type inductif, | letouzey | 2006-04-14 |
* | Test files for subtac. | msozeau | 2006-04-14 |
* | Simplifying the proof of principles | jforest | 2006-04-12 |
* | 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-10 |
* | - Documentation of the Program tactics. | msozeau | 2006-04-07 |
* | appel Zenon sans prelude | filliatr | 2006-03-27 |
* | utilisation de la VM pour la normalisation finale de romega | letouzey | 2006-03-24 |
* | correctifs de bug pour romega: | letouzey | 2006-03-23 |
* | 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-22 |
* | + destruct now works as induction on multiple arguments : | jforest | 2006-03-21 |
* | Adding "New Functional Scheme" | jforest | 2006-03-20 |
* | Modification des propriétés (svn:executable) | notin | 2006-03-17 |
* | Cleaning dead code | jforest | 2006-03-16 |
* | + Debugging and cleaning functional principle generation tactic | jforest | 2006-03-14 |
* | Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}. | msozeau | 2006-03-13 |
* | -Debugging multiple induction, a bug appeared when having function | courtieu | 2006-03-12 |
* | cleaning | jforest | 2006-03-10 |
* | Coq did not compile in Ocaml 3.06 and 3.07 since Map.S did not contain is_emp... | jforest | 2006-03-07 |
* | Exploitation du 'let rec' + présentation | herbelin | 2006-03-05 |
* | New files for subtac | coq | 2006-03-05 |
* | tactic haRVey pour appeler haRVey (contrib/dp) | filliatr | 2006-03-02 |
* | Correction bug #842 (rename d'une hyp du contexte) | herbelin | 2006-03-01 |
* | appel de Zenon | filliatr | 2006-03-01 |
* | *** empty log message *** | filliatr | 2006-02-28 |
* | dp: sortie Why | filliatr | 2006-02-27 |
* | Work on recursive definitions | coq | 2006-02-22 |
* | Add vernacular file for subtac | coq | 2006-02-22 |
* | Julien: | bertot | 2006-02-22 |
* | 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-21 |
* | 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-20 |
* | bug correction | bertot | 2006-02-17 |
* | Julien: | bertot | 2006-02-17 |