aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2008-06-07Correct handling of the environment in build_signature, and throwmsozeau
2008-06-07Change setoid_rewrite's matching semantics to continue matching insidemsozeau
2008-06-07Fix library index template and associated script.msozeau
2008-06-07add tiny change to coqidejnarboux
2008-06-06Enhancements to coqdoc, better globalization of sections and modules.msozeau
2008-06-06avoid duplicated creation of WFacts instancesletouzey
2008-06-06ajout d'un printer pour les contraintes d'univers + correction d'un bug sur l...soubiran
2008-06-062-3 petites modifs pour la compilation sous Windows...notin
2008-06-06Copie des .cmi en plus des .cma et des .cmxanotin
2008-06-06Correction terminologie et ajout plage unicode 1D400-1D7FF (mathematicalherbelin
2008-06-06- On adopte finalement la méthode de Pierre Courtieu pour le undo deherbelin
2008-06-05Quelques infos pour la portabilité 8.1 --> 8.2notin
2008-06-05One (last?) more update of CHANGES.letouzey
2008-06-05changed w_coerce_to_type to consider remaining unif problems (Hugo\'s patch)barras
2008-06-05Fix typoslmamane
2008-06-05Renommage id dans le test Nametab (suite ajout d'une constante de ceherbelin
2008-06-05Correctly catch UnresolvableConstraint exception which is now located. msozeau
2008-06-04more updates of CHANGESletouzey
2008-06-03Fixes incorrect handling of existing existentials variables inmsozeau
2008-06-03Fix setoid_rewrite documentation examples.msozeau
2008-06-03improve name, size and position of detached windowsjnarboux
2008-06-03Some updates of CHANGES (to be continued...)letouzey
2008-06-03try to reduce the size of the queries panejnarboux
2008-06-03Temporarily disabling automatic test for bug 1338.vnotin
2008-06-03In abstract parts of theories/Numbers, plus/times becomes add/mul, letouzey
2008-06-02In abstract parts of theories/Numbers, plus/times becomes add/mul, letouzey
2008-06-02Minor bug correction in recdefjforest
2008-06-02Petites corrections diverses :herbelin
2008-06-02newton iteration for sqrt31thery
2008-06-01Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided inletouzey
2008-06-01remove additional occurrences of +/- forgotten in commit 11030letouzey
2008-06-01On cesse de demander une valeur pour l'option reals si l'utilisateurherbelin
2008-06-01Bactrack sur +, - dans rewrite qui, redondants avec ->, <-, n'en sont qu'àherbelin
2008-06-01Quelques amendements liées à la compilation des packages.herbelin
2008-06-01BigQ: starting to create and use an interface QSigletouzey
2008-06-01Enhance the BigN and BigZ infrastructure: letouzey
2008-05-31Fix last commit about revision: I'm unsure about the role of "set -e", letouzey
2008-05-31Attempt to avoid killing+recreating the file revision with same content.letouzey
2008-05-30Improvements on coqdoc by adding more information into .globmsozeau
2008-05-30Improve the dependent induction tactic to automatically find themsozeau
2008-05-30- Correction d'un nouveau bug de undo de CoqIDE ("Admitted" et "Proof t"herbelin
2008-05-29fixed catch_failerror + improved progress check + fixed repeat (repeat simpl ...barras
2008-05-29backtrack sur utilisation de do_overwrite_confirmationjnarboux
2008-05-29commented out overwrite confirmation handler (requires lablgtk >=2.10)barras
2008-05-29transparent backgroundbarras
2008-05-29fixed bug #1780: a lift was missing (match predicate)barras
2008-05-29NBigN: proofs that BigN implements axioms of NAxiomsSigletouzey
2008-05-28- Modification de la déf de minus et pred conformément aux remarques deherbelin
2008-05-28Notation concise pour la valeur par défaut des cas reconnus commeherbelin
2008-05-28Cyclic31: no more Admitted, but I've cheated: sqrt31 and sqrt312 are letouzey