aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Take constraints into account in the "instantiate" tacticGravatar herbelin2009-10-30
* Remove old compatibility stuff (Tacred.nf)Gravatar glondu2009-10-28
* fixed czar bug with parametric inductivesGravatar corbinea2009-10-27
* Add support for remaining side-conditions in "apply in as".Gravatar herbelin2009-10-25
* Improved the treatment of Local/Global options (noneffective Local onGravatar herbelin2009-10-25
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Only one "in" clause in "destruct" even for a multiple "destruct".Gravatar herbelin2009-09-20
* - Fixed a bug in checking that implicit arguments are all correctlyGravatar herbelin2009-09-18
* Remove useless Liboject.export_function fieldGravatar glondu2009-09-17
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* 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
* Added "etransitivity".Gravatar herbelin2009-08-03
* - Fixing bug #2139 (kernel-based test of well-formation of eliminationGravatar herbelin2009-07-15
* Reactivation of pattern unification of evars in apply unification, inGravatar herbelin2009-07-08
* Jolification : tentative de supprimer les "( evd)" et associés quiGravatar aspiwack2009-07-07
* Use a lazy value for the message in FailError, so that it won't beGravatar msozeau2009-06-11
* Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0Gravatar herbelin2009-06-06
* Backtrack on experimental unification with sort variables: it requires Gravatar msozeau2009-06-02
* A try at using sort variables during unification. Instead of refreshingGravatar msozeau2009-05-23
* - Fixing declarative mode in presence of high use of Change_evars nodesGravatar herbelin2009-05-20
* Minor unification changes:Gravatar msozeau2009-05-18
* Fixing bug #2308 ("instantiate" tactic did not comply withGravatar herbelin2009-04-24
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20
* Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"Gravatar herbelin2009-03-16
* Cleaning/uniformizing the interface of tacticals.mliGravatar herbelin2009-03-14
* commande Timeout + compaction des traces de debug_tacticGravatar barras2009-03-04
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
* pushed evar reduction in kernelGravatar barras2009-02-06
* Really compare evar maps in progress, due to merging in apply and otherGravatar msozeau2009-01-23
* Backporting from v8.2 to trunk:Gravatar herbelin2009-01-18
* Fixed bugs #2001 (search_guard was overwriting the guard index givenGravatar herbelin2009-01-04
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* - Optimized "auto decomp" which had a (presumably) exponential inGravatar herbelin2008-12-26
* Fix looping class resolution bug discovered by B. Aydemir and use theGravatar msozeau2008-12-14
* About "apply in":Gravatar herbelin2008-12-09
* fixing problem with CompCert: reordering resulting from tac change was not cl...Gravatar barras2008-11-27
* closed bug 1898: fold x in x; added a reordering primitive tacticGravatar barras2008-11-26
* Fixes and refinements regarding occurrence selection:Gravatar herbelin2008-10-26
* Backtrack sur commit 11467 (tentative d'optimisation meta_instance quiGravatar herbelin2008-10-26
* More debugging of handling of open constrs with typeclasses:Gravatar msozeau2008-10-25
* Fix for bug #1981, correct the mismatch between the meta types used inGravatar msozeau2008-10-25
* Raise informative errors instead of Failures or anomalies in case a metaGravatar msozeau2008-10-24
* - 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
* fixing r11433 again:Gravatar barras2008-10-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 21:19:58 +0000