aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* 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
* bug #1951: polymorphic indtypes: universe subst was not performed in the type...Gravatar barras2008-10-06
* Correction bug assert (introduit dans la révision 11300) qui neGravatar herbelin2008-09-09
* More debugging of [Equations], now able to discharge even the heavilyGravatar msozeau2008-09-07
* Correction de bugs:Gravatar herbelin2008-08-05
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* - Rebranchement backtrack du langage déclaratif dans CoqideGravatar herbelin2008-07-18
* Modification rapide du message d'erreur lorsqu'un _ ne peut êtreGravatar herbelin2008-07-18
* Changement de catch_error pour qu'il rattrape les erreurs d'arguments Gravatar aspiwack2008-06-27
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
* Add possibility to match on defined hypotheses, using brackets toGravatar msozeau2008-06-16
* Correction de deux bugs liés au commit 11094 sur les clauses "at" et "in".Gravatar herbelin2008-06-11
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* Fixes incorrect handling of existing existentials variables inGravatar msozeau2008-06-03
* fixed catch_failerror + improved progress check + fixed repeat (repeat simpl ...Gravatar barras2008-05-29
* Strategy commands are now exportedGravatar barras2008-05-22
* refined the conversion oracleGravatar barras2008-05-21
* Move exception-handling code for catching tactics failure Gravatar msozeau2008-05-01
* Réutilisation de l'infrastructure pour le polymorphisme d'univers desGravatar herbelin2008-04-30
* Suite commit 10861Gravatar herbelin2008-04-28
* Petites corrections vis à vis des commits 10860, 10859, 10850Gravatar herbelin2008-04-28
* - Backtrack sur option with_types suite à confusion sur l'utilisationGravatar herbelin2008-04-27
* - Backtrack sur extension de syntaxe pour pose qui rentre en conflit avecGravatar herbelin2008-04-26
* Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveGravatar herbelin2008-04-25
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* - Parameterize unification by two sets of transparent_state, one for openGravatar msozeau2008-04-21
* Bug squashing day !Gravatar msozeau2008-04-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-30 18:48:23 +0000