aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/tacmach.mli
Commit message (Expand)AuthorAge
* Ajout pf_applyGravatar herbelin2003-11-09
* pf_get_new_id en provenance de feu wcclausenvGravatar herbelin2003-10-10
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* code mortGravatar herbelin2002-12-21
* Option pour rendre les vérifications du refiner optionnelleGravatar herbelin2002-12-09
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* Simplification de Proof_type.prim_ruleGravatar herbelin2002-03-27
* Uniformisation convert_hypGravatar herbelin2002-02-28
* Ajout tactiques Rename et Pose; modifications pour InversionGravatar herbelin2002-02-01
* Cosmétique avant toutGravatar herbelin2001-11-20
* Diverses petites simplications de la machine de preuves.Gravatar clrenard2001-11-19
* Suppression des stamps et donc des *_constraintsGravatar clrenard2001-11-12
* Suite de la suppression : enamed_declaration est remplace par evar_map.Gravatar clrenard2001-11-06
* Suppression des local_constraints, des ctxtty et du focus.Gravatar clrenard2001-11-06
* GROS COMMIT:Gravatar barras2001-11-05
* Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'Cle...Gravatar herbelin2001-10-05
* Nettoyage reduce_to_ind et one_step_reduceGravatar herbelin2001-09-09
* Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ...Gravatar herbelin2001-08-07
* Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...Gravatar herbelin2001-06-25
* amelioration de la structure des universGravatar barras2001-03-28
* entetesGravatar filliatr2001-03-15
* application patch Cuit Alvarado : tclTHENSi et intros_until_n exportésGravatar filliatr2001-02-01
* Mise en place de la possibilite d'unfolder des variables locales et des const...Gravatar filliatr2001-01-31
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Portage d'AutoRewriteGravatar delahaye2000-12-02
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Elimination des coupures sur le type constantGravatar herbelin2000-10-04
* Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion d...Gravatar herbelin2000-09-26
* Abstraction de constrGravatar herbelin2000-09-14
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* 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
* Modifs d'interpretation de patternsGravatar delahaye2000-07-21
* portage EAuto et RingGravatar filliatr2000-06-21
* Retrait du i pour tclTHEN_i et correction bugs DecomposeGravatar herbelin2000-05-16
* Nettoyage de l'interface de PfeditGravatar herbelin2000-05-04
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* Nettoyage de l'interface d'Astterm; renommage des {pf_,}constr_of_com* en {pf...Gravatar herbelin2000-03-28
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
* modifs pour premiere edition de liensGravatar filliatr1999-12-02
* module PfeditGravatar filliatr1999-12-01
* - environment -> safe_environmentGravatar filliatr1999-12-01
* - Typing -> Safe_typingGravatar filliatr1999-12-01
* module Tactics (debut)Gravatar filliatr1999-11-22
* module Pattern, Wcclausenv (interface) et TacticalsGravatar filliatr1999-11-19
* module Clenv (debut)Gravatar filliatr1999-10-20
* modules Evar_refiner et Typing_evGravatar filliatr1999-10-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-19 15:17:48 +0000