index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
proofs
/
proof_type.ml
Commit message (
Expand
)
Author
Age
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Here comes the commit, announced long ago, of the new tactic engine.
aspiwack
2010-04-22
*
Generic support for open terms in tactics
herbelin
2009-12-21
*
Made the interpretation levels rlevel/glevel/tlevel truly phantom
herbelin
2009-12-19
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0
herbelin
2009-06-06
*
Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"
herbelin
2009-03-16
*
commande Timeout + compaction des traces de debug_tactic
barras
2009-03-04
*
closed bug 1898: fold x in x; added a reordering primitive tactic
barras
2008-11-26
*
Évolutions diverses et variées.
herbelin
2008-08-04
*
- Propagation des evars non résolues vers les with_bindings; permet par exemple
herbelin
2007-05-20
*
Correction du bug #1315:
notin
2007-01-22
*
affichage des ... dans les scripts
barras
2006-10-16
*
Declarative Proof Language: main commit
corbinea
2006-09-20
*
Changement des named_context
gregoire
2005-12-02
*
premiere reorganisation de l\'unification
barras
2004-09-03
*
Nouvelle en-tête
herbelin
2004-07-16
*
Suppression définitive de lmatch et or_metanum dans tacinterp
herbelin
2003-05-21
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
simplification de solve_subgoal: n'utilise plus frontier
barras
2002-12-19
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Intégration des modifs de la branche mowgli :
herbelin
2002-11-05
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
MAJ commentaires
herbelin
2002-07-23
*
Réorganisation des tclTHEN (cf dev/changements.txt)
herbelin
2002-05-29
*
Simplification de Proof_type.prim_rule
herbelin
2002-03-27
*
Uniformisation convert_hyp
herbelin
2002-02-28
*
Ajout tactiques Rename et Pose; modifications pour Inversion
herbelin
2002-02-01
*
Suppression des stamps et donc des *_constraints
clrenard
2001-11-12
*
Suite de la suppression : enamed_declaration est remplace par evar_map.
clrenard
2001-11-06
*
Suppression des local_constraints, des ctxtty et du focus.
clrenard
2001-11-06
*
GROS COMMIT:
barras
2001-11-05
*
Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'Cle...
herbelin
2001-10-05
*
Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ...
herbelin
2001-08-07
*
Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...
herbelin
2001-06-25
*
Ajout de _ dans les patterns d'intro
mohring
2001-04-12
*
amelioration de la structure des univers
barras
2001-03-28
*
entetes
filliatr
2001-03-15
*
Déplacement de qualid dans Nametab, hors du noyau
herbelin
2001-03-01
*
Prise en compte noms longs dans SuperAuto
herbelin
2001-02-16
*
Portage d'AutoRewrite
delahaye
2000-12-02
*
Renommage canonique :
herbelin
2000-10-18
*
Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion d...
herbelin
2000-09-26
*
Pattern matching de sous-termes
delahaye
2000-08-17
*
Modifs de presentation.
delahaye
2000-06-28
*
Ajout du langage de tactiques
delahaye
2000-05-03