aboutsummaryrefslogtreecommitdiff
path: root/tactics/hipattern.ml
AgeCommit message (Expand)Author
2017-02-14Hipattern API using EConstr.Pierre-Marie Pédrot
2017-02-14Tacmach API using EConstr.Pierre-Marie Pédrot
2017-02-14Cases API using EConstr.Pierre-Marie Pédrot
2017-02-14Constr_matching API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops API using EConstr.Pierre-Marie Pédrot
2017-02-14Termops API using EConstr.Pierre-Marie Pédrot
2016-09-23Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-16Addressing OCaml compilation warnings.Hugo Herbelin
2016-09-08Merge PR #244.Pierre-Marie Pédrot
2016-08-24CLEANUP: minor readability improvementsMatej Kosik
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Remove errorlabstrm in favor of user_errEmilio Jesus Gallego Arias
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
2016-06-24Optimize the subst tactic.Pierre-Marie Pédrot
2016-06-05Removing the Q_constr file.Pierre-Marie Pédrot
2016-06-05Moving Hipattern to a regular ML file.Pierre-Marie Pédrot
2006-03-22- Réintroduction d'un parseur de pattern (q_constr.ml4) à usage deherbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...herbelin
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par o...herbelin
2005-11-02Types inductifs parametriquesmohring
2004-07-16Nouvelle en-têteherbelin
2004-03-11code obsoleteherbelin
2003-06-20Ground Update.corbinea
2003-05-25Ground and CCsolve updatescorbinea
2003-05-19Restructuration des procédures de filtrageherbelin
2003-05-07Enhancement of the Ground tactic, addition of GTauto and GIntuition.corbinea
2003-04-25Added the Ground tactic.corbinea
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
2002-11-14JMeq now treated as an equality by tactics.courant
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-05-22Correction of a bug in Intuition (no more decomposition of dependent pairs).corbinea
2002-02-14- Reforme de la gestion des args recursifs (via arbres reguliers)barras
2001-11-05GROS COMMIT:barras
2001-10-11Suppression option immediate_discharge; nettoyage de Declare et conséquencesherbelin
2001-09-13eclaircissement du codecourant
2001-03-15entetesfilliatr
2001-02-14Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...herbelin
2000-11-02suppression des (* open Generic *)filliatr
2000-10-06Correction incompatibilites dans la fn des types des inductifsherbelin
2000-10-01Renommage AppL en Appherbelin
2000-09-14Abstraction de constrherbelin
2000-09-10Correction pour make docherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-06-15Code mortherbelin
2000-05-31Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeursherbelin
2000-05-18Effets de bords suite à la restructuration des inductives (cf Inductive)herbelin
2000-05-03Ajout get_referenceherbelin
2000-05-02Diversherbelin
2000-04-30Suite intégration de constr_patternherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 03:36:55 +0000