| Age | Commit message (Expand) | Author |
|---|
| 2009-12-21 | Generic support for open terms in tactics | herbelin |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-06-11 | Use a lazy value for the message in FailError, so that it won't be | msozeau |
| 2009-05-20 | - Fixing declarative mode in presence of high use of Change_evars nodes | herbelin |
| 2009-03-14 | Cleaning/uniformizing the interface of tacticals.mli | herbelin |
| 2008-12-26 | - Optimized "auto decomp" which had a (presumably) exponential in | herbelin |
| 2008-10-18 | Optimisation de clenv.ml pour que meta_instance ne soit pas appelé | herbelin |
| 2008-05-01 | Move exception-handling code for catching tactics failure | msozeau |
| 2008-02-22 | Merge with lmamane's private branch: | lmamane |
| 2007-12-31 | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau |
| 2007-12-07 | Adding the tactic "instantiate" (without argument), to force the | glondu |
| 2007-07-12 | (Port of r9984) Easier debugging: | glondu |
| 2007-05-20 | - Propagation des evars non résolues vers les with_bindings; permet par exemple | herbelin |
| 2007-04-02 | Extension to the general sequence operator (tactical). Now in addition to ... | emakarov |
| 2006-10-16 | affichage des ... dans les scripts | barras |
| 2006-10-05 | revision de la semantique de rewrite ... in <clause>. details dans la doc | letouzey |
| 2006-09-26 | mise a jour du nouveau ring et ajout du nouveau field, avant renommages | barras |
| 2006-09-20 | Declarative Proof Language: main commit | corbinea |
| 2006-01-21 | Messages de idtac et fail peuvent maintenant être des listes de string, int ... | herbelin |
| 2005-01-21 | Compatibilité ocamlweb pour cible doc | herbelin |
| 2004-12-31 | Déplacement de 'project' dans Refiner pour supprimer des dépendances en Tac... | herbelin |
| 2004-09-17 | restructuration des printers: proofs passe avant parsing | barras |
| 2004-09-15 | hiding the meta_map in evar_defs | barras |
| 2004-09-07 | deuxieme vague de modifs: evar_defs fonctionnel | barras |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2003-11-12 | Idtac peut prendre un argument à afficher | narboux |
| 2003-11-05 | Amelioration de l'afficheur de script structure | herbelin |
| 2003-06-20 | Ground Update. | corbinea |
| 2003-05-19 | Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern | herbelin |
| 2003-03-31 | Ajout d'un message à FailTac | herbelin |
| 2002-12-19 | simplification de solve_subgoal: n'utilise plus frontier | barras |
| 2002-12-09 | Option pour rendre les vérifications du refiner optionnelle | herbelin |
| 2002-05-29 | Réorganisation des tclTHEN (cf dev/changements.txt) | herbelin |
| 2001-11-12 | Suppression des stamps et donc des *_constraints | clrenard |
| 2001-11-06 | Suite de la suppression : enamed_declaration est remplace par evar_map. | clrenard |
| 2001-11-06 | Suppression des local_constraints, des ctxtty et du focus. | clrenard |
| 2001-05-18 | Erreur dans un commentaire ... | clrenard |
| 2001-03-15 | entetes | filliatr |
| 2001-02-01 | application patch Cuit Alvarado : tclTHENSi et intros_until_n exportés | filliatr |
| 2000-12-12 | syntaxe AST Inversion + commentaires ocamlweb autour de $ | filliatr |
| 2000-12-02 | Portage d'AutoRewrite | delahaye |
| 2000-10-18 | Simplifications autour de typed_type (renommé types par analogie avec sorts)... | herbelin |
| 2000-10-18 | Renommage canonique : | herbelin |
| 2000-10-13 | Code redondant | herbelin |
| 2000-07-24 | Passage à des contextes de vars et de rels pouvant contenir des déclarations | herbelin |
| 2000-07-21 | Modifs d'interpretation de patterns | delahaye |
| 2000-05-23 | Doc | herbelin |
| 2000-05-16 | Retrait du i pour tclTHEN_i et correction bugs Decompose | herbelin |
| 2000-05-04 | Nettoyage de l'interface de Pfedit | herbelin |
| 2000-05-03 | Ajout du langage de tactiques | delahaye |
