aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* Ajout constructeur External pour appel outil externe à CoqGravatar herbelin2005-02-04
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...Gravatar herbelin2005-01-02
* Déplacement de 'project' dans Refiner pour supprimer des dépendances en Tac...Gravatar herbelin2004-12-31
* Suppression de la dépendance en Tacmach pour pouvoir être appelé de top_pr...Gravatar herbelin2004-12-31
* Code mortGravatar herbelin2004-11-18
* Mise en pageGravatar herbelin2004-11-17
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* 'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...Gravatar herbelin2004-10-11
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* inclusion de meta_map dans evar_defsGravatar barras2004-09-12
* simplification de clenvGravatar barras2004-09-10
* When refining a given term, the primitive refiner used to accepts some casts,Gravatar sacerdot2004-09-10
* unification encore...Gravatar barras2004-09-08
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07
* deplacement de clenv vers pretypingGravatar barras2004-09-03
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Nouvelle en-têteGravatar herbelin2004-07-16
* bugs #667 and #783 (mimick_evar and loc_table on large files)Gravatar barras2004-07-13
* bypass w_Define when w_refine-ingGravatar corbinea2004-07-07
* updated printing of evar context (may loop ?)Gravatar corbinea2004-06-30
* moved instantiate binding to extratacticsGravatar corbinea2004-06-29
* more evar stuffGravatar corbinea2004-06-28
* effective evar refiningGravatar corbinea2004-06-26
* Amélioration message d'erreur quand échec unificationGravatar clrenard2004-04-20
* Export du type de preuve en cours pour xmlGravatar herbelin2004-03-29
* Changement de natural en int_or_var pour 'do' et 'fail' pour paramétrisation...Gravatar herbelin2004-03-02
* Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...Gravatar herbelin2004-03-02
* Déplacement définition intro_pattern_expr dans GenargGravatar herbelin2004-03-01
* added breakpoints to help ideGravatar corbinea2004-02-26
* Localisation des erreurs d'internalisation des notations de tactiquesGravatar herbelin2004-02-12
* bugs avec Pose et AssertGravatar barras2004-01-09
* Bug affichage des metas dans un environnement avec definitions locales (bug 277)Gravatar herbelin2003-12-19
* Amélioration du message d'erreur "w_unify"Gravatar clrenard2003-12-01
* Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...Gravatar herbelin2003-11-25
* Prise en compte des defs syntaxiques dans is_global et global_reference qui p...Gravatar herbelin2003-11-24
* Amelioration du message d'erreur en cas de tentative d'instanciationGravatar clrenard2003-11-15
* factorisation et generalisation des clausesGravatar barras2003-11-13
* Idtac peut prendre un argument à afficherGravatar narboux2003-11-12
* petits changements de syntaxeGravatar barras2003-11-12
* Traduction semantique des InHyp de clause en InHypValue si local defGravatar herbelin2003-11-09
* Ajout pf_applyGravatar herbelin2003-11-09
* Added Instantiate ... inGravatar corbinea2003-11-06
* 2 espaces en tropGravatar herbelin2003-11-05
* Amelioration de l'afficheur de script structureGravatar herbelin2003-11-05
* nouvelle syntaxe de ltacGravatar barras2003-10-16
* code mortGravatar herbelin2003-10-10
* pf_get_new_id en provenance de feu wcclausenvGravatar herbelin2003-10-10