aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacinterp.ml
Commit message (Expand)AuthorAge
* Make usage of Dyn explicitGravatar glondu2009-10-28
* New cleaning phase of the Local/Global option managementGravatar herbelin2009-10-26
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Relaxed error severity when encountering unknown library objects or tacticGravatar gmelquio2009-10-06
* Apply "Declare Implicit Tactic" also to terms interpreted as "openGravatar herbelin2009-09-27
* Fixed a hole in glob_tactic that allowed some Ltac code to refer toGravatar herbelin2009-09-26
* Only one "in" clause in "destruct" even for a multiple "destruct".Gravatar herbelin2009-09-20
* Remove useless Liboject.export_function fieldGravatar glondu2009-09-17
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11
* Added syntax "exists bindings, ..., bindings" for iterated "exists".Gravatar herbelin2009-09-10
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 15:02:37 +0000