aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/leminv.ml
Commit message (Expand)AuthorAge
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-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
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Changement des named_contextGravatar gregoire2005-12-02
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* inclusion de meta_map dans evar_defsGravatar barras2004-09-12
* 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
* Unification lemInv et lemInv_inGravatar herbelin2003-10-10
* Utilisation du second-ordre avec possibilité de K-rédex dans lemInvGravatar herbelin2002-12-24
* suite du commit precedentGravatar barras2002-12-19
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* petits changements cosmetiques sur les tactiquesGravatar barras2002-02-15
* petit nettoyage de kernel/inductiveGravatar barras2002-02-07
* Ajout tactiques Rename et Pose; modifications pour InversionGravatar herbelin2002-02-01
* compat ocaml 3.03Gravatar filliatr2001-12-13
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
* Suppression des local_constraints, des ctxtty et du focus.Gravatar clrenard2001-11-06
* GROS COMMIT:Gravatar barras2001-11-05
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* TransparentGravatar barras2001-09-20
* Remplacement de 'clause' par 'hyps' pour les tactiques qui ne peuvent pas s'a...Gravatar herbelin2001-08-05
* Branchement sur bad_tactic_argsGravatar herbelin2001-07-10
* amelioration de la structure des universGravatar barras2001-03-28
* entetesGravatar filliatr2001-03-15
* Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...Gravatar herbelin2001-01-24
* conflit useInversionLemmaGravatar mohring2000-12-13
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* caractere opaque des constantes repris en compteGravatar filliatr2000-12-04
* nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...Gravatar filliatr2000-11-06
* correction Abstract (et make world passe!)Gravatar filliatr2000-11-02
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Abstraction de constrGravatar herbelin2000-09-14
* Correction pour make docGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Plus de env et sigma dans get_arity, plus de sigma dans make_arityGravatar herbelin2000-07-01
* Extension de find_inductive aux co-inductifs et renommage en find_rectypeGravatar herbelin2000-07-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 03:20:49 +0000