aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/tacmach.mli
Commit message (Expand)AuthorAge
* Clean-up : no more Proof_type.proof_treeGravatar letouzey2012-10-06
* Updating headers.Gravatar herbelin2012-08-08
* Glob_term now mli-only, operations now in Glob_opsGravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Two dead functions in Tacmach.Gravatar aspiwack2012-04-18
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0Gravatar herbelin2009-06-06
* Cleaning/uniformizing the interface of tacticals.mliGravatar herbelin2009-03-14
* closed bug 1898: fold x in x; added a reordering primitive tacticGravatar barras2008-11-26
* Optimisation de clenv.ml pour que meta_instance ne soit pas appeléGravatar herbelin2008-10-18
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* Solde de code mort et petites optimisations sur lesquels je suisGravatar herbelin2008-02-09
* (Port of r9984) Easier debugging:Gravatar glondu2007-07-12
* extension of the rename tactic: the following is now allowed: Gravatar letouzey2007-07-06
* Changement des named_contextGravatar gregoire2005-12-02
* 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
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Nouvelle en-têteGravatar herbelin2004-07-16
* 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