aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2008-11-14Amélioration du README.doc et de l'installation de la docnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11591 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-14Restores behaviour of v8.1 for unification problems which fail (backport of ↵letouzey
11585) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11590 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-14Faster comparison of universesletouzey
- compare the integer indexes first, in order to avoid comparing the dirpath part if possible - use an ad-hoc comparison function rather than Pervasives.compare (slightly faster during my tests on the compcert contrib) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11589 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-14make doc ne compilait plus la doc de stdlib (bug #1996)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11588 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-14Add missing test-suite files for closed bugs.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11587 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-14retour sur le commit 11579 qui faisait plante les contribs FSet et color.soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11586 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-13Tentative d'amélioration de la robustesse des Makefile générés parnotin
coq_makefile en présence de fichiers .ml : - ajout d'une option -config à coqtop qui affiche les informations de configuration (COQTOP, COQBIN, COQLIB, CAMLP4, CAMLP4LIB, CAMLBIN, LOCAL) - coq_makefile inclut un fichier Makefile.config qui contient les valeurs des variables sus-mentionnées git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11584 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-13git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11583 ↵barras
85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-12Correction du bug #1995notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11580 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-12Les signatures des applications de foncteur sont précalculées, cela ↵soubiran
alourdit un peu les vo mais accélère la compilation lorsque les foncteurs sont massivement utilisés. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11579 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-10Makefile.build: an OPTFLAGS behind a bytecode ocamlc (which refuses -p)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11577 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-10Fix mixup between Record, Structure and Class by adding a new variant formsozeau
the three cases. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11572 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-10Fix bug reported by Mark Dickinson on Coq-Club about [setoid_rewrite] notmsozeau
reducing the type of the given lemma. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11571 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-09- Correction erreur dans test output Notation.vherbelin
- Ajout test pour non-régression du bug #1968 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11569 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-09f_equal : solve an inefficiency issue (apply vs. simple apply)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11567 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-09better fix for #1931 by using sort_ofletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11566 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-09Oops... forgot to commit a file related to r11561.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11565 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-09Add test-suite file related to discussion of syntax of implicit binders.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11564 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-09More factorization of inductive/record and typeclasses: move classmsozeau
declaration code to toplevel/record, including support for singleton classes as definitions. Parsing code also factorized. Arnaud: one more thing to think about when refactoring the definitions in vernacentries. Add support for specifying what to do with anonymous variables in contexts during internalisation (fixes bug #1982), current choice is to generate a name for typeclass bindings. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11563 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-09- Fixed bug 1968 (inversion failing due to a Not_found bug introduced inherbelin
Evarutil.check_and_clear_in_constr in V8.2 revision 11309 and trunk revision 11300). - Improved various error messages related to inversion, evars and case analysis (including the removal of the obsolete dependent/non dependent distinction). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11561 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-08Apply vmconv if there are no _undefined_ evars around.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11560 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-07Slight change of the semantics of user-given casts: they don't reallymsozeau
help the type _checking_ anymore (they don't become typing constraints) but they permit to coerce a subterm in a type. In particular, when using a VM cast we avoid unneeded, unexpected conversions using the default machine (oops!). Also remove the corresponding comment in pretyping and fix the wrong use of casts in toplevel/command: accept the trouble of using evars. This has the somewhat adverse effect that when typing casted object we now have no typing constraints (see e.g. examples in Cases.v)! Probably, this will be backtracked partially tomorrow as many contribs can rely on it and the change could make some unifications fail (in particular with deep coercions). Let's try anyway! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11558 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-07- Ajout possibilité de lancer ocamldebug sur coqideherbelin
- Correction bug #1815 sur "coqide dir_inexistant/nom_fichier" - Tests oubliés de la révision 11438 (amélioration affichage coercions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11555 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-07Suite #11533notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11554 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-07Correction du bug #1926notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11553 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-07Add some example uses of the new record features in Record.v:msozeau
- introduction notation with missing fields and interaction with Program. - Ability to add (currently a single) "where notation" clause to each field. - Use every information available to do type inference and internalisation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11552 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-07Fix a bug in the specialization by unification tactic related to the problemsmsozeau
given by injection. Add the example to the test-suite for [dependent destruction]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11551 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-07Add the ability to give a specific tactic to solve each obligation inmsozeau
Program. No syntax to do it yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11550 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-07Fix universe problem appearing ConCaT using the existing infrastructure formsozeau
declaring additional conversion problems when unifying the type of an evar instance and the evar's declared type. Fix the corresponding conversion heuristic which failed due to (misplaced?) assertions when faced with general conversion problems. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11549 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-06Cosmetic: no more whitespace at end of lines in extraction filesletouzey
(diff says it's a big commit, whereas diff -w says it's an empty one ;-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11547 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-06Correction d'un petit bug en cas de redéfintion par l'utilisateur de ↵notin
variables utilisées dans PP git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11546 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-05Minor fixes:msozeau
- Rework definition of the type of respecful functions in Morphisms.v - Unfold [flip] in "Add Morphism" tactic (suggested by N. Tabareau) - Add a "coqvariableref" command in coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11545 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-05Port [rewrite] tactics to open terms. Currently no check that evarsmsozeau
introduced by the lemma remain in the subgoals (i.e. it's really [erewrite]). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11544 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-05Fix in the unification algorithm using evars: unify types of evarmsozeau
instances and the corresponding evar's type if it contains existentials to avoid dangling evars. No noticeable performance impact (at least on the stdlib). Subsumes (and fixes) the (broken) fix in unification.ml that was previously patched by M. Puech. Improve error messages related to existential variables and type classes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11543 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-05Move Record desugaring to constrintern and add ability to use notationsmsozeau
for record fields (using "someproj : sometype where not := constr" syntax). Only one notation allowed currently and no redeclaration after the record declaration either (will be done for typeclasses). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11542 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-05Suite commit 11539 sur notation Record dans (Co)Inductive (MAJherbelin
contrib/interface avec Arnaud) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11541 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-05Petit bug dans le commit précédent.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11540 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-05Nouvelle syntaxe pour écrire des records (co)inductifs :aspiwack
CoInductive stream (A:Type) := { hd : A ; tl : stream A }. Inductive nelist (A:Type) := { hd : A ; tl : option (nelist A) }. L'affichage n'est pas encore poli. Il reste à choisir l'exact destin de la syntaxe qui était apparue dans la 8.2beta pour les records coinductifs (qui consistait à utiliser "Record" au lieu de "CoInductive" comme maintenant). VernacRecord et VernacInductive semblent maintenant faire doublon, il doit y avoir moyen de les fusionner. Les records mutuellement inductifs restent aussi à faire. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11539 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-05Better extraction renaming phase (fix #1914 plus other non-reported bugs)letouzey
Ocaml : - Fix the Coq__1 that was appearing in a .mli for some functor app in the corresponding .ml (virtual printing of the interface in the .ml + a pp_modname delayed in MTfunsig) - Cleanup in MTwith parts - Better handling of subst for MTsig - Correct push/pop_visible in pp_struct/pp_signature Common : - Merge most of pp_global and pp_module - Clarify the use of tables : remove some of them, attach many others to their corresponding function. - The "visible" table now groups mps, their content, and some subst (for the inside of MTsig) - Cleanup of tables is done via a registration mecanism - No more "initial" create_renamings, instead some fully on-the-fly renaming (thanks to the "Pre" phase) - opened libaries are computed between "Pre" and "Impl" phases - for simplicity, static_clash aren't computed statically anymore (cost?) Extract_env: - A "Pre" phase not only for Ocaml - Extraction Library is in fact also Recursive (for getting a right mpfiles_content) ... but only last item is printed to a real file instead of /dev/null Modutil: No more struct_get_references_* Util : fix the evaluation order of prlist_strict git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11538 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-04Adaptation to ocaml 3.11 new semantics of String.index_from (see bug #1974)herbelin
Grant wish #1988 ("fun" forces reduction in "refine" if needed) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11536 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-042 petites améliorations de coq_makefile (traitement des .ml4 + cibles ↵notin
génériques dans -custom git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11535 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-02Fix CAMLHLIB (due to r11358) (Closes: #1986)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11532 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-02test-suite/ideal-features/{apply.v -> eapply_evar.v}glondu
...to avoid trouble on case-insensitive filesystems (Closes: #1987) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11531 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-31Ajout d'une option -raw pour Coqdoc (sortie en texte brut)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11529 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-31allowed patternidents starting with an '_'amahboub
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11526 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-30The lexer is changer to break former PATTERNIDENT into two tokens.amahboub
This allows more flexibility in the other uses of the question mark and in particular suppresses the hack for rewriter in g_tactic.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11524 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-29Document native "Declare ML Module"glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11523 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-29Remove calls to Dynlink.add_{interfaces,available_units} altogetherglondu
According to OCaml's Changes, all modules loaded so far (and statically linked) are available to dynamically loaded modules (since 3.07). Therefore, these calls seem irrelevant now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11522 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-29Adaptation du vieil appel à "apply" sur lemme de symétrie au cas oùherbelin
une réduction a eu lieu (insertion d'un "change" pour que "apply" n'échoue pas). À faire : nettoyer la construction par tactique de la preuve de symétrie de a=b -> b=a (quand le lemme de symétrie n'existe pas) pour quelle ne lance pas une conversion potentiellement longue entre a et b (le cas est arrivé dans CatsInZFC/notation.v !) [HH + MS] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11521 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-29Oups...notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11520 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-17 03:00:06 +0000