Open Hub
Black Duck Open Hub

 Settings |  Report Duplicate

0
I Use This!
Inactive

Commits : Listings

Analyzed 1 day ago. based on code collected 2 days ago.
May 08, 2023 — May 08, 2024
Commit Message Contributor Files Modified Lines Added Lines Removed Code Location Date
Mauvaise dépendance dans Makefile.doc
notin
More... almost 16 years ago
Oubli lors de la révision #11177
notin
More... almost 16 years ago
Some work on BigQ : * keep only one implementation of BigQ * QMake (ex-Q0Make) becomes functorial * proofs in it have been reworked, some new functions (e.g. red, power) * BigQ.t is declared to be a setoid and a field
letouzey
More... almost 16 years ago
Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisation (add_glob* et dump_*)
notin
More... almost 16 years ago
Report de la révision #11175 de la branche v8.2 vers le trunk
notin
More... almost 16 years ago
Installation de la documentation
notin
More... almost 16 years ago
Micromega : bugs fixes - renaming of tactics - documentation
fbesson
More... almost 16 years ago
Typo in documentation (isn't it?)
Stéphane Glondu
as glondu
More... almost 16 years ago
Les contraintes d'univers sont maintenant collectées dans le champs mod_constraints des modules.
soubiran
More... almost 16 years ago
Catch a Not_found exception in the Combined Scheme mechanism to hide an ugly Anomaly with a better error message
vsiles
More... almost 16 years ago
Suppression de l'option -dump-glob et ajout d'une option -no-glob
notin
More... almost 16 years ago
MAJ fichiers spécifiques trunk
herbelin
More... almost 16 years ago
Rename obligations_tactic to obligation_tactic and fix bugs #1893.
msozeau
More... almost 16 years ago
Code cleanup in typeclasses, remove dead and duplicated code. Change from named_context to rel_context for class params and fields.
msozeau
More... almost 16 years ago
Correction petit bug sur révision 11159 (res_pf fait un effet de bord sur le sigma, utilisation de refine à la place).
herbelin
More... almost 16 years ago
Fix bug #1889, correct globalization in class declarations.
msozeau
More... almost 16 years ago
- Implantation de la suggestion 1873 sur discriminate. Au final, discriminate/injection/simplify_eq acceptent maintenant un terme comme argument. Les clauses "with" et les variantes "e" sont aussi acceptées. Aussi, discriminate sans argument essaie maintenant toutes les hyps quantifiées (au lieu de traiter seulement les buts t1<>t2).
herbelin
More... almost 16 years ago
Correction bug #1886 (pb unification.ml, report de 11157 de v8.2 vers trunk)
herbelin
More... almost 16 years ago
Various improvements in handling of evars in general and typing constraints in Program: - normalize types and defs of local fixpoints before checking the guardness condition to avoid having to give type annotations, e.g: << Definition fold (A B : Set) (f : B -> A -> B) : B -> tree A -> B := fix aux acc t := match t with | Leaf x => f acc x | Node l => fold_left aux l acc end. >> - add new inh_coerce_to_prod to allow coercion of the typing constraint to a product before trying to split it. It's a noop in standard mode, and forgets subsets in Program. Allows to typecheck: << (λ x, x) : { f : nat -> nat | ... } >>. - Better handling of the "abstract" typing constraints in Program. - Correctly normalize w.r.t. evars. the tycon given by users in Program.
msozeau
More... almost 16 years ago
typo in a comment
letouzey
More... almost 16 years ago
Little fixes: print unbound variable in error message (patch by Samuel Bronson), some keywords in coqdoc, and test well-typedness of predicate in subtac_cases after abstraction.
msozeau
More... almost 16 years ago
incomplete bugfix for info
corbinea
More... almost 16 years ago
removed unwanted linebreaks in pretty printing
corbinea
More... almost 16 years ago
Propagation des révisions 11144 et 11136 de la 8.2 vers le trunk (résolution entre autres des bugs 1882, 1883, 1884).
herbelin
More... almost 16 years ago
Fix bug in implementation of splitting of class constraints.
msozeau
More... almost 16 years ago
Improvements in subtac: - Use return clause inference in addition to the automatic generation of equalities for pattern-matching. - Disallow generation of coercions between type constructors, which are not provable anyway. - Improve inference for local (co-)fixpoints using the typing constraint.
msozeau
More... almost 16 years ago
Compatibility fixes (Add Setoid bug and accidental introduction of a tactic named "app").
msozeau
More... almost 16 years ago
meilleur gestion de la fonction de "cache" des alias (declaremods), et correction d'un bug sur Import/Export module.
soubiran
More... almost 16 years ago
Detection de l'architecture sous Windows (et sans uname -o)
notin
More... almost 16 years ago
Où l'on se débarrasse de uname -o
notin
More... almost 16 years ago