index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
proofs
/
refiner.ml
Commit message (
Expand
)
Author
Age
*
Really compare evar maps in progress, due to merging in apply and other
msozeau
2009-01-23
*
Évolutions diverses et variées.
herbelin
2008-08-04
*
- Rebranchement backtrack du langage déclaratif dans Coqide
herbelin
2008-07-18
*
fixed catch_failerror + improved progress check + fixed repeat (repeat simpl ...
barras
2008-05-29
*
Move exception-handling code for catching tactics failure
msozeau
2008-05-01
*
Merge with lmamane's private branch:
lmamane
2008-02-22
*
Adding the tactic "instantiate" (without argument), to force the
glondu
2007-12-07
*
Extension to the general sequence operator (tactical). Now in addition to ...
emakarov
2007-04-02
*
Correction du bug #1315:
notin
2007-01-22
*
bug #1194: normalisation evars a la sortie de focus
barras
2006-10-23
*
affichage des ... dans les scripts
barras
2006-10-16
*
revision de la semantique de rewrite ... in <clause>. details dans la doc
letouzey
2006-10-05
*
mise a jour du nouveau ring et ajout du nouveau field, avant renommages
barras
2006-09-26
*
Declarative Proof Language: main commit
corbinea
2006-09-20
*
Standardisation du nom des méthodes de Evd
herbelin
2006-04-28
*
replacing whd_betaiotaevar_preserving_vm_cast
jforest
2006-04-14
*
Correction bug #842 (rename d'une hyp du contexte)
herbelin
2006-03-01
*
Messages de idtac et fail peuvent maintenant être des listes de string, int ...
herbelin
2006-01-21
*
changement d'egalite pour le named_context_val
gregoire
2005-12-05
*
Changement des named_context
gregoire
2005-12-02
*
Confusion assert/error détectée par nouveau warning X de ocaml 3.09
herbelin
2005-11-04
*
Protection against saving a proof with still non-instantiated evars (cf bug #...
herbelin
2005-04-29
*
Protection against saving a proof with still non-instantiated evars (cf bug #...
herbelin
2005-04-29
*
Déplacement de 'project' dans Refiner pour supprimer des dépendances en Tac...
herbelin
2004-12-31
*
Mise en page
herbelin
2004-11-17
*
restructuration des printers: proofs passe avant parsing
barras
2004-09-17
*
hiding the meta_map in evar_defs
barras
2004-09-15
*
deuxieme vague de modifs: evar_defs fonctionnel
barras
2004-09-07
*
deplacement de clenv vers pretyping
barras
2004-09-03
*
premiere reorganisation de l\'unification
barras
2004-09-03
*
Nouvelle en-tête
herbelin
2004-07-16
*
added breakpoints to help ide
corbinea
2004-02-26
*
Bug affichage des metas dans un environnement avec definitions locales (bug 277)
herbelin
2003-12-19
*
Idtac peut prendre un argument à afficher
narboux
2003-11-12
*
2 espaces en trop
herbelin
2003-11-05
*
Amelioration de l'afficheur de script structure
herbelin
2003-11-05
*
Paramétrisation vis à vis de existential_key
herbelin
2003-09-06
*
Ground update
corbinea
2003-07-08
*
Ground Update.
corbinea
2003-06-20
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
Affichage des tactiques en v8
herbelin
2003-04-07
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
Ajout d'un message à FailTac
herbelin
2003-03-31
*
simplification de solve_subgoal: n'utilise plus frontier
barras
2002-12-19
*
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
*
Intégration des modifs de la branche mowgli :
herbelin
2002-11-05
*
Protection contre l'encapsulage de FailError dans Exc_located (sinon, par exe...
herbelin
2002-07-11
*
Réorganisation des tclTHEN (cf dev/changements.txt)
herbelin
2002-05-29
*
prterm -> prterm_env
filliatr
2002-02-08
[next]