aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/funind/rawterm_to_relation.ml
Commit message (Expand)AuthorAge
* Les records déclarés avec Record ne peuvent plus être récursifs (le Gravatar aspiwack2009-01-19
* DISCLAIMERGravatar puech2009-01-17
* Generalized binding syntax overhaul: only two new binders: `() and `{},Gravatar msozeau2008-12-14
* amelioration mineur du comportement de FunctionGravatar jforest2008-11-24
* first attempt to allow Function to deal with dependent pattern matching. This...Gravatar jforest2008-11-23
* More factorization of inductive/record and typeclasses: move classGravatar msozeau2008-11-09
* Move Record desugaring to constrintern and add ability to use notationsGravatar msozeau2008-11-05
* Nouvelle syntaxe pour écrire des records (co)inductifs :Gravatar aspiwack2008-11-05
* Open notation for declaring record instances.Gravatar msozeau2008-10-23
* - Second pass on implementation of let pattern. Parse "let ' par [as x]?Gravatar msozeau2008-03-28
* Adapt funind to the RLetPattern constructor.Gravatar msozeau2008-03-15
* Merge with lmamane's private branch:Gravatar lmamane2008-02-22
* Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...Gravatar msozeau2008-01-17
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Add a parameter to QuestionMark evar kind to say it can be turned into an obl...Gravatar msozeau2007-03-19
* Detection des paramettres pour les Functions bien fondeesGravatar jforest2006-09-27
* Ajout possibilité clause "where" dans co-points fixes Gravatar herbelin2006-09-01
* Amelioration des messages d'erreur de Fucntion Gravatar jforest2006-08-24
* + timide essai pour le traitement des as dans les patterns lors de la generat...Gravatar jforest2006-08-16
* Code cleaning in FunctionGravatar jforest2006-07-18
* +functional inversion now takes the function to invert as an optional argument. Gravatar jforest2006-07-10
* Use typing informations while defining graphs for Function. Gravatar jforest2006-07-05
* adding comments and cleaning code Gravatar jforest2006-07-04
* - completely new version of "functional inversion" using inversion onGravatar jforest2006-07-04
* Passage des graphes de Function dans Type Gravatar jforest2006-06-23
* LetTuple are now supported in FunctionGravatar jforest2006-05-22
* Fixing two minor bugs in recdef and graph of function generation. Gravatar jforest2006-05-03
* Cleanning and factorizing code in funind. Spliting new_arg_principles into to...Gravatar jforest2006-05-03
* - Distinction explicite des parties paramètres et arguments dans le typeGravatar herbelin2006-04-27
* + Handling "if" and cast in GenFixpoint Gravatar jforest2006-04-24
* + Changing a little functional schemes types Gravatar jforest2006-04-10
* cleaning Gravatar jforest2006-03-10
* Coq did not compile in Ocaml 3.06 and 3.07 since Map.S did not contain is_emp...Gravatar jforest2006-03-07
* Julien:Gravatar bertot2006-02-17
* Julien:Gravatar bertot2006-02-08
* New version of functional induction / inversion. By Julien Forest,Gravatar coq2006-02-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 08:55:03 +0000