aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2008-02-14Added default canonical structures (see example in test-suite)corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10566 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-14Backtrack changes on eauto, move specialized version of eauto inmsozeau
class_tactics for further customizations. Add Equivalence.v for typeclass definitions on equivalences and clrewrite.v test-suite for clrewrite. Debugging the tactic I found missing morphisms that are now in Morphisms.v and removed some that made proof search fail or take too long, not sure it's complete however. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10565 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-13Move class_setoid to class_tactics.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10564 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-13Debugging of the class_setoid tactic and eauto. Prepare for move frommsozeau
class_setoid to class_tactics... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10563 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-13Correction du bug #1512notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10562 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-13Implement KEEP_ML4_PREPROCESSED option in build systemlmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10561 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-13Implement NO_RECALC_DEPS option in build systemlmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10560 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-13Suppression de l'option -glob-from de Coqdoc: les globalisations sontnotin
lues directement des fichiers .glob git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10559 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-13Essai de prise en compte de delta dans unify_0 (même sur termes non clos). herbelin
- Pour éviter de pénaliser auto, eauto, autorewrite, mise en place d'une option "modulo_conv" pour contrôler l'usage de cette delta. - Pour éviter que rewrite ne réussise trop souvent, la delta est désactivée pour les tactiques d'élimination (une étude fine reste à faire). - On n'utilise aussi delta que sur les sous-termes du problème d'unification initial. C'est une heuristique qui est intuitive mais qui reste à être évaluée. - Au bilan, le surcoût en temps de compilation des theories est d'un peu moins d'1%. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10557 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-13Correction de ce qui semble être un petit bug dans la gestion de laherbelin
marge de manoeuvre vis a vis de eta dans l'unification : la convention est qu'on donne la forme eta-reduite avec l'indication du nombre d'expansions autorisées mais ce nombre était incorrect pour l'unification pattern de w_unify. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10556 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-11Correction d'un bug de clearnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10552 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-10Fixing bug 1795 (occur check was not correctly done)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10551 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-10suppression code mort oublié lors du commit 10495herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10550 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-10Granting wish 1794 (the name provided in the "using" clause of theherbelin
"abstract" tactical is now as a regular ltac parameter of the "identifier" type). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10549 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-10Backport Program Instance into Instance. Proper early error message ifmsozeau
trying to declare an instance with an already existing name. Add possibility of not giving all the fields in Instance declarations, using Refine.refine to generate the subgoals. No control over opacity in this case though... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10548 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-10Proposal of a nice notation for constructors xI and xO of type positiveletouzey
More details in the header of BinPos.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10547 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-10Major revision: use of Function, including some non-structural onesletouzey
Sequel of commit 10545 on FSetAVL. This time, no compile-time penality since there are fewer non-structural functions in FMapAVL. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10546 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-09Major revision of FSetAVL: more Function, including some non-structural onesletouzey
NB: this change adds about 10s of compile-time to a file that is already taking about 30s on my machine. If somebody strongly objects to this, contact me. I really think that the gain in uniformity, clarity, and computability (in Coq) worth the extra compile-time: no more function-by-tactic, everything (vm_)computes, and quite efficiently. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10545 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-09Solde de code mort et petites optimisations sur lesquels je suisherbelin
tombé au cours du temps git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10544 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-09Fix the clrewrite tactic, change Relations.v to work on relations in Propmsozeau
only, and get rid of the "relation" definition which makes unification fail blatantly. Replace it with a notation :) In its current state, the new tactic seems ready for larger tests. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10543 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08misc improvementsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10539 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08Documentation of CHANGES and refman doc for the implicit argument bindermsozeau
`X`. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10538 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08better comments in FMapInterfaceletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10536 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08better comments in FSetInterfaceletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10535 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08Change implementation of resolution for typeclasses to use a customizedmsozeau
eauto instead of an arbitrary tactic. Export more from eauto to allow easier debugging. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10534 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08Add more information to IllFormedRecBody exceptions, to show the exactmsozeau
definition on which it is failing (useful for Program definitions and others too). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10533 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08Move generally useful definition of nf_evar on contexts to evarutil.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10532 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08Add printer for Pp.std_ppcmds...msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10531 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08New "Preterm [ of id ] " command to show the preterm before giving it tomsozeau
Coq (solves part 2 of bug #1784). Add corresponding documentation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10530 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08Backport code from command.ml to subtac_command.ml for defininingmsozeau
recursive definitions. Now program accepts cofixpoints and uses the new way infer structurally decreasing arguments. Also, checks for correct recursive calls before giving the definition to the obligations machine (solves part 1 of bug #1784). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10529 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08more complete FSets.vletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10528 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08updates concerning FSetsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10527 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08one forgotten compatibility lemmaletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10526 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08Oubli dans r10524notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10525 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08Correction d'un bug de Coqdoc + ajout de Include dans les mots clés ↵notin
reconnus par Coqdoc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10524 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-07Mise en place d'une toute petite amélioration de l'unification deherbelin
apply : si on a trouvé une méta, alors, on l'utilise pour instancier les trous lors de la tentative de conversion modulo delta. Cela permet ainsi de résoudre de petits cas d'unification, tel que celui annoncé échouant dans le "beginner question" du 6 fevrier 2008 de coq-club. Solde au passage de modifs cosmétiques de setoid_replace.ml avant abandon probable du code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10523 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-06Suite 10518herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10521 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-06- Documentation des nouvelles options d'implicites (Set Strongly Strictherbelin
Implicit, Set Maximal Implicit Insertion, Set Reversible Pattern Implicit, Set Printing Implicit Defensive). - Changement de la sémantique de Set Strongly Strict Implicit : il contient maintenant Set Strict Implicit. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10520 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-06Détection plus souple et message un peu moins radical en cas deherbelin
fichiers emacs ouverts au moment de la création des dépendances git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10519 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-06Correction d'un bug à l'interprétation de "change" (on exigeait queherbelin
l'argument soit un type même lorsque c'était un terme qu'on convertissait). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10518 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-06Résolution d'une confusion dans le rôle des variables CAMLP4 et CAMLP4LIB:herbelin
- CAMLP4 dit si on utilise camlp4 ou camlp5 - CAMLP4LIB est le chemin camlp4/5 à donner en option -I git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10517 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-06Fix obligations not being discharged due to new definition of complement.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10516 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-06New algorithm to resolve morphisms, after discussion with Nicolasmsozeau
Tabareau: - first pass: generation of the Morphism constraints with metavariables for unspecified relations by one fold over the term. This builds a "respect" proof term for the whole term with holes. - second pass: constraint solving of the evars, taking care of finding a solution for all the evars at once. - third step: normalize proof term by found evars, apply it, done! Works with any relation, currently not as efficient as it could be due to bad handling of evars. Also needs some fine tuning of the instances declared in Morphisms.v that are used during proof search, e.g. using priorities. Reorganize Classes.* accordingly, separating the setoids in Classes.SetoidClass from the general morphisms in Classes.Morphisms and the generally applicable relation theory in Classes.Relations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10515 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-06Work-in-progress to make eauto accept a list of goals as input andmsozeau
return a solution for the whole set of goals at once only. Add "debug eauto" and "dfs eauto" syntaxes to get better control on the algorithm from the surface interface. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10514 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-06Protection contre l'erreur mentionnée dans le rapport de bug 1790herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10513 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-05kill some useless module aliases E:=X (for better name printing, see Elie's ↵letouzey
14097) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10511 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-05Correction d'un bug sur les substitutions:soubiran
Require Import FSets FSetAVL. Module M:=FSetAVL.Make Z_as_OT. (* ... uncaught exception Not_found *) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10509 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-05Add Morphisms for Qceiling and Qfloorroconnor
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10508 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-05Ajout d'un test pour le bug #1787notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10507 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-04Reorganization of FSet+FMap : no more files specific to Weak Sets/Mapsletouzey
Thanks to Elie's work and especially "Include Type ...", full sets can be simply expressed as extensions of weak sets. Moreover, Facts and Properties functors can be factorized almost completely. As a result, things like FSetWeakAAA.BBB can now be found as FSetAAA.WBBB, Same with maps / weak maps ... No backward compatibility intended for weak sets / maps, but porting scripts should mostly amounts to name changes (see above). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10505 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 20:14:35 +0000