index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
proofs
/
pfedit.mli
Commit message (
Expand
)
Author
Age
...
*
declaration_hooks use Ephemeron
gareuselesinge
2013-10-18
*
get rid of closures in global/proof state
gareuselesinge
2013-08-08
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Use the Hook module here and there.
ppedrot
2013-05-12
*
A uniformization step around understand_* and interp_* functions.
herbelin
2013-05-09
*
Fixing ocamldoc compilation.
ppedrot
2013-05-06
*
Merging Context and Sign.
ppedrot
2013-04-29
*
Restrict (try...with...) to avoid catching critical exn (part 5)
letouzey
2013-03-13
*
Modulification of identifier
ppedrot
2012-12-14
*
Updating headers.
herbelin
2012-08-08
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
remove many excessive open Util & Errors in mli's
letouzey
2012-05-29
*
New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr
letouzey
2012-05-29
*
A unified backtrack mechanism, with a basic "Show Script" as side-effect
letouzey
2012-03-23
*
Remove old proof-managment commands Suspend/Resume
letouzey
2012-03-23
*
Integrated obligations/eterm and program well-founded fixpoint building to to...
msozeau
2012-03-14
*
Noise for nothing
pboutill
2012-03-02
*
Proof using ...
gareuselesinge
2011-12-12
*
Moving implicit tactic support from Tacinterp to Pfedit and final evar
herbelin
2011-09-26
*
Remove code concerning the obsolete Set/Unset Undo
letouzey
2011-09-05
*
Applying Tom Prince's patch for build_constant_by_tactic not able to
herbelin
2011-04-08
*
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
*
Pfedit.resume_proof doesn't implicitly Pfedit.suspend_proof
pboutill
2010-05-05
*
Various minor improvements of comments in mli for ocamldoc
letouzey
2010-04-29
*
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
*
Added support for definition of fixpoints using tactics.
herbelin
2009-11-27
*
A bit of cleaning around name generation + creation of dedicated file namegen.ml
herbelin
2009-11-09
*
Restructuration of command.ml + generic infrastructure for inductive schemes
herbelin
2009-11-08
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Fixed bugs #2001 (search_guard was overwriting the guard index given
herbelin
2009-01-04
*
Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve
herbelin
2008-04-25
*
Merge with lmamane's private branch:
lmamane
2008-02-22
*
Declarative Proof Language: main commit
corbinea
2006-09-20
*
Changement des named_context
gregoire
2005-12-02
*
Implementation of a new backtracking system, that allow to go back
coq
2005-04-20
*
restructuration des printers: proofs passe avant parsing
barras
2004-09-17
*
Nouvelle en-tête
herbelin
2004-07-16
*
Export du type de preuve en cours pour xml
herbelin
2004-03-29
*
Gestion en temps constant de la pile des Unfo; affichage des buts par Pfedit ...
herbelin
2003-10-10
*
Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...
herbelin
2003-10-08
*
Ajout du vernac Proof with
gregoire
2002-12-12
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
simplification common_ancestor
courant
2002-11-13
*
Intégration des modifs de la branche mowgli :
herbelin
2002-11-05
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
Ajout d'un point d'entree pour exporter les arbres de preuves en XML
herbelin
2002-07-24
*
Commentaires
herbelin
2002-06-14
[prev]
[next]