index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
portage exemples Correctness; changement du nom de pred_of_minus dans coq_omega
filliatr
2001-04-10
*
Modified searchPattern. Before this correction, constructors were overlooked,
bertot
2001-04-10
*
réparation Correctness; options Extraction (changement de syntaxe)
filliatr
2001-04-10
*
bug lift dans IsRel de extract_type. Axiomes dans extract_type
letouzey
2001-04-10
*
Mise a jour de la config pour distrib
mohring
2001-04-10
*
MAJ
herbelin
2001-04-10
*
Bug affichage LETPATTERN
herbelin
2001-04-10
*
Bug context incoherent au passage du lambda et du let dans evar_eqappr
herbelin
2001-04-10
*
Interdiction des 'Save (thm_tok)? id' si thm pas ouvert par Goal
herbelin
2001-04-09
*
Uniformisation des 'Save def_tok id'
herbelin
2001-04-09
*
nettoyage d'entrees de grammaires inutiles
courant
2001-04-09
*
exemples Correctness
filliatr
2001-04-09
*
branchement extraction en standard (pas de Require)
filliatr
2001-04-09
*
mise à jour
filliatr
2001-04-09
*
réparation Quote
filliatr
2001-04-09
*
MAJ
herbelin
2001-04-09
*
Ajout lemmes arithmetiques
mohring
2001-04-08
*
ajout des lemmes Zimmerman
mohring
2001-04-08
*
Make sure the parser knows about the constructors of type nat, so
bertot
2001-04-07
*
Two constants had been given in the wrong package (Logic_type instead of
bertot
2001-04-07
*
correction d'un bug de Quote
filliatr
2001-04-06
*
bug Print Proof; usage coqtop/coqc
filliatr
2001-04-06
*
mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4
filliatr
2001-04-05
*
array_fold_left_i
filliatr
2001-04-05
*
axiomes dans les types
filliatr
2001-04-04
*
ajout de coq_example# dans coq-tex
werner
2001-04-04
*
renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...
filliatr
2001-04-04
*
Adding the dependencies for the parser that is used in the interface pcoq.
bertot
2001-04-04
*
implification de extract_constr et extract_term
letouzey
2001-04-04
*
adding the directives to compile the parser that is used in the graphical
bertot
2001-04-04
*
Added a flag that makes it possible to re-load files while taking only the
bertot
2001-04-04
*
Added two files that are used for the connection with the graphical user-inte...
bertot
2001-04-04
*
Add a flag to avoid sending too many warnings when reloading syntax files
bertot
2001-04-04
*
These files are used to construct an independent parser, that is a small
bertot
2001-04-04
*
These files are loaded coq-interface to make a process that is "pcoq" enabled.
bertot
2001-04-04
*
Make sure the constructors of Z and positive are recognized: they show up
bertot
2001-04-04
*
Add a Comments command, that does nothing, but is quite useful to to have
bertot
2001-04-04
*
add the binary coq-interface, used for the communication with the graphical
bertot
2001-04-04
*
add the compilation of the files needed for the interface with pcoq.
bertot
2001-04-04
*
adding entry points for the arguments of the Comment command.
bertot
2001-04-04
*
Adding A command for comments, this makes it possible to have structured
bertot
2001-04-04
*
dependencies required for contrib/interface
bertot
2001-04-04
*
Files that handle the dialogue with the graphical user-interface pcoq.
bertot
2001-04-04
*
documentation
filliatr
2001-04-04
*
supression vieux fichiers extraction
filliatr
2001-04-04
*
rollback sur les commandes Extract Constant/Inductive; nettoyage et documenta...
filliatr
2001-04-04
*
deux fichiers (past et ptype) uniquement sous forme de .mli
filliatr
2001-04-04
*
commandes Extract Constant/Inductive; message d'erreur pour les axiomes
filliatr
2001-04-03
*
The function filter_by_module, that was previously exported was not the
bertot
2001-04-03
*
Export a function (build_inductive) that is used in the graphical interface.
bertot
2001-04-03
[next]