index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
proofs
/
proof_trees.mli
Age
Commit message (
Expand
)
Author
2010-04-22
Here comes the commit, announced long ago, of the new tactic engine.
aspiwack
2009-11-09
A bit of cleaning around name generation + creation of dedicated file namegen.ml
herbelin
2006-09-20
Declarative Proof Language: main commit
corbinea
2005-12-02
Changement des named_context
gregoire
2004-09-17
restructuration des printers: proofs passe avant parsing
barras
2004-09-15
hiding the meta_map in evar_defs
barras
2004-07-16
Nouvelle en-tête
herbelin
2003-10-10
code mort
herbelin
2003-09-06
Paramétrisation vis à vis de existential_key
herbelin
2002-12-19
simplification de solve_subgoal: n'utilise plus frontier
barras
2002-05-29
Réorganisation des tclTHEN (cf dev/changements.txt)
herbelin
2002-02-07
petit nettoyage de kernel/inductive
barras
2001-11-12
Suppression des stamps et donc des *_constraints
clrenard
2001-11-06
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-03-15
entetes
filliatr
2000-12-20
Ajout set_lc
herbelin
2000-12-12
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-11-21
Traitement du pretty-print des Redexp
delahaye
2000-11-02
correction Abstract (et make world passe!)
filliatr
2000-10-18
Renommage canonique :
herbelin
2000-05-03
Ajout du langage de tactiques
delahaye
2000-01-28
documentation
filliatr
1999-12-02
modifs pour premiere edition de liens
filliatr
1999-12-01
module Pfedit
filliatr
1999-12-01
- environment -> safe_environment
filliatr
1999-10-20
- documentation repertoire proofs/
filliatr
1999-10-20
modules Evar_refiner et Typing_ev
filliatr
1999-10-19
les variables existentielles contiennent maintenant un environnement (type
filliatr
1999-10-18
- déplacement (encore une fois !) des variables existentielles : elles sont
filliatr
1999-10-14
module Proof_trees
filliatr
1999-10-13
- re-introduction d'une evar_map dans unsafe_env
filliatr
1999-10-08
deplacement des var. ex. dans proofs
filliatr
1999-09-28
quelques trucs necessaires au toplevel
filliatr