aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Collapse)Author
2007-09-15* Adding compability with ocaml 3.10 + camlp5 (rework of letouzey
the patch by S. Mimram) * for detecting architecture, also look for /bin/uname * restore the compatibility of kernel/byterun/coq_interp.c with ocaml 3.07 (caml_modify vs. modify). There is still an issue with this 3.07 and 64-bits architecture (see coqdev and a future bug report). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10122 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-14Correction du bug #1679 (congruence) et ajout test-suitecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10120 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-06errors in recdef.ml4:bertot
a few errors of parentheses around fun x -> ... constructs, a use of tclTHEN was left over from bug tracking modifications, it was badly parenthesized. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10117 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-06this should fix a problem described in a message by Dufourd on July 30th, 2007bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10116 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-31fin de la correction de Functionjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10108 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-31correction bug d'efficacite dans Functionjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10107 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-30Oubli dans commit 10102...herbelin
+ Formattage affichage arguments evars. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10104 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-29- Débogueur: positionnement de set_detype_anonymous pour ne pasherbelin
échouer sur les Rel liées a des Anonymous et export de l'instance des evars vers le printeur du débogueur. - Suppression d'un reste de code mort lié à la V7 dans pretyping.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10102 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-27Oubli dans la révision 10098 (nettoyage body_of_type)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10099 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-27Suppression des type_app et body_of_type qui alourdissent inutilement le codeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10098 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-26Fix bug on wellfounded defs with constant parameters and dependencies on the ↵msozeau
rec argument, example given by Brian Aydemir. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10097 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-26Fix de Bruijn bug in wf definitions.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10096 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-26Fix evars bug in mutual fixpoints with implicit types and bug in ↵msozeau
inequalities generation for multiple patterns. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10094 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-16Correction du bug #1680: ajout d'un champ avoid_ids dans interp_sign;notin
modification de interp_ltac_reference pour passer les ids utilisées dans le contexte d'appel d'une tactique. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10076 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-08Fix dependency bugs due to Program modules renamings.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10064 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-07Move Program tactics into a proper theories/ directory as they are general ↵msozeau
purpose and can be used directly be the user. Document them. Change Prelude to disambiguate an import of a Tactics module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10060 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-24fixed bug 1448 and 1674barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10046 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-24fixed bug 1675: computing carrier from the relation type was not rightbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10043 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-24Declarative language: fixed the generation of fixpoints for induction proofs.corbinea
Cleaner code: the guardedness bug is now corrected. Added "trivial" to the automation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10042 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-19Documentation of Program and its tactics, fix enormous interaction bug due ↵msozeau
to bad cache handling. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10032 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-18A generic preprocessing tactic zify for (r)omegaletouzey
------------------------------------------------ See file PreOmega for more details and/or test-suite/succes/*Omega*.v The zify tactic performs a Z-ification of your current goal, transforming parts of type nat, N, positive, taking advantage of many equivalences of operations, and of the positivity implied by these types. Integration with omega and romega: (r)omega : the earlier tactics, 100% compatible (r)omega with * : full zify applied before the (r)omega run (r)omega with <types>, where <types> is a sub-list of {nat,N,positive,Z}, applies only specific parts of zify (btw "with Z" means take advantage of Zmax, Zmin, Zabs and Zsgn). As a particular consequence, "romega with nat" should now be a close-to-perfect replacement for omega. Slightly more powerful, since (forall x:nat, x*x>=0) is provable and also slightly less powerful: if False is somewhere in the hypothesis, it doesn't use it. For the moment zify is done in a direct way in Ltac, using rewrite when necessary, but crucial chains of rewrite may be made reflexive some day. Even though zify is designed to help (r)omega, I think it might be of interest for other tactics (micromega ?). Feel free to complete zify if your favorite operation / type isn't handled yet. Side-effects: - additional results for ZArith, NArith, etc... - definition of Ple, Plt, Pgt, Pge and notations for them in positive_scope - romega now start by doing "intros". Since the conclusion will be negated, and this operation will be justified by means of decidability, it helps to have as little as possible in the conclusion. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10028 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-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-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-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-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-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-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-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-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-06Adding a syntax for "n-ary" rewrite: letouzey
rewrite H, H' means: rewrite H; rewrite H'. This should still be compatible with other "features" of rewrite: like orientation, implicit arguments (t:=...), and "in" clause. Concerning the "in" clause, for the moment only one is allowed at the very end of the tactic, and it applies to all the different rewrites that are done. For instance, if someone _really_ wants to use all features at the same time: rewrite H1 with (t:=u), <-H2, H3 in * means: rewrite H1 with (t:=u) in *; rewrite <- H2 in *; rewrite H3 in * git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9954 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-06sequel to commit 9952: forgot to adapt xlate to the new n-ary renameletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9953 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-06extension of the rename tactic: the following is now allowed: letouzey
rename A into B, C into D, E into F. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9952 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-06New intro pattern "@A", which generates a fresh name based on A.glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9950 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-05Minor bug correction in Function. Non terminating Function e.g. jforest
Function f (x:A) { wf R x} := f x. was not accepted. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9943 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-02Better handling of aliases, add command to solve a particular obligation.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9929 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-26killing some more non-exhaustive patternsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9912 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-21Correction de plusieurs bugs de l'export XML (utilisation d'un type deherbelin
constante par defaut pour les nouveaux types plutot qu'echouer; avertissement plutot qu'echec en cas de foncteur; nommage systematique des LetIn -- p.ex. functional induction engendre des LetIn non nommes --; branchement de la fonction de normalisation de tete evitant CProp sur Closure au lieu de Tacred afin de garantir la f.n. de tete) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9902 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-14Add Solve All Obligations command, fix bug in inequality generation ↵msozeau
introduced by previous commit, add general purpose tactics for destructing existentials and disjunctions. Compiles without camlp4 warnings too. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9888 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-09Various Program fixes, multiple pattern matches, aliases. Fix bug in ↵msozeau
coercion code for simultaneous coercion of different arguments of an inductive type. Add tactics for dealing with heterogeneous equality. Export more error reporting functions from Cases. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9886 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-07Extension of NArith: Nminus, Nmin, etcletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9883 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-07Unification des types + clause filtrage manquante + uniformisation localeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9879 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-25Modification of VernacScheme to handle a new scheme: Equality (equality invsiles
boolean, will be added later) and update so everything is fine with the new syntax. New Type: type scheme = | InductionScheme of bool * lreference * sort_expr | EqualityScheme of lreference ... | VernacScheme of (lident * scheme) list git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9860 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-24fixed (PR#1483)corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9857 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 09:37:08 +0000