aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/hipattern.ml
Commit message (Expand)AuthorAge
...
* Removing the Q_constr file.Gravatar Pierre-Marie Pédrot2016-06-05
* Moving Hipattern to a regular ML file.Gravatar Pierre-Marie Pédrot2016-06-05
* - Réintroduction d'un parseur de pattern (q_constr.ml4) à usage deGravatar herbelin2006-03-22
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Types inductifs parametriquesGravatar mohring2005-11-02
* Nouvelle en-têteGravatar herbelin2004-07-16
* code obsoleteGravatar herbelin2004-03-11
* Ground Update.Gravatar corbinea2003-06-20
* Ground and CCsolve updatesGravatar corbinea2003-05-25
* Restructuration des procédures de filtrageGravatar herbelin2003-05-19
* Enhancement of the Ground tactic, addition of GTauto and GIntuition.Gravatar corbinea2003-05-07
* Added the Ground tactic.Gravatar corbinea2003-04-25
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* JMeq now treated as an equality by tactics.Gravatar courant2002-11-14
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* Correction of a bug in Intuition (no more decomposition of dependent pairs).Gravatar corbinea2002-05-22
* - Reforme de la gestion des args recursifs (via arbres reguliers)Gravatar barras2002-02-14
* GROS COMMIT:Gravatar barras2001-11-05
* Suppression option immediate_discharge; nettoyage de Declare et conséquencesGravatar herbelin2001-10-11
* eclaircissement du codeGravatar courant2001-09-13
* entetesGravatar filliatr2001-03-15
* Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...Gravatar herbelin2001-02-14
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Correction incompatibilites dans la fn des types des inductifsGravatar herbelin2000-10-06
* Renommage AppL en AppGravatar herbelin2000-10-01
* Abstraction de constrGravatar herbelin2000-09-14
* Correction pour make docGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Code mortGravatar herbelin2000-06-15
* Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeursGravatar herbelin2000-05-31
* Effets de bords suite à la restructuration des inductives (cf Inductive)Gravatar herbelin2000-05-18
* Ajout get_referenceGravatar herbelin2000-05-03
* DiversGravatar herbelin2000-05-02
* Suite intégration de constr_patternGravatar herbelin2000-04-30
* Decoupage de tactics/pattern en proofs/pattern et tactics/hipatternGravatar herbelin2000-04-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 08:28:54 +0000