aboutsummaryrefslogtreecommitdiff
path: root/contrib/funind
AgeCommit message (Collapse)Author
2008-03-08correction d'un bug d'efficacite dans Function (+ ajout de eauto_with_bases)jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10640 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-22Merge with lmamane's private branch:lmamane
- New vernac command "Delete" - New vernac command "Undo To" - Added a few hooks used by new contrib/interface - Beta/incomplete version of dependency generation and dumping git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10580 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-17Add new LetPattern construct to replace dest. syntax: let| pat := t in b is ↵msozeau
backwards compatible. Update CHANGES with things i've done. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10446 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-09Correction of bug #1769jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10433 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-31Merged revisions ↵msozeau
10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,10398,10403-10408 via svnmerge from svn+ssh://msozeau@scm.gforge.inria.fr/svn/coq/branches/TypeClasses ........ r10358 | msozeau | 2007-12-10 15:42:53 +0100 (Mon, 10 Dec 2007) | 1 line Comment grammar error ........ r10359 | msozeau | 2007-12-10 16:04:09 +0100 (Mon, 10 Dec 2007) | 7 lines The initial Type Classes patch. This patch introduces type classes and instance definitions a la Haskell. Technically, it uses the implicit arguments mechanism which was extended a bit. The patch also introduces a notation for explicitely marking implicit, maximally inserted parameters. It includes the tactic redefinition code too (Ltac tac ::= foo redefines tac). ........ r10360 | msozeau | 2007-12-10 16:14:30 +0100 (Mon, 10 Dec 2007) | 1 line Fix interface ........ r10361 | msozeau | 2007-12-10 16:28:19 +0100 (Mon, 10 Dec 2007) | 1 line Fix more xlate code ........ r10362 | msozeau | 2007-12-11 02:00:53 +0100 (Tue, 11 Dec 2007) | 3 lines Update coqdoc for type classes, fix proof state not being displayed on Next Obligation. ........ r10365 | msozeau | 2007-12-11 14:22:35 +0100 (Tue, 11 Dec 2007) | 3 lines Bug fixes in Instance decls. ........ r10371 | msozeau | 2007-12-12 21:17:30 +0100 (Wed, 12 Dec 2007) | 3 lines Streamline typeclass context implementation, prepare for class binders in proof statements. ........ r10372 | msozeau | 2007-12-12 22:03:38 +0100 (Wed, 12 Dec 2007) | 1 line Minor cosmetic fixes: allow sorts as typeclass param instances without parens and infer more types in class definitions ........ r10373 | msozeau | 2007-12-13 00:35:09 +0100 (Thu, 13 Dec 2007) | 2 lines Better names in g_vernac, binders in Lemmas and Context [] to introduce a typeclass context. ........ r10377 | msozeau | 2007-12-13 18:34:33 +0100 (Thu, 13 Dec 2007) | 1 line Stupid bug ........ r10383 | msozeau | 2007-12-16 00:04:48 +0100 (Sun, 16 Dec 2007) | 1 line Bug fixes in name handling and implicits, new syntax for using implicit mode in typeclass constraints ........ r10384 | msozeau | 2007-12-16 15:53:24 +0100 (Sun, 16 Dec 2007) | 1 line Streamlined implementation of instances again, the produced typeclass is a typeclass constraint. Added corresponding implicit/explicit behaviors ........ r10394 | msozeau | 2007-12-18 23:42:56 +0100 (Tue, 18 Dec 2007) | 4 lines Various fixes for implicit arguments, new "Enriching" kw to just enrich existing sets of impl args. New syntax !a to force an argument, even if not dependent. New tactic clrewrite using a setoid typeclass implementation to do setoid_rewrite under compatible morphisms... very experimental. Other bugs related to naming in typeclasses fixed. ........ r10395 | msozeau | 2007-12-19 17:11:55 +0100 (Wed, 19 Dec 2007) | 3 lines Progress on setoids using type classes, recognize setoid equalities in hyps better. Streamline implementation to return more information when resolving setoids (return the results setoid). ........ r10398 | msozeau | 2007-12-20 10:18:19 +0100 (Thu, 20 Dec 2007) | 1 line Syntax change, more like Coq ........ r10403 | msozeau | 2007-12-21 22:30:35 +0100 (Fri, 21 Dec 2007) | 1 line Add right-to-left rewriting in class_setoid, fix some discharge/substitution bug, adapt test-suite to latest syntax ........ r10404 | msozeau | 2007-12-24 21:47:58 +0100 (Mon, 24 Dec 2007) | 2 lines Work on type classes based rewrite tactic. ........ r10405 | msozeau | 2007-12-27 18:51:32 +0100 (Thu, 27 Dec 2007) | 2 lines Better evar handling in pretyping, reorder theories/Program and add some tactics for dealing with subsets. ........ r10406 | msozeau | 2007-12-27 18:52:05 +0100 (Thu, 27 Dec 2007) | 1 line Forgot to add a file ........ r10407 | msozeau | 2007-12-29 17:19:54 +0100 (Sat, 29 Dec 2007) | 4 lines Generalize usage of implicit arguments in terms, up to rawconstr. Binders are decorated with binding info, either Implicit or Explicit for rawconstr. Factorizes code for typeclasses, topconstrs decorations are Default (impl|expl) or TypeClass (impl|expl) and implicit quantification is resolve at internalization time, getting rid of the arbitrary prenex restriction on contexts. ........ r10408 | msozeau | 2007-12-31 00:58:50 +0100 (Mon, 31 Dec 2007) | 4 lines Fix parsing of subset binders, bugs in subtac_cases and handling of mutual defs obligations. Add useful tactics to Program.Subsets. ........ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10410 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-06Plus de combinateurs sont passés de Util à Option. Le module Options aspiwack
devient Flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
lib/option.ml(i) . J'en profite pour rajouter des primitives de lifting des fonctions (à un ou deux arguments tous ou partie de type option). Il reste quelques opérations dans Util à propos desquelles je ne suis pas trop sûr, ou simplement que j'ai oublié, mais qui attendront demain car il est tard (comme some_in qui devrait devenir Option.make je suppose) . Elles s'expriment souvent facilement en fonction des autres, par exemple "option_compare x y" est égal à "Option.lift2 compare x y" . Le option_cons devrait faire son chemin dans le module parce qu'il est assez primitif et qu'il n'y a pas de fonction "cons" dans OCaml. J'en ai profité aussi pour remplacer les trop nombreux "failwith" par des erreurs locales au module, donc plus robustes. J'ai trouvé aussi une fonction qui était définie deux fois, et une définie dans un module particulier. Mon seul bémol (mais facile à traiter) c'est la proximité entre le nom de module Option et l'ancien Options. J'ai pas de meilleure idée de nom à l'heure qu'il est, ni pour l'un, ni pour l'autre. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10346 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-27bug correction in functional inversion principle generationjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10340 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-26minor bug correction in Functionjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10338 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-19Bug in functionnal induction principle generationjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10326 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-08Prise en compte des notations "alias" dans la globalisation des coercions.herbelin
Au passage, un peu plus de standardisation des noms de fonctions de globalisation Principe de base : locate_foo : qualid -> foo (échoue avec Not_found) global : reference -> global_reference (échoue avec UserError) global_of_foo : foo -> global_reference (échoue avec UserError) f_with_alias : se comporte comme f mais prenant aussi en compte les notations de la forme "Notation id:=ref" Principale exception : locate, au lieu de locate_global locate_global_with_alias, qui prend en entrée un "qualid located" Restent beaucoup de fonctions qui pourraient utiliser global_with_alias au lieu de global, notamment dans contribs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10305 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-30Cleaning code and comment.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10272 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-03Ajout de eelim, ecase, edestruct et einduction (expérimental).herbelin
Ajout de l'option with à (e)destruct et (e)induction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10169 85f007b7-540e-0410-9357-904b9bb8a0f7
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-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-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-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-05-20- Propagation des evars non résolues vers les with_bindings; permet par exempleherbelin
de résoudre des buts comme celui-ci : Record nat_retract : Type := {f1 : nat -> nat; f2 : nat -> nat; f1_o_f2 : forall x, f1 (f2 x) = x}. Goal nat_retract. exists (fun x => x) (fun x => x). - Nouvelle tentative d'utilisation des types des metas/evars pour inférer de nouvelles instances de metas/evars; permet par exemple d'utiliser f_equal sans option with, mais aussi, avec la modif précédente, de résoudre des buts tels que Goal exists f:bool->Prop, f true = True. exists (fun x => True). [Les expériences passées avaient montré qu'en prenant en compte les types dans l'unification, on peut unifier trop tôt une evars à une mauvaise sorte; à défaut de mécanisme de prise en compte des problème d'unification avec sous-typage, on s'est interdit ici d'unifier des types qui sont des arités.] - Tout les constr de tactic_expr deviennent des open_constr (même si seul with_bindings les accepte au final... c'est pas l'idéal). - Renommage env -> evd et templenv -> env dans clausenv. - Renommage closed_generic_argument -> typed_generic_argument. - Renommage closed_abstract_argument_type -> typed_abstract_argument_type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9842 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-17correction de bug dans Function et augmentation de la classe des fonctions ↵jforest
supportees git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9833 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-28Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.herbelin
Fusion des syntaxes de "apply" et "eapply". Ajout de "eapply in", "erewrite" et "erewrite in". Correction au passage des bugs #1461 et #1522). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9802 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-05Mise en place d'une nouvelle strategie plus efficace pour les preuves de ↵jforest
Function. => Changement d'ordre et de forme des obligations de preuve generees (pas de la semantique des obligations). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9746 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-19Add a parameter to QuestionMark evar kind to say it can be turned into an ↵msozeau
obligations (even an opaque one). Change cast_type to include the converted-to type or nothing in case of a Coerce cast, required much minor changes. Various little subtac changes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9718 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-16 r11153@tannat: jforest | 2007-03-16 10:25:55 +0100jforest
correction bug 1442 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9710 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-13Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé deherbelin
fonctionner entre la V7.3 et la V8.0 (notation : "@ ?meta id1 ... idn") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9644 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-12Bug mineur dans la generation des principes d'induction pour Functionjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9643 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-11Correction d'un bug dans la génération des principes d'inductionjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9639 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-09Retour r9310 en attendant mieuxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9629 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-07Meilleur anglais (cf 9619)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9620 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-26Contounement d'un probleme avec la VM dans Function jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9538 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-19Protection contre les warnings 'unused variable' de ocaml 3.09herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9502 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-24Functional graph merging deals with letins.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9404 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-24Fixed the graph merging parameter order.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9403 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-23Fixing syntax and parameter order in functional graph merging.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9401 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-20Changing merging functional scheme syntax.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9395 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-16Small fix in functional graph merging.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9383 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-13Correction de la seconde partie du bug #1278jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9373 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-13Correction de la premiere partie du #1278 (but non referme en cas d'echec)jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9372 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-28Extension du polymorphisme de sorte au cas des définitions dans Type.herbelin
(suppression au passage d'un cast dans constant_entry_of_com - ce n'est pas normal qu'on force le type s'il n'est pas déjà présent mais en même temps il semble que ce cast serve pour rafraîchir les univers algébriques...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9310 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-28Fixes in experimental merging of functional graphs.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9305 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-27Fixes on functional graphs merging: put functional results at the endcourtieu
of args. Still a bug with parameters. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9300 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-27Fixes on functional graphs merging: removed debug printing.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9296 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-27Fixes on functional graphs merging: names of constructors.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9295 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-26Some fixes in experimental merging of two functional graphs. courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9287 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-26Experimental merging of two functional graphs.courtieu
temporary synatx: Mergeschemes (G1 a b c) with (G2 a d e) using G1G2. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9285 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-20Starting to add a function schemes merging command (not finished, notcourtieu
activated). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9251 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-13 r9778@tannat: jforest | 2006-10-13 11:36:37 +0200jforest
Changement de nom des lemme de correction/completude des Functions vis a vis de leur graphes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9236 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-27Detection des paramettres pour les Functions bien fondeesjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9182 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-20Declarative Proof Language: main commitcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-19Gestion des arguments implicites dans les Functions bien fondeesjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9152 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-18correction of bug #1220jforest
adding a "using" optional argument to Function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9150 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 13:58:49 +0000