index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
hipattern.ml
Commit message (
Expand
)
Author
Age
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-09-23
|
\
|
*
Addressing OCaml compilation warnings.
Hugo Herbelin
2016-09-16
*
|
Merge PR #244.
Pierre-Marie Pédrot
2016-09-08
|
\
\
*
|
|
CLEANUP: minor readability improvements
Matej Kosik
2016-08-24
|
|
/
|
/
|
|
*
Make the user_err header an optional parameter.
Emilio Jesus Gallego Arias
2016-08-19
|
*
Remove errorlabstrm in favor of user_err
Emilio Jesus Gallego Arias
2016-08-19
|
/
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
Separate flags for fix/cofix/match reduction and clean reduction function names.
Maxime Dénès
2016-07-01
*
Optimize the subst tactic.
Pierre-Marie Pédrot
2016-06-24
*
Removing the Q_constr file.
Pierre-Marie Pédrot
2016-06-05
*
Moving Hipattern to a regular ML file.
Pierre-Marie Pédrot
2016-06-05
*
- Réintroduction d'un parseur de pattern (q_constr.ml4) à usage de
herbelin
2006-03-22
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-26
*
Nettoyage suite à la détection par défaut des variables inutilisées par o...
herbelin
2005-11-08
*
Types inductifs parametriques
mohring
2005-11-02
*
Nouvelle en-tête
herbelin
2004-07-16
*
code obsolete
herbelin
2004-03-11
*
Ground Update.
corbinea
2003-06-20
*
Ground and CCsolve updates
corbinea
2003-05-25
*
Restructuration des procédures de filtrage
herbelin
2003-05-19
*
Enhancement of the Ground tactic, addition of GTauto and GIntuition.
corbinea
2003-05-07
*
Added the Ground tactic.
corbinea
2003-04-25
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
JMeq now treated as an equality by tactics.
courant
2002-11-14
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
Correction of a bug in Intuition (no more decomposition of dependent pairs).
corbinea
2002-05-22
*
- Reforme de la gestion des args recursifs (via arbres reguliers)
barras
2002-02-14
*
GROS COMMIT:
barras
2001-11-05
*
Suppression option immediate_discharge; nettoyage de Declare et conséquences
herbelin
2001-10-11
*
eclaircissement du code
courant
2001-09-13
*
entetes
filliatr
2001-03-15
*
Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...
herbelin
2001-02-14
*
suppression des (* open Generic *)
filliatr
2000-11-02
*
Correction incompatibilites dans la fn des types des inductifs
herbelin
2000-10-06
*
Renommage AppL en App
herbelin
2000-10-01
*
Abstraction de constr
herbelin
2000-09-14
*
Correction pour make doc
herbelin
2000-09-10
*
Ajout d'un LetIn primitif.
herbelin
2000-09-10
*
Code mort
herbelin
2000-06-15
*
Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeurs
herbelin
2000-05-31
*
Effets de bords suite à la restructuration des inductives (cf Inductive)
herbelin
2000-05-18
*
Ajout get_reference
herbelin
2000-05-03
*
Divers
herbelin
2000-05-02
*
Suite intégration de constr_pattern
herbelin
2000-04-30
*
Decoupage de tactics/pattern en proofs/pattern et tactics/hipattern
herbelin
2000-04-28