index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
proofs
/
tacmach.mli
Commit message (
Expand
)
Author
Age
*
Less use of the list-based interface for goal-bound tactics.
aspiwack
2013-11-02
*
Tachmach.New is now in Proofview.Goal.enter style.
aspiwack
2013-11-02
*
Getting rid of Goal.here, and all the related exceptions and combinators.
aspiwack
2013-11-02
*
Makes the new Proofview.tactic the basic type of Ltac.
aspiwack
2013-11-02
*
Moving side effects into evar_map. There was no reason to keep another
ppedrot
2013-10-05
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Merging Context and Sign.
ppedrot
2013-04-29
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Modulification of identifier
ppedrot
2012-12-14
*
Clean-up : no more Proof_type.proof_tree
letouzey
2012-10-06
*
Updating headers.
herbelin
2012-08-08
*
Glob_term now mli-only, operations now in Glob_ops
letouzey
2012-05-29
*
locus.mli for occurrences+clauses, misctypes.mli for various little things
letouzey
2012-05-29
*
Two dead functions in Tacmach.
aspiwack
2012-04-18
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
Here comes the commit, announced long ago, of the new tactic engine.
aspiwack
2010-04-22
*
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/uniformizing the interface of tacticals.mli
herbelin
2009-03-14
*
closed bug 1898: fold x in x; added a reordering primitive tactic
barras
2008-11-26
*
Optimisation de clenv.ml pour que meta_instance ne soit pas appelé
herbelin
2008-10-18
*
Évolutions diverses et variées.
herbelin
2008-08-04
*
- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)
herbelin
2008-06-10
*
Solde de code mort et petites optimisations sur lesquels je suis
herbelin
2008-02-09
*
(Port of r9984) Easier debugging:
glondu
2007-07-12
*
extension of the rename tactic: the following is now allowed:
letouzey
2007-07-06
*
Changement des named_context
gregoire
2005-12-02
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...
herbelin
2005-01-02
*
restructuration des printers: proofs passe avant parsing
barras
2004-09-17
*
premiere reorganisation de l\'unification
barras
2004-09-03
*
Nouvelle en-tête
herbelin
2004-07-16
*
Ajout pf_apply
herbelin
2003-11-09
*
pf_get_new_id en provenance de feu wcclausenv
herbelin
2003-10-10
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
code mort
herbelin
2002-12-21
*
Option pour rendre les vérifications du refiner optionnelle
herbelin
2002-12-09
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
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
*
Cosmétique avant tout
herbelin
2001-11-20
*
Diverses petites simplications de la machine de preuves.
clrenard
2001-11-19
*
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
[next]