aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/funind/rawtermops.ml
Commit message (Expand)AuthorAge
* Experimental merging of two functional graphs.Gravatar courtieu2006-10-26
* + timide essai pour le traitement des as dans les patterns lors de la generat...Gravatar jforest2006-08-16
* +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
* - completely new version of "functional inversion" using inversion onGravatar jforest2006-07-04
* + ameliorating the tactic "functional induction"Gravatar jforest2006-06-06
* bug in alpha-conversionGravatar jforest2006-06-01
* LetTuple are now supported in FunctionGravatar jforest2006-05-22
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* + Handling "if" and cast in GenFixpoint Gravatar jforest2006-04-24
* + Changing a little functional schemes types Gravatar jforest2006-04-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
* New version of functional induction / inversion. By Julien Forest,Gravatar coq2006-02-01