aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Factorize code for internalization of binders to fix bug #1846. AlsoGravatar msozeau2008-05-04
* Quelques éléments de réflexionGravatar herbelin2008-05-03
* Move exception-handling code for catching tactics failure Gravatar msozeau2008-05-01
* Clarification de l'ordre d'interprétation des variables dans ltac. EnGravatar herbelin2008-05-01
* Réutilisation de l'infrastructure pour le polymorphisme d'univers desGravatar herbelin2008-04-30
* Contournement laborieux de la "feature" de camlp5 qui entrainait leGravatar herbelin2008-04-30
* Correct a bug in "new auto" and also unify_eqn which did not do localGravatar msozeau2008-04-30
* Calcul plus robuste du numéro de révision (ne marche en positionnantGravatar herbelin2008-04-29
* Ajout notation [ x ; ... ; y ] dans list_scope. Changement de laGravatar herbelin2008-04-29
* Suppression de la partie ML de la contrib correctness. Les fichiersGravatar herbelin2008-04-29
* Correction d'un bug dans coq_makefile: génération des règles implicites en...Gravatar notin2008-04-29
* Fix eauto still using delta when it shouldn't (should make CoRN compileGravatar msozeau2008-04-29
* reparation bug de compil introduit au precedent commitGravatar jforest2008-04-28
* menage dans funind + deplaceemnt de recdef dans funindGravatar jforest2008-04-28
* Backtrack on using metas eagerly in auto, only done in "new auto" forGravatar msozeau2008-04-28
* Suite commit 10861Gravatar herbelin2008-04-28
* Petites corrections vis à vis des commits 10860, 10859, 10850Gravatar herbelin2008-04-28
* Quelques bricoles autour de l'unification:Gravatar herbelin2008-04-27
* Correction du bug des types singletons pas sous-type de SetGravatar herbelin2008-04-27
* Suite r10857Gravatar herbelin2008-04-27
* Report des quelques modifs faites avec Pierre Letouzey sur lesGravatar herbelin2008-04-27
* - Backtrack sur option with_types suite à confusion sur l'utilisationGravatar herbelin2008-04-27
* - Fix bug in unification not taking into account the right metaGravatar msozeau2008-04-27
* - Backtrack sur extension de syntaxe pour pose qui rentre en conflit avecGravatar herbelin2008-04-26
* Debug implementation of failing tactics in Morphism to allow earlierGravatar msozeau2008-04-26
* Modif un peu gadget (??): on peut écrire "set (f n:=t)" pour Gravatar herbelin2008-04-26
* Adaptation des fichiers de micromega suite aux changements dansGravatar notin2008-04-25
* Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveGravatar herbelin2008-04-25
* correction bug 1839Gravatar soubiran2008-04-25
* - Fix bug in eterm which was not taking filtered contexts in evars intoGravatar msozeau2008-04-25
* Remplacement de l'appel à interp_constr pour globaliser une constanteGravatar herbelin2008-04-24
* Fix bug #1844, generalize implementation to handle and combination ofGravatar msozeau2008-04-24
* - Add pretty-printers for Idpred, Cpred and transparent_state, used forGravatar msozeau2008-04-24
* Ajout propriété svn:keywords aux nouveaux fichiers du commit 10840Gravatar herbelin2008-04-24
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* correction d'un bug sur la compostion des substitutions induites par les alia...Gravatar soubiran2008-04-23
* correction du bug sur Parameter Inline que j'ai reouvert hier par inadvertanceGravatar soubiran2008-04-23
* Added frozen state after each command.Gravatar courtieu2008-04-23
* Backtrack on change of flags for elim, otherwise rewrite goes underGravatar msozeau2008-04-23
* Change default eauto depth to 100 in setoid_rewrite, bump necessaryGravatar msozeau2008-04-23
* Test que la bibliothèque ZArith est chargée lors d'un appel à simplify, er...Gravatar notin2008-04-22
* correction bug 1839Gravatar soubiran2008-04-22
* fixed universes bug related to module inclusionGravatar barras2008-04-22
* test module include w.r.t. universe constraintsGravatar barras2008-04-21
* added the .vo checker (with independent Makefile)Gravatar barras2008-04-21
* - Correct unification for the rewrite variant of setoid_rewrite,Gravatar msozeau2008-04-21
* - Parameterize unification by two sets of transparent_state, one for openGravatar msozeau2008-04-21
* Addded the "Dump Tree" command.Gravatar cek2008-04-21
* corection bug #1837Gravatar soubiran2008-04-21
* Correction bug 1838 + doc modules.Gravatar soubiran2008-04-21