aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/funind/functional_principles_proofs.ml
Commit message (Expand)AuthorAge
* About "apply in":Gravatar herbelin2008-12-09
* first attempt to allow Function to deal with dependent pattern matching. This...Gravatar jforest2008-11-23
* Fixes and refinements regarding occurrence selection:Gravatar herbelin2008-10-26
* - New auto hints for transparency/opacity control, not bound to Gravatar msozeau2008-08-22
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Enhanced discrimination nets implementation, which can now work withGravatar msozeau2008-06-27
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveGravatar herbelin2008-04-25
* - Parameterize unification by two sets of transparent_state, one for openGravatar msozeau2008-04-21
* Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.Gravatar msozeau2008-04-12
* correction d'un bug d'efficacite dans Function (+ ajout de eauto_with_bases)Gravatar jforest2008-03-08
* 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
* minor bug correction in FunctionGravatar jforest2007-11-26
* Bug in functionnal induction principle generationGravatar jforest2007-11-19
* Ajout de eelim, ecase, edestruct et einduction (expérimental).Gravatar herbelin2007-10-03
* * Adding compability with ocaml 3.10 + camlp5 (rework of Gravatar letouzey2007-09-15
* correction bug d'efficacite dans FunctionGravatar jforest2007-08-31
* extension of the rename tactic: the following is now allowed: Gravatar letouzey2007-07-06
* correction de bug dans Function et augmentation de la classe des fonctions su...Gravatar jforest2007-05-17
* Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.Gravatar herbelin2007-04-28
* Mise en place d'une nouvelle strategie plus efficace pour les preuves de Func...Gravatar jforest2007-04-05
* Bug mineur dans la generation des principes d'induction pour FunctionGravatar jforest2007-02-12
* Correction d'un bug dans la génération des principes d'inductionGravatar jforest2007-02-11
* Correction de la seconde partie du bug #1278Gravatar jforest2006-11-13
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
* Detection des paramettres pour les Functions bien fondeesGravatar jforest2006-09-27
* two minor bug corrections in General Recursive Functions Gravatar jforest2006-08-25
* Bug corrections in Function.Gravatar jforest2006-08-11
* In the old version, recursive functions cannot be declared inside a sectionGravatar bertot2006-08-08
* +functional inversion now takes the function to invert as an optional argument. Gravatar jforest2006-07-10
* - completely new version of "functional inversion" using inversion onGravatar jforest2006-07-04
* forgot a file Gravatar jforest2006-06-29
* + ameliorating the tactic "functional induction"Gravatar jforest2006-06-06
* Replacing the old version of "functional induction" with the new one. Gravatar jforest2006-05-31
* Error during last commit (coq didn't compile)Gravatar jforest2006-05-23
* Correcting a bug with ocaml <= 3.08.3 (Map.fold changing)Gravatar jforest2006-05-23
* + correcting a bug in general recursive function (match e with _ => match f e...Gravatar jforest2006-05-07
* Cleanning and factorizing code in funind. Spliting new_arg_principles into to...Gravatar jforest2006-05-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-03 13:40:23 +0000