Open Hub
Black Duck Open Hub

 Settings |  Report Duplicate

0
I Use This!
Inactive

Commits : Listings

Analyzed 2 days ago. based on code collected 2 days ago.
May 31, 2023 — May 31, 2024
Commit Message Contributor Files Modified Lines Added Lines Removed Code Location Date
It seems more natural to put those operators at same level as "->"...
Stéphane Glondu
as glondu
More... about 16 years ago
Minor updates in the documentation of notations.
Stéphane Glondu
as glondu
More... about 16 years ago
Mise en place d'un algorithme d'inversion des contraintes de type lors du filtrage. Cela permet de détecter les cas impossibles et de simuler les contraintes d'inversion exprimables sous la forme d'un assignement des arguments du constructeurs (cf le cas de Vtail dans Bvector.v).
herbelin
More... about 16 years ago
More emacs-friendly error messages.
Stéphane Glondu
as glondu
More... about 16 years ago
Factorize code for internalization of binders to fix bug #1846. Also rewrite interp_context to use this new code instead of doing internalization by itself.
msozeau
More... about 16 years ago
Quelques éléments de réflexion
herbelin
More... about 16 years ago
Move exception-handling code for catching tactics failure in a separate function in Refiner and use it in eauto to capture the same semantics as auto (which uses tclTRY) when trying tactics.
msozeau
More... about 16 years ago
Clarification de l'ordre d'interprétation des variables dans ltac. En particulier, TacCall(_,f,[]) est utilisé pour une référence à une variable ltac ou une tactique et Reference(f) est utilisé pour une référence à une variable ltac ou un constr (en passant, standardisation de l'utilisation de constr: ou ltac: à setoid_ring).
herbelin
More... about 16 years ago
Réutilisation de l'infrastructure pour le polymorphisme d'univers des constantes qui avait été mise en place pour la 8.1gamma puis abandonné pour cause entre autres d'inefficacité. Cette fois, on restreind le polymorphisme au seul cas d'alias vers un inductif.
herbelin
More... about 16 years ago
Contournement laborieux de la "feature" de camlp5 qui entrainait le bug "no level labelled 8" (camlp5 ne sait pas annuler un extend lorsque le niveau initial existe mais est vide : l'appel à delete efface le niveau au lieu d'annuler l'effet de extend et de revenir à un niveau existant vide).
herbelin
More... about 16 years ago
Correct a bug in "new auto" and also unify_eqn which did not do local delta conversion when it should (setoid_rewrite bug reported by roconnor).
msozeau
More... about 16 years ago
Calcul plus robuste du numéro de révision (ne marche en positionnant LANG que si LC_ALL n'est pas lui-même défini)
herbelin
More... about 16 years ago
Ajout notation [ x ; ... ; y ] dans list_scope. Changement de la syntaxe interne de ring_lookup et field_lookup qui n'était pas assez robuste pour supporter une syntaxe [ ... ] dans constr. Déplacement de now_show de List.v vers Tactics.v, déplacement de "[ _ ]" au niveau 0.
herbelin
More... about 16 years ago
Suppression de la partie ML de la contrib correctness. Les fichiers n'étaient plus compilés depuis le 14 janvier 2004 (avant la 8.0), Why ayant pris la suite de correctness.
herbelin
More... about 16 years ago
Correction d'un bug dans coq_makefile: génération des règles implicites en présence de l'option -custom
notin
More... about 16 years ago
Fix eauto still using delta when it shouldn't (should make CoRN compile in reasonable time), add (unfinished) documentation on type classes. Put some classes into Prop explicitely as singleton inductive types are no longer in Prop by default even if all the arguments are (is that really what we want? roconnor says no).
msozeau
More... about 16 years ago
reparation bug de compil introduit au precedent commit
jforest
More... about 16 years ago
menage dans funind + deplaceemnt de recdef dans funind
jforest
More... about 16 years ago
Backtrack on using metas eagerly in auto, only done in "new auto" for now. Fix proof scripts that failed correspondingly. Should make many contribs compile again...
msozeau
More... about 16 years ago
Suite commit 10861
herbelin
More... about 16 years ago
Petites corrections vis à vis des commits 10860, 10859, 10850 - pour le "try", la nouvelle erreur CannotFindWellTypedAbstraction doit être catchable - pour accomoder Type -1 dans le discharge, il faut un refresh_universes strict - bugs dans les fichiers de test-suite
herbelin
More... about 16 years ago
Quelques bricoles autour de l'unification: - Un patch pour le bug de non vérification du typage de Stéphane L. - Changement du fameux message "cannot solve a second-order matching problem" en espérant, à défaut de savoir résoudre plus souvent le problème, que le message est plus explicite. - Divers changements cosmétiques.
herbelin
More... about 16 years ago
Correction du bug des types singletons pas sous-type de Set (i.e. "Inductive unit := tt." conduisait à "t:Prop" alors que le principe de la hiérarchie d'univers est d'être cumulative -- et que Set en soit le niveau 0).
herbelin
More... about 16 years ago
Suite r10857
herbelin
More... about 16 years ago
Report des quelques modifs faites avec Pierre Letouzey sur les fichiers en attendant une intégration à theories/Numbers
herbelin
More... about 16 years ago
- Backtrack sur option with_types suite à confusion sur l'utilisation des types des with-bindings dans la 8.1 [ceux-ci étaient déjà utilisés et ce qui est vraiment nouveau est que l'unification est maintenant celle de evarconv alors que c'était avant un mélange d'unify_0 (sans delta) et de coercion sur les termes sans evars]. Je renonce à maintenir la compatibilité (on se retrouve donc avec un exemple qui fonctionne différement dans TermsConv.v de CoLoR). - Robustesse accrue pour la nouvelle facilité de syntaxe de binding avec paramètre pour pose/set.
herbelin
More... about 16 years ago
- Fix bug in unification not taking into account the right meta substitution. Makes unification succeed a bit more often, hence auto works better in some cases. - Backtrack the changes of auto using Hint Unfold to do more delta and add a new tactic "new auto" which does that, for compatibility.
msozeau
More... about 16 years ago
- Backtrack sur extension de syntaxe pour pose qui rentre en conflit avec "pose as" de Program. - Report des modifs de coercion.ml (révision 10840) dans subtac_coercion.ml. - Comportement de "simple apply" rendu plus proche de celui du apply 8.1
herbelin
More... about 16 years ago
Debug implementation of failing tactics in Morphism to allow earlier failures in proof search. Catch Refiner.FailError in typeclasses eauto to indicate that an extern tactic failed.
msozeau
More... about 16 years ago
Modif un peu gadget (??): on peut écrire "set (f n:=t)" pour "set (f:=fun n => t)" (et idem pour pose).
herbelin
More... about 16 years ago