aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/inv.ml
Commit message (Expand)AuthorAge
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Made intros_until and onInductionArg a bit stricter and robustGravatar herbelin2010-06-13
* Fixed bug #2135 (second-order unification was raising cryptic message)Gravatar herbelin2010-06-12
* Fixing spelling: pr_coma -> pr_commaGravatar herbelin2010-06-12
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Fixing XML doc (COQ_XML not working as an environment variable).Gravatar herbelin2009-10-24
* Fixed a bug in the interaction between dEqThen and inject_at_positionsGravatar herbelin2009-09-27
* Delay the choice of eliminator in destruct/induction until we know ifGravatar herbelin2009-09-27
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Added two new introduction patterns with the following temptative syntaxes:Gravatar herbelin2009-06-07
* Cleaning/uniformizing the interface of tacticals.mliGravatar herbelin2009-03-14
* - Deactivation of dynamic loading on Mac OS 10.5 (see bug #2024).Gravatar herbelin2009-01-11
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
* About "apply in":Gravatar herbelin2008-12-09
* - Fixed bug 1968 (inversion failing due to a Not_found bug introduced inGravatar herbelin2008-11-09
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Modification rapide du message d'erreur lorsqu'un _ ne peut êtreGravatar herbelin2008-07-18
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
* - Un peu de doc, préparation du CHANGES pour la release.Gravatar herbelin2008-04-15
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
* Quelques améliorations des intro patterns:Gravatar herbelin2008-04-04
* bug in accessing n-th abstractionGravatar barras2008-01-18
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Ajout de eelim, ecase, edestruct et einduction (expérimental).Gravatar herbelin2007-10-03
* New intro pattern "@A", which generates a fresh name based on A.Gravatar glondu2007-07-06
* Nouvelle stratégie d'unification des types des with-bindings dansGravatar herbelin2007-05-22
* - Propagation des evars non résolues vers les with_bindings; permet par exempleGravatar herbelin2007-05-20
* Ajout motif d'introduction "?" (IntroAnonymous) pour laisser CoqGravatar herbelin2006-01-16
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Réparation bug #1004; nettoyageGravatar herbelin2005-09-08
* Correction bug de dependent_hyps qui ne met pas à jour le type des hyps dép...Gravatar herbelin2005-03-20
* Restructuration fonctions de réécriture depuis égalité dépendanteGravatar herbelin2004-10-27
* Simplifications concommitantes à la correction du bug #855Gravatar herbelin2004-09-24
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* inclusion de meta_map dans evar_defsGravatar barras2004-09-12
* simplification de clenvGravatar barras2004-09-10
* unification encore...Gravatar barras2004-09-08
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Nouvelle en-têteGravatar herbelin2004-07-16
* Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...Gravatar herbelin2004-03-02
* Déplacement définition intro_pattern_expr dans GenargGravatar herbelin2004-03-01
* bugs avec Pose et AssertGravatar barras2004-01-09
* factorisation et generalisation des clausesGravatar barras2003-11-13
* Un Try supplementaire utile pour la compatibilite, car bring_hyps dans genera...Gravatar herbelin2003-10-13
* Bug calcul du nom de la premiere equationGravatar herbelin2003-10-11