| Commit message (Expand) | Author | Age |
|---|
| * | Directory 'contrib' renamed into 'plugins', to end confusion with archive of ... |  letouzey | 2009-03-20 |
| * | Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl) |  herbelin | 2009-03-17 |
| * | Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod -> | herbelin | 2008-12-31 |
| * | Désactivation de dumpglob lors des appels a functional induction (erreurs pa... |  notin | 2008-12-18 |
| * | first attempt to allow Function to deal with dependent pattern matching. This... |  jforest | 2008-11-23 |
| * | Move Record desugaring to constrintern and add ability to use notations |  msozeau | 2008-11-05 |
| * | Open notation for declaring record instances. | msozeau | 2008-10-23 |
| * | Generalized implementation of generalization. | msozeau | 2008-10-23 |
| * | Add enough information to correctly globalize recursive calls in inductive and | msozeau | 2008-09-11 |
| * | Évolutions diverses et variées. | herbelin | 2008-08-04 |
| * | - Extension de "generalize" en "generalize c as id at occs". | herbelin | 2008-06-08 |
| * | Improvements on coqdoc by adding more information into .glob | msozeau | 2008-05-30 |
| * | Postpone the search for the recursive argument index from the user given | msozeau | 2008-05-06 |
| * | correction of bug 1829 | jforest | 2008-04-08 |
| * | - Second pass on implementation of let pattern. Parse "let ' par [as x]? | msozeau | 2008-03-28 |
| * | Adapt funind to the RLetPattern constructor. | msozeau | 2008-03-15 |
| * | Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b... | msozeau | 2008-01-17 |
| * | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau | 2007-12-31 |
| * | Plus de combinateurs sont passés de Util à Option. Le module Options |  aspiwack | 2007-12-06 |
| * | Factorisation des opérations sur le type option de Util dans un module | aspiwack | 2007-12-05 |
| * | Ajout de eelim, ecase, edestruct et einduction (expérimental). | herbelin | 2007-10-03 |
| * | Slight cleanup of refl_omega.ml : in particular it uses now list | letouzey | 2007-07-11 |
| * | Add a parameter to QuestionMark evar kind to say it can be turned into an obl... | msozeau | 2007-03-19 |
| * | r11153@tannat: jforest | 2007-03-16 10:25:55 +0100 | jforest | 2007-03-16 |
| * | Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de | herbelin | 2007-02-13 |
| * | Retour r9310 en attendant mieux | herbelin | 2007-02-09 |
| * | Meilleur anglais (cf 9619) | herbelin | 2007-02-07 |
| * | Extension du polymorphisme de sorte au cas des définitions dans Type. | herbelin | 2006-10-28 |
| * | Detection des paramettres pour les Functions bien fondees | jforest | 2006-09-27 |
| * | Gestion des arguments implicites dans les Functions bien fondees | jforest | 2006-09-19 |
| * | correction of bug #1220 | jforest | 2006-09-18 |
| * | mise en conformite des messages d'erreur de Function avec la doc. | jforest | 2006-09-14 |
| * | Amelioration des messages d'erreur de Fucntion | jforest | 2006-08-24 |
| * | Bug corrections in Function. | jforest | 2006-08-11 |
| * | Code cleaning in Function | jforest | 2006-07-18 |
| * | Code cleaning in Function | jforest | 2006-07-18 |
| * | bug correction when defining graph of fixpoints/definitions not generated by ... | jforest | 2006-07-13 |
| * | +functional inversion now takes the function to invert as an optional argument. | jforest | 2006-07-10 |
| * | - completely new version of "functional inversion" using inversion on | jforest | 2006-07-04 |
| * | ajout d'un argument with_clean a Indfun.functional_induction permettant de ch... | jforest | 2006-06-13 |
| * | rearrangement du code: deplacement du code effectuant functional |  courtieu | 2006-06-13 |
| * | LetTuple are now supported in Function | jforest | 2006-05-22 |
| * | Correction in generate_graph (now handles fun _ => fix ....) | jforest | 2006-05-05 |
| * | Cleanning and factorizing code in funind. Spliting new_arg_principles into to... | jforest | 2006-05-03 |
| * | Replacing "GenFixpoint" with "Function" and "mes" with "measure" | jforest | 2006-04-26 |
| * | + Handling "if" and cast in GenFixpoint | jforest | 2006-04-24 |
| * | Si un fixpoint a plusieurs arguments, mais un seul de type inductif, | letouzey | 2006-04-14 |
| * | + Changing a little functional schemes types | jforest | 2006-04-10 |
| * | Adding "New Functional Scheme" | jforest | 2006-03-20 |
| * | + Debugging and cleaning functional principle generation tactic | jforest | 2006-03-14 |
letouzey
herbelin
notin
jforest
msozeau
aspiwack
courtieu