aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2007-07-18Raffinement de interp_ident pour que l'ident interprété soit au choixherbelin
frais (par exemple pour "intro") ou pas forcément (par exemple pour "fresh") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10021 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-18Makefile: needs GNU Make 3.81lmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10020 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-18J'ai enlevé un fichier qui était en double. Merci à Pierre pour avoir aspiwack
noté cette erreur de ma part (copier/coller mon amour). Ça créait des soucis dans les dépendance dans l'ancienne architecture de Makefile, probablement dans la nouvelle aussi dans certaines circonstances. Exit les bêtise, c'est plus propre maintenant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10019 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-18Makefile: more robustness all aroundlmamane
- Make sure make notices when a command fails - don't leave behind half-baked output files of commands that failed git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10016 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-17Makefile: Do _not_ delete dummy .ml files of .ml4 files even when not needed ↵lmamane
anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10015 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-16Do not try to clean the doc when no config/Makefilelmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10013 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-16Reorganise cleaning targetslmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10012 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-16Makefile: -MG doesn't (and can't) do what is necessarylmamane
The -MG option causes gcc to add any non-found .h file verbatim in the dependencies. This naturally doesn't include the path to it (because the path is unknown) and thus make doesn't know how to build it; it knows how to build kernel/byterun/coq_jumptbl.h, not "coq_jumptbl.h". --This line, and those below, will be ignored-- M Makefile.common M Makefile.build git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10011 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-16A cleaner solution to "make deletes .ml4.d files -> infinite loop" problemlmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10010 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-16Oups... empty .ml4.d files producedlmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10009 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-16CAMLP4DEPS will not work for .byteml and .optmllmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10008 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-16Generalized CAMLP4USE for pp dependenciescorbinea
Removed parsing/lexer.ml4 special case No file depends on pa_extend_m.cmo anymore, Wierd ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10007 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-16Makefile: work around gcc bug: lhs of make rule created by -MM does not ↵lmamane
include path git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10006 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-16Makefile: in C, .d files need to depend on the same as the .o filelmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10005 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-16makefile: dependencies of .c files: assume missing headers are generated fileslmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10004 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-15Makefile: use CFLAGS for dependency generation of .c fileslmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10003 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-13An update on axiomatization of number classes.emakarov
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10002 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-13some more useless constant in const_omegaletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10001 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-13Beginning of a reorganisation of the ml part for romega: letouzey
- deletion of some dead code - grouping all stuff depending on Z in a nice module Int git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10000 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-13A emacs-specific comment to use makefile-mode on Makefile.*letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9999 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-13Added Qpower_plus' and Zpower_Qpowerroconnor
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9997 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-13Small cleanupletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9996 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-13Répertoire Numbers poursuit l'objectif entamé en syntaxe V7 dans leherbelin
répertoire Num. Suppression de ce dernier de l'archive courante. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9995 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-13Deletion of some firstorder calls in FSetAVL: letouzey
after commit 9983 of Bruno concerning kernel/closure.ml, a few firstorder were awfully slow. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9994 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-13New bootstrapping, improved, Makefile systemcorbinea
Documented in dev/doc/build-system.txt . git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9992 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-13removing a warning at compilation timejforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9991 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-12Proof for subthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9990 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-12(Port of r9984) Easier debugging:glondu
* explicitation of some types * tags for grammar entries git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9989 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-12Update (test-suite was not successful).glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9988 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-12Deletion of an obsolete file (euclidian division done in old syntax with ↵letouzey
realizers) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9987 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-12Deletion of contrib/extraction/testletouzey
Not maintained, probably broken, of no interest except (maybe) for myself, bad interaction with tools that work recursively (coqdep). ===> I move it to a personal repository git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9986 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-12normalisation (by closure) was not performed under fixpointsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9983 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-12port de r9968: bug avec les ring calculatoiresbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9982 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-12An optimization to simplify generated obligations removing unnecessary let-in's.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9981 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-12Fix bug when adding progs with no obligationsmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9978 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-12Forgot to commit new Makefilemsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9975 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-12Remove dead modules in Subtac.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9973 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-12Cleanup, use Util list functions when possiblemsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9972 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-12Proof for succ, add, predthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9971 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-11dead codeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9970 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-11Slight cleanup of refl_omega.ml : in particular it uses now listletouzey
utilities from Util. Some additions in Util, and simplifications in various files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9969 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-11Added ForAll_Str_nth_tlroconnor
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9967 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-10Big reorganization of romega/ReflOmegaCore.v: towards a modular letouzey
and generic romega tactic... For the moment, nothing is visible yet from the user's point of view (hopefully). But internally, we prepare a romega that can works on any integer types. ReflOmegaCore is now separated in several modules: * First, an interface Int that specifies the minimal amount of things needed on our integer type for romega to work: - int should be a ring (re-use of ring_theory definition ;-) - it should come with an total order, compatible with + * - - we should have a decidable ternary comparison function - moreover, we ask one (and only one!) critical property specific to integers: a<b <-> a<=b-1 * Then a functor IntProperties derives from this interface all the various lemmas on integers that are used in the romega part, in particular the famous OMEGA?? lemmas. * The romega reflexive part is now in another functor IntOmega, that rely on some Int: no more Z inside. The main changes is that Z0 was a constructor whereas our abstract zero isn't. So matching Z0 is transformed into (if beq ... 0 then ...). With extensive use of && and if then else, it's almost clearer this way. * Finally, for the moment Z_as_Int show that Z fulfills our interface, and ZOmega = IntOmega(Z_as_Int) is used by the tactic. Remains to be done: - revision of the refl_omega to use any Int instead of just Z, and creating a user interface. - Int has no particular reason to use the leibniz equality (only rely on the beq boolean test). Setoids someday ? - a version with "semi-ring" for nat ? or rather a generic way to plug additional equations on the fly, e.g. n>=0 for every nat subpart ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9966 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-09Petites corrections sur le Makefilenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9965 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-09More natural notation for intro pattern: @a -> ?aglondu
Caveat about a slight loss of compatibility: Some intro patterns don't need space between them. In particular intros ?a?b used to be legal and equivalent to intros ? a ? b. Now it is still legal but equivalent to intros ?a ?b. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9964 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-09Improvements / Bug fixes for ROmega letouzey
----------------------------------- All romega tests in the test-suite are now bug-free. The only known remaining limitation of romega with respect to omega is that it cannot handle stuff on nat. * Equivalences A<->B are now understood by romega (as well as omega), and seen as (A->B)/\(B->A). There might be a smarter way to procede, for instance having a primitive Iff construct and trying to break equivalences as late as possible. * Conclusion-as-Pprop issue: After the resolution by the abstract omega machinery, useless parts are discarded from the reification process by replacing them with Pprop construct (see really_useful_prop). This allow to decrease the size of the proof terms and speed up their normalisation, I guess. But when such Pprop are created in the conclusion, this leads to failure, since concl is negated, and this is donc only if it is decidable. And introducing some Pprop might change the decidability status of the concl: for instance, Pfalse is decidable, whereas Pprop False is considered as _not_ decidable. Quick fix: no more really_useful_prop applied on concl (needs careful computation of useful_var). * NEGATE_CONTRADICT(_INV): This trace instrution comes in fact in two flavors, according to a boolean flag. We now translate to O_NEGATE_CONTRADICT_INV if this flag is false. (fix Besson's bug #1298) * EXACT_DIVIDE: could be used on NeqTerm and not only on EqTerm. * h_step indexes: The abstract omega machinery can introduce new hyps. In the list of hyps, they appears _before_ the regular one (but after the goal seen as an hyp by negating it). But the normalization steps were applied to regular hyps thanks to their indexes counted _before_ the addition extra hyps. * extra hyps (a)normal forms: extra hyps and variables are initially of the shape poly(v1,...,v(n-1)) = vn but O_STATE was expecting them in form 0 = poly(...) + -vn (by the way, SPLIT_INEQ should be checked someday). Since the above is one weekend's worth of debugging, there might well remain some more bugs :-(. For the record, here's the less painful way to debug a failed romega run: - activate debug flag in omega.ml and refl_omega.ml - at the bottom of refl_omega, replace normalise_vm_in_concl with convert_no_check (see comment there): this allow to skip the usually _huge_ error message about "Impossible to unify True with ..." - run the romega - try to run Qed, and enjoy the nice errror message about a (omega_tactic ? ? ? ?) that should be reducible to True. Here starts the real debug work... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9962 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-07If a fixpoint is not written with an explicit { struct ... }, then letouzey
all arguments are tried successively (from left to right) until one is found that satisfies the structural decreasing condition. When the system accepts a fixpoint, it now prints which decreasing argument was used, e.g: plus is recursively defined (decreasing on 1st argument) The search is quite brute-force, and may need to be optimized for huge mutual fixpoints (?). Anyway, writing explicit {struct} is always a possible fallback. N.B. in the standard library, only 4 functions have an decreasing argument different from the one that would be automatically infered: List.nth, List.nth_ok, List.nth_error, FMapPositive.xfind And compiling with as few explicit struct as possible would add about 15s in compilation time for the whole standard library. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9961 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-06a few works about my commits since Februaryletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9960 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-06minor bug correction (continuing r 9943)jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9956 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-06Update of theories/Numbers directory.emakarov
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9955 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 23:17:43 +0000