aboutsummaryrefslogtreecommitdiff
path: root/contrib/funind
AgeCommit message (Expand)Author
2008-05-06Postpone the search for the recursive argument index from the user givenmsozeau
2008-04-28menage dans funind + deplaceemnt de recdef dans funindjforest
2008-04-25Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveherbelin
2008-04-24Remplacement de l'appel à interp_constr pour globaliser une constanteherbelin
2008-04-21- Parameterize unification by two sets of transparent_state, one for openmsozeau
2008-04-12Désactivation du dumping des notations quand funind appelle lesherbelin
2008-04-12Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.msozeau
2008-04-08correction of bug 1829jforest
2008-03-28- Second pass on implementation of let pattern. Parse "let ' par [as x]?msozeau
2008-03-18Added a function to rebuild an elim scheme from elim_scheme_info. Willcourtieu
2008-03-15Adapt funind to the RLetPattern constructor.msozeau
2008-03-14Backtrack wrong commit.courtieu
2008-03-14indentation.courtieu
2008-03-13trying fcourtieu
2008-03-08correction d'un bug d'efficacite dans Function (+ ajout de eauto_with_bases)jforest
2008-02-22Merge with lmamane's private branch:lmamane
2008-01-17Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...msozeau
2008-01-09Correction of bug #1769jforest
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau
2007-12-06Plus de combinateurs sont passés de Util à Option. Le module Options aspiwack
2007-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
2007-11-27bug correction in functional inversion principle generationjforest
2007-11-26minor bug correction in Functionjforest
2007-11-19Bug in functionnal induction principle generationjforest
2007-11-08Prise en compte des notations "alias" dans la globalisation des coercions.herbelin
2007-10-30Cleaning code and comment.courtieu
2007-10-03Ajout de eelim, ecase, edestruct et einduction (expérimental).herbelin
2007-09-15* Adding compability with ocaml 3.10 + camlp5 (rework of letouzey
2007-08-31correction bug d'efficacite dans Functionjforest
2007-07-11Slight cleanup of refl_omega.ml : in particular it uses now listletouzey
2007-07-06extension of the rename tactic: the following is now allowed: letouzey
2007-05-20- Propagation des evars non résolues vers les with_bindings; permet par exempleherbelin
2007-05-17correction de bug dans Function et augmentation de la classe des fonctions su...jforest
2007-04-28Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.herbelin
2007-04-05Mise en place d'une nouvelle strategie plus efficace pour les preuves de Func...jforest
2007-03-19Add a parameter to QuestionMark evar kind to say it can be turned into an obl...msozeau
2007-03-16 r11153@tannat: jforest | 2007-03-16 10:25:55 +0100jforest
2007-02-13Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé deherbelin
2007-02-12Bug mineur dans la generation des principes d'induction pour Functionjforest
2007-02-11Correction d'un bug dans la génération des principes d'inductionjforest
2007-02-09Retour r9310 en attendant mieuxherbelin
2007-02-07Meilleur anglais (cf 9619)herbelin
2007-01-26Contounement d'un probleme avec la VM dans Function jforest
2007-01-19Protection contre les warnings 'unused variable' de ocaml 3.09herbelin
2006-11-24Functional graph merging deals with letins.courtieu
2006-11-24Fixed the graph merging parameter order.courtieu
2006-11-23Fixing syntax and parameter order in functional graph merging.courtieu
2006-11-20Changing merging functional scheme syntax.courtieu
2006-11-16Small fix in functional graph merging.courtieu
2006-11-13Correction de la seconde partie du bug #1278jforest