aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* Pattern matching de sous-termesGravatar delahaye2000-08-17
* retablissement make doc et make minicoqGravatar filliatr2000-07-25
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Passage à des contextes de vars et de rels pouvant contenir des déclaration...Gravatar herbelin2000-07-24
* Pattern -> parsingGravatar delahaye2000-07-21
* Modifs d'interpretation de patternsGravatar delahaye2000-07-21
* portage RefineGravatar filliatr2000-07-20
* Correction de CofixGravatar delahaye2000-07-03
* Extension de find_inductive aux co-inductifs et renommage en find_rectypeGravatar herbelin2000-07-01
* RienGravatar herbelin2000-06-29
* Modifs de presentation.Gravatar delahaye2000-06-28
* portage EAuto et RingGravatar filliatr2000-06-21
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
* Nettoyage de GenericGravatar herbelin2000-05-31
* Déplacement de save_thm and co de PFedit vers CommandGravatar herbelin2000-05-25
* Bug existential_value au lieu de existential_type + divers sur existentialGravatar herbelin2000-05-25
* DocGravatar herbelin2000-05-23
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* bug (typage avec meta)Gravatar herbelin2000-05-18
* Effets de bords suite à la restructuration des inductives (cf Inductive)Gravatar herbelin2000-05-18
* docGravatar herbelin2000-05-18
* Retrait du i pour tclTHEN_i et correction bugs DecomposeGravatar herbelin2000-05-16
* Achèvement nettoyage PfeditGravatar herbelin2000-05-05
* Nettoyage de l'interface de PfeditGravatar herbelin2000-05-04
* compilation bytecode / native :Gravatar filliatr2000-05-03
* Completion d'un match non exhaustifGravatar delahaye2000-05-03
* diverses modifs pour ocamlwebGravatar filliatr2000-05-03
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* portage Omega (mais toujours pas Zpower et Zlogarithm)Gravatar filliatr2000-05-02
* Bug redondance entre 'RRef (RMeta _)' et 'PMeta _'Gravatar herbelin2000-05-02
* Suite intégration de constr_patternGravatar herbelin2000-04-30
* Renommage bdize -> ast_of_constrGravatar herbelin2000-04-28
* Decoupage de tactics/pattern en proofs/pattern et tactics/hipatternGravatar herbelin2000-04-28
* chgt unify_0Gravatar herbelin2000-04-28
* Introduction d'un type constr_pattern pour les différents filtragesGravatar herbelin2000-04-26
* Abstraction du type typed_type (un pas vers les jugements 2 niveaux)Gravatar herbelin2000-04-20
* Nettoyage de l'interface d'Astterm; renommage des {pf_,}constr_of_com* en {pf...Gravatar herbelin2000-03-28
* Modification de type_of_case, type_case_branches, etcGravatar herbelin2000-03-21
* Remplacement plain_instance en instance qui n'a plus besoin de envGravatar herbelin2000-03-21
* Correction bug des réduction 'deltat' et renommage 'deltat' en 'evar'Gravatar herbelin2000-03-17
* documentationGravatar filliatr2000-01-28
* MAJ ocaml 2.99 (espaces dans la syntaxe des cast)Gravatar herbelin2000-01-26
* Abstraction de l'implémentation des signatures de Sign en vue intégration d...Gravatar herbelin2000-01-26
* Renommage command en constrGravatar herbelin2000-01-07
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
* rattrapage exceptions autres que UserErrorGravatar filliatr1999-12-14
* bug mk_clenv_from lorsque pas d argumentsGravatar filliatr1999-12-14
* mise a jour de refiner.ml (reports de modifs de la V6.3)Gravatar barras1999-12-13
* - états fabriqués avec -silentGravatar filliatr1999-12-13
* - méthode load sur les HintsGravatar filliatr1999-12-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 00:09:25 +0000