aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacinterp.ml
Commit message (Expand)AuthorAge
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* - Add more precise error localisation when one of the application failsGravatar herbelin2009-08-04
* Added "etransitivity".Gravatar herbelin2009-08-03
* Jolification : tentative de supprimer les "( evd)" et associés quiGravatar aspiwack2009-07-07
* Add new variants of [rewrite] and [autorewrite] which differ in theGravatar msozeau2009-06-30
* Use a lazy value for the message in FailError, so that it won't beGravatar msozeau2009-06-11
* - Added two new introduction patterns with the following temptative syntaxes:Gravatar herbelin2009-06-07
* - Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: itGravatar herbelin2009-05-10
* - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceGravatar herbelin2009-05-09
* - Fixed a little bug in previous commit (bad failure in case of unknown entry).Gravatar herbelin2009-04-27
* - Cleaning (unification of ML names, removal of obsolete code,Gravatar herbelin2009-04-27
* Fixing bug #2308 ("instantiate" tactic did not comply withGravatar herbelin2009-04-24
* nouvelle version de la tactique groebner proposee par Loic:Gravatar barras2009-04-16
* Display the content of the list instead of "<list>" when an idtacGravatar herbelin2009-04-05
* Fix useless redeclaration of a tactic name when UpdateTac is replayed.Gravatar msozeau2009-03-28
* Backport from v8.2 branch of 11986 (interpretation of quantifiedGravatar herbelin2009-03-22
* coq_makefile: -c and -shared conflict; tacinterp: delay evaluation of tactic ...Gravatar barras2009-03-19
* - gros commit sur ring et field: passage des arguments simplifieGravatar barras2009-03-17
* illegal tactic application was having Ltac interpreter loopGravatar barras2009-03-04
* commande Timeout + compaction des traces de debug_tacticGravatar barras2009-03-04
* Backtrack sur la mémoïsation de nf_evar.Gravatar aspiwack2009-03-04
* =?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...Gravatar aspiwack2009-02-27
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
* Fixed bugs #2001 (search_guard was overwriting the guard index givenGravatar herbelin2009-01-04
* - Temptative change to notations like "as [|n H]_eqn" or "as [|n H]_eqn:H",Gravatar herbelin2009-01-02
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* About "apply in":Gravatar herbelin2008-12-09
* Port [rewrite] tactics to open terms. Currently no check that evarsGravatar msozeau2008-11-05
* More debugging of handling of open constrs with typeclasses:Gravatar msozeau2008-10-25
* Forgot one file which had other local modifications...Gravatar msozeau2008-10-23
* - Export de pattern_ident vers les ARGUMENT EXTEND and co.Gravatar herbelin2008-10-19
* Optimisation de clenv.ml pour que meta_instance ne soit pas appeléGravatar herbelin2008-10-18
* Backporting 11445 from 8.2 to trunk (negative conditions inGravatar herbelin2008-10-11
* Correction de bugs:Gravatar herbelin2008-08-05
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Propagation de l'information "strict" (càd à toplevel ou en train deGravatar herbelin2008-07-24
* Modification rapide du message d'erreur lorsqu'un _ ne peut êtreGravatar herbelin2008-07-18
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Quelques modifications autour du filtrage Ltac:Gravatar herbelin2008-07-16
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
* Little fixes: print unbound variable in error message (patch by SamuelGravatar msozeau2008-06-19
* incomplete bugfix for infoGravatar corbinea2008-06-19
* Better typeclass error messages, always giving the full set ofGravatar msozeau2008-06-17
* Add possibility to match on defined hypotheses, using brackets toGravatar msozeau2008-06-16
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* - Correction de la version simplifiée (filtrage sur deux sigGravatar herbelin2008-06-09
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* - Cleanup parsing of binders, reducing to a single production for allGravatar msozeau2008-05-11
* Clarification de l'ordre d'interprétation des variables dans ltac. EnGravatar herbelin2008-05-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 11:35:13 +0000