aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proof_type.ml
Commit message (Expand)AuthorAge
...
* commande Timeout + compaction des traces de debug_tacticGravatar barras2009-03-04
* closed bug 1898: fold x in x; added a reordering primitive tacticGravatar barras2008-11-26
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* - Propagation des evars non résolues vers les with_bindings; permet par exempleGravatar herbelin2007-05-20
* Correction du bug #1315:Gravatar notin2007-01-22
* affichage des ... dans les scriptsGravatar barras2006-10-16
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
* Changement des named_contextGravatar gregoire2005-12-02
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Nouvelle en-têteGravatar herbelin2004-07-16
* Suppression définitive de lmatch et or_metanum dans tacinterpGravatar herbelin2003-05-21
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* simplification de solve_subgoal: n'utilise plus frontierGravatar 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
* MAJ commentairesGravatar herbelin2002-07-23
* Réorganisation des tclTHEN (cf dev/changements.txt)Gravatar herbelin2002-05-29
* Simplification de Proof_type.prim_ruleGravatar herbelin2002-03-27
* Uniformisation convert_hypGravatar herbelin2002-02-28
* Ajout tactiques Rename et Pose; modifications pour InversionGravatar herbelin2002-02-01
* Suppression des stamps et donc des *_constraintsGravatar clrenard2001-11-12
* Suite de la suppression : enamed_declaration est remplace par evar_map.Gravatar clrenard2001-11-06
* Suppression des local_constraints, des ctxtty et du focus.Gravatar clrenard2001-11-06
* GROS COMMIT:Gravatar barras2001-11-05
* Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'Cle...Gravatar herbelin2001-10-05
* Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ...Gravatar herbelin2001-08-07
* Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...Gravatar herbelin2001-06-25
* Ajout de _ dans les patterns d'introGravatar mohring2001-04-12
* amelioration de la structure des universGravatar barras2001-03-28
* entetesGravatar filliatr2001-03-15
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* Prise en compte noms longs dans SuperAutoGravatar herbelin2001-02-16
* Portage d'AutoRewriteGravatar delahaye2000-12-02
* Renommage canonique :Gravatar herbelin2000-10-18
* Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion d...Gravatar herbelin2000-09-26
* Pattern matching de sous-termesGravatar delahaye2000-08-17
* Modifs de presentation.Gravatar delahaye2000-06-28
* Ajout du langage de tactiquesGravatar delahaye2000-05-03