aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2008-11-26closed bug 1898: fold x in x; added a reordering primitive tacticbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11633 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-26closed bug 1898: fold x in x; added a reordering primitive tacticbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11632 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-25correction bug 1997.soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11630 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-24eventually fixing r11612barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11626 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-24amelioration mineur du comportement de Functionjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11625 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-23first attempt to allow Function to deal with dependent pattern matching. ↵jforest
This Functionnality is VERY VERY experimental and only works with non recursive functions and structurally defined function git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11624 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-23- Synchronized subst_object with load_object (load_and_subst_objects)herbelin
and set Declare ML Module as a regular substitutive object so that Declare ML Module is treated at the right place in the order of appearance of substitutive declarations of a required module. - Note: The full load/import mechanism for modules is not so clear: the Require part of a Require Import inside a module is set outside the module at module closing but the Import part remains inside (why not to put the "special" objects in the module too?); moreover the "substitute" and "keep" objects of a module are desynchronised at module closing (is that really harmless/necessary?). - Treatment of .cmxs targets in coq_makefile and in coqdep. - Better make clean in coq_makefile generated makefiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11623 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-23Fine-tuning rewriting from "eq_true b": using <- to rewrite true to bherbelin
(if ever necessary). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11621 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-23Minor improvement to commit 11619herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11620 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-23Fixed bug #2006 (type constraint on Record was not taken into account) +herbelin
slight improving of the printing of record. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11619 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-22Fixed bug in VernacExtend printing + missing vernacular printing rules +herbelin
revival of option -translate as a -beautify option. PS: compilation checked against 11610. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11618 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-22- Fixed minor bug #1994 in the tactic chapter of the manual [doc]herbelin
- Improved warning when found several path to the same file in path [mltop.ml4, system.ml] - Add support for "rewrite" on specific equality to true (i.e. eq_true) [Datatypes.v, tactics] PS: compilation test made over 11611 to shunt the archive-breaking 11612 and 11614 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11617 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-21fixed problem with r11612barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11614 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-21fixed exponential behavior of evar unif (ground case)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11612 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-20correction of bug #2002jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11610 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-19Add implicit rules for native plugins (.cmxs)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11607 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-19Execute #rectypes directive in embedded OCaml toplevel...glondu
...to avoid the need to have cflags.cmi around. This directive will likely be available in the next version of OCaml. See OCaml bug #4460. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11605 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-19Fix typo in omega docglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11604 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-17integrate suggestions by B. Baydemir (see #1930)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11600 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-16Univ: two < instead of a Pervasives.compare on int (as suggested by X. Leroy)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11595 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-15Correct display of constraints for Print Universes "dumpfile"letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11593 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-20 17:06:24 +0000