aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
Commit message (Collapse)AuthorAge
* Accept more Unicode symbolsGravatar glondu2009-06-10
| | | | | | The comment just below makes me think this is just a typo... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12180 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceGravatar herbelin2009-05-09
| | | | | | | | | | | | | as hints (see wish #2104). - New type hint_entry for interpreted hint. - Better centralization of functions dealing with evaluable_global_reference. - Unfortunately, camlp4 does not factorize rules so that "Hint Resolve" had uglily to be factorized by hand. - Typography in RefMan-tac.tex. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12121 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Cleaning (unification of ML names, removal of obsolete code,Gravatar herbelin2009-04-27
| | | | | | | | | | | | | reorganization of code) and documentation (in pcoq.mli) of the code for parsing extensions (TACTIC/VERNAC/ARGUMENT EXTEND, Tactic Notation, Notation); merged the two copies of interp_entry_name to avoid they diverge. - Added support in Tactic Notation for ne_..._list_sep in general and for (ne_)ident_list(_sep) in particular. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12108 85f007b7-540e-0410-9357-904b9bb8a0f7
* comparison functions on lists and arraysGravatar barras2009-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12091 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
| | | | | | | | | | | | | | This commit concerns about the first half of the useless code mentionned by Oug for coqtop (without plugins). For the moment, Oug is used in a mode where any elements mentionned in a .mli is considered to be precious. This already allows to detect and remove about 600 lines, and more is still to come. Among the interesting points, the type Entries.specification_entry and its constructors SPExxx were never used. Large parts of cases.ml (and hence subtac_cases.ml) were also useless. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12069 85f007b7-540e-0410-9357-904b9bb8a0f7
* A first pearl found by the Oug analyzer: there were two list_map_i in UtilGravatar letouzey2009-04-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12060 85f007b7-540e-0410-9357-904b9bb8a0f7
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20
| | | | | | | | | | | | | | | | | | | | | | | | * generalize the use of .mllib to build all cma, not only in plugins/ * the .mllib in plugins/ now mention Bruno's new _mod.ml files * lots of .cmo enumerations in Makefile.common are removed, since they are now in .mllib * the list of .cmo/.cmi can be retreive via a shell script line, see for instance rule install-library * Tolink.core_objs and Tolink.ide now contains ocaml _modules_, not _files_ * a -I option to coqdep_boot allows to control piority of includes (some files with the same names in kernel and checker ...) This is quite a lot of changes, you know who to blame / report to if something breaks. ... and last but not least I've started playing with ocamlbuild. The myocamlbuild.ml is far from complete now, but it already allows to build coqtop.{opt,byte} here. See comments at the top of myocamlbuild.ml, and don't hesitate to contribute, either for completing or simplifying it ! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12002 85f007b7-540e-0410-9357-904b9bb8a0f7
* Timeout message was not always displayedGravatar barras2009-03-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11960 85f007b7-540e-0410-9357-904b9bb8a0f7
* Heavy modifications on the widget and edition tab creation mechanism.Gravatar vgross2009-03-02
| | | | | | | | Overloading of GPack.notebook => Vector no longer needed git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11952 85f007b7-540e-0410-9357-904b9bb8a0f7
* Gestion des espaces dans les noms + guess_coqlib sous WindowsGravatar notin2009-02-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11921 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix d'un problème lors de l'appel à coqtop avec un chemin relatifGravatar notin2009-02-11
| | | | | | (cherry picked from commit 76796fca17ec7763b1301b0dd22c07ddc92983fc) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11917 85f007b7-540e-0410-9357-904b9bb8a0f7
* memoized is_ground_envGravatar barras2009-02-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11893 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixed various Overfull in documentation.Gravatar herbelin2009-01-27
| | | | | | | | | | - Removed useless coq-tex preprocessing of RecTutorial. - Make "Set Printing Width" applies to "Show Script" too. - Completed documentation (specially of ltac) according to CHANGES file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11863 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petit nettoyage faisant suite au commit #11847 .Gravatar aspiwack2009-01-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | Quelques modifications autour (géographiquement) de Util.list_split_at Util.list_split_at devient Util.list_split_when (dénomination inventée arbitrairement par moi-même, mais qui ne devrait pas déranger grand monde vu qu'il semble n'y avoir que deux occurences de cette fonction). Pour laisser la place à la fonction suivante : Introduction de Util.list_split_at: qui sépare la liste à une position donnée (alors que la nouvellement nommé list_split_when sépare à la première occurence "vrai" d'un prédicat). Ajout de quelques commentaires dans util.ml (pas le mli) sur ces deux fonctions. Suppression de Impargs.list_split_at (appel à Util). Suppression de Subtac_pretyping.list_split_at (qui était du code mort de toute façon). Suppression Util.list_split_by qui n'est utilisé nulle part et est une réimplémentation de List.partition (qui est probablement meilleure, en particulier tail-recursive) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11851 85f007b7-540e-0410-9357-904b9bb8a0f7
* Util.split_at : for quadratic to linear complexityGravatar letouzey2009-01-22
| | | | | | | | This function is probably used only on small lists, but it's not a reason to let it be quadratic... I'm wondering how many other inefficient functions like this one may exist in the source of Coq. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11847 85f007b7-540e-0410-9357-904b9bb8a0f7
* Experimental file commited by mistake, sorry.Gravatar herbelin2009-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11806 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backporting from v8.2 to trunk:Gravatar herbelin2009-01-18
| | | | | | | | | | - Filtering of doc compilation messages (11793,11795,11796). - Fixing bug #1925 and cleaning around bug #1894 (11796, 11801). - Adding some tests. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11802 85f007b7-540e-0410-9357-904b9bb8a0f7
* DISCLAIMERGravatar puech2009-01-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ========== This big patch is commited here with a HUGE experimental tag on it. It is probably not a finished job. The aim of committing it now, as agreed with Hugo, is to get some feedback from potential users to identify more clearly the directions the implementation could take. So please feel free to mail me any remarks, bug reports or advices at <puech@cs.unibo.it>. Here are the changes induced by it : For the user ============ * Search tools have been reimplemented to be faster and more general. Affected are [SearchPattern], [SearchRewrite] and [Search] (not [SearchAbout] yet). Changes are: - All of them accept general constructions, and previous syntactical limitations are abolished. In particular, one can for example [SearchPattern (nat -> Prop)], which will find [isSucc], but also [le], [gt] etc. - Patterns are typed. This means that you cannot search mistyped expressions anymore. I'm not sure if it's a good or a bad thing though (especially regarding coercions)... * New tool to automatically infer (some) Record/Typeclasses instances. Usage : [Record/Class *Infer* X := ...] flags a record/class as subject to instance search. There is also an option to activate/deactivate the search [Set/Unset Autoinstance]. It works by finding combinations of definitions (actually all kinds of objects) which forms a record instance, possibly parameterized. It is activated at two moments: - A complete search is done when defining a new record, to find all possible instances that could have been formed with past definitions. Example: Require Import List. Record Infer Monoid A (op:A->A->A) e := { assoc : forall x y z, op x (op y z) = op (op x y) z; idl : forall x, x = op x e ; idr : forall x, x = op e x }. new instance Monoid_autoinstance_1 : (Monoid nat plus 0) [...] - At each new declaration (Definition, Axiom, Inductive), a search is made to find instances involving the new object. Example: Parameter app_nil_beg : forall A (l:list A), l = nil ++ l. new instance Build_Monoid_autoinstance_12 : (forall H : Type, Monoid (list H) app nil) := (fun H : Type => Build_Monoid (list H) app nil ass_app (app_nil_beg H) (app_nil_end H)) For the developper ================== * New yet-to-be-named datastructure in [lib/dnet.ml]. Should do efficient one-to-many or many-to-one non-linear first-order filtering, faster than traditional methods like discrimination nets (so yes, the name of the file should probably be changed). * Comes with its application to Coq's terms [pretyping/term_dnet.ml]. Terms are represented so that you can search for patterns under products as fast as you would do not under products, and facilities are provided to express other kind of searches (head of application, under equality, whatever you need that can be expressed as a pattern) * A global repository of all objects defined and imported is maintained [toplevel/libtypes.ml], with all search facilities described before. * A certain kind of proof search in [toplevel/autoinstance.ml]. For the moment it is specialized on finding instances, but it should be generalizable and reusable (more on this in a few months :-). The bad news ============ * Compile time should increase by 0 to 15% (depending on the size of the Requires done). This could be optimized greatly by not performing substitutions on modules which are not functors I think. There may also be some inefficiency sources left in my code though... * Vo's also gain a little bit of weight (20%). That's inevitable if I wanted to store the big datastructure of objects, but could also be optimized some more. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11794 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove trailing newlines in outputs of X -whereGravatar glondu2009-01-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11768 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made the debugger work again:Gravatar herbelin2009-01-02
| | | | | | | | | | | | | | - call to open_process_full from Envars.camlp4lib was apparently disturbing stdin/stdout/stderr and precipitating coqtop.byte death in ocamldebug; renounced to add camlp4 to the ml path (why was it useful?) which was the reason for calling camlp4lib (seems like camlp4lib is now useless), - Envars was needing str.cma which was missing when calling printers.cma; renounced to use str.cma since its only use was for an elementary split function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11734 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixed bugs and compatibilities issues in Gravatar herbelin2008-12-30
| | | | | | | | | | match_conjunction/match_disjunction/array_for_all_i - Finally activate fine-tuned unfolding of iff in tauto: it breaks at only one place in the user contribs (FSetAVL_dep.v). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11726 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Another bug in get_sort_family_of (sort-polymorphism of constants andGravatar herbelin2008-12-28
| | | | | | | | | | | | | | | | | | | | | | | inductive types was not taken into account). - Virtually extended tauto to - support arbitrary-length disjunctions and conjunctions, - support arbitrary complex forms of disjunctions and conjunctions when in the contravariant of an implicative hypothesis, - stick with the purely propositional fragment and not apply reflexivity. This is virtual in the sense that it is not activated since it breaks compatibility with the existing tauto. - Modified the notion of conjunction and unit type used in hipattern in a way that is closer to the intuitive meaning (forbid dependencies between parameters in conjunction; forbid indices in unit types). - Investigated how far "iff" could be turned into a direct inductive definition; modified tauto.ml4 so that it works with the current and the alternative definition. - Fixed a bug in the error message from lookup_eliminator. - Other minor changes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11721 85f007b7-540e-0410-9357-904b9bb8a0f7
* - coq_makefile: target install now respects the original tree structureGravatar herbelin2008-12-24
| | | | | | | | | | | | | of the archive to install in coq user-contrib installation directory. - Relaxed the validity check on identifiers from an error to a warning. - Added a filtering option to Print LoadPath. - Support for empty root in option -R. - Better handling of redundant paths in ml loadpath. - Makefile's: Added target initplugins and added initplugins to coqbinaries. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11713 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage des variables Coq et amélioration de coqmktop. LesGravatar notin2008-12-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | principaux changements sont: - coqtop (et coqc) maintenant insensible aux variables d'environnement COQTOP, COQBIN et COQLIB; le chemin vers les librairies Coq peut être spécifié par l'option -coqlib - coqmktop prend 4 nouvelles options: -boot, -coqlib, -camlbin et -camlp4bin; en mode boot, coqmktop se réfère à Coq_config pour les chemins des exécutables OCaml; en dehors du mode boot, coqmktop cherche les exécutables OCaml dans PATH - installation des *.cmxs *.o et *.a en plus des *.cm[ioxa]; ceux-ci étant installé en copiant l'architecture des sources (ie lib.cmxa est installé dans COQLIB/lib/lib.cmxa) - coq_makefile prend maintenant 3 paramètres sous forme de variables d'environnement: COQBIN pour dire où trouver les exécutables Coq, CAMLBIN et CAMLP4BIN pour les exécutables OCaml et Camlp4/5; les chemins vers les librairies sont déduits en utilisant -where Le tout a testé avec Ssreflect (cf coq-contribs) en essayant de simuler les conditions de la vie réelle (Ocaml pas dans le PATH, installation binaire relocalisée, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11707 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add some unicode symbols from japanese CJC (request by Y. Regis-Gianas)Gravatar letouzey2008-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11683 85f007b7-540e-0410-9357-904b9bb8a0f7
* eventually fixing r11612Gravatar barras2008-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11626 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bug in VernacExtend printing + missing vernacular printing rules +Gravatar herbelin2008-11-22
| | | | | | | | | | 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
* - Fixed minor bug #1994 in the tactic chapter of the manual [doc]Gravatar herbelin2008-11-22
| | | | | | | | | | | | | - 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
* fixed problem with r11612Gravatar barras2008-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11614 85f007b7-540e-0410-9357-904b9bb8a0f7
* Better extraction renaming phase (fix #1914 plus other non-reported bugs)Gravatar letouzey2008-11-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Adaptation to ocaml 3.11 new semantics of String.index_from (see bug #1974)Gravatar herbelin2008-11-04
| | | | | | | 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
* - Fixed many "Theorem with" bugs.Gravatar herbelin2008-10-27
| | | | | | | | | | | - Fixed doc of assert as. - Doc of apply in + update credits. - Nettoyage partiel de Even.v en utilisant "Theorem with". - Added check that name is not in use for "generalize as". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11511 85f007b7-540e-0410-9357-904b9bb8a0f7
* Open notation for declaring record instances.Gravatar msozeau2008-10-23
| | | | | | | | | | | | | | | | | | | | It solves feature request 1852, makes me and Arnaud happy and will permit to factor some more code in typeclasses. - Records are introduced using the syntax "{| x := t; y := foo |}" and "with" clauses are currently parsed but not yet supported in the elaboration. You are invited to suggest other syntaxes :) - Missing fields are turned into holes, extra fields cause an error message. The current implementation finds the type of the record at pretyping time, from the typing constraint alone (and just expects an inductive with one constructor). It is then impossible to use scope information to parse the bodies: that may be wrong. The other solution I see is using the fields to detect the type earlier, before internalisation of the bodies, but then we get in name clash hell. - In funind/contrib/interface I mostly put [assert false] everywhere to avoid warnings. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11496 85f007b7-540e-0410-9357-904b9bb8a0f7
* Affichage des notations récursives:Gravatar herbelin2008-10-22
| | | | | | | | | | | | | - Prise en compte des notations applicatives - Remplacement du codage des arguments liste des notations récursives sous forme de terme par une représentation directe (permet notamment de résoudre un problème de stack overflow de la fonction d'affichage) + Correction bug affichage Lemma dans ppvernac.ml + Divers util.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11489 85f007b7-540e-0410-9357-904b9bb8a0f7
* avoid small overflowsGravatar barras2008-09-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11346 85f007b7-540e-0410-9357-904b9bb8a0f7
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Correction divers messages d'erreur - lorsque rien à réécrire dans une hyp, - lorsqu'une variable ltac n'est pas liée, - correction anomalie en présence de ?id dans le "as" de induction, - correction mauvais env dans message d'erreur de unify_0. - Diverses extensions et améliorations - "specialize" : - extension au cas (fun x1 ... xn => H u1 ... un), - renommage au même endroit. - "assert" et "pose proof" peuvent réutiliser la même hyp comme "specialize". - "induction" - intro des IH toujours au sommet même si induction sur var quantifiée, - ajout d'un hack pour la reconnaissance de schémas inductifs comme N_ind_double mais il reste du boulot pour reconnaître (et/ou réordonner) les composantes d'un schéma dont les hypothèses ne sont pas dans l'ordre standard, - vérification de longueur et éventuelle complétion des intropatterns dans le cas de sous-patterns destructifs dans induction (par exemple "destruct n as [|[|]]" sur "forall n, n=0" ne mettait pas le n dans le contexte), - localisation des erreurs d'intropattern, - ajout d'un pattern optionnel après "as" pour forcer une égalité et la nommer (*). - "apply" accepte plusieurs arguments séparés par des virgules (*). - Plus de robustesse pour clear en présence d'evars. - Amélioration affichage TacFun dans Print Ltac. - Vieux pb espace en trop en tête d'affichage des tactiques EXTEND résolu (incidemment, ça remodifie une nouvelle fois le test output Fixpoint.v !). - Fusion VTactic/VFun dans l'espoir. - Mise en place d'un système de trace de la pile des appels Ltac (tout en préservant certains aspects de la récursivité terminale - cf bug #468). - Tactiques primitives - ajout de "move before" dans les tactiques primitives et ajout des syntaxes move before et move dependent au niveau utilisateur (*), - internal_cut peuvent faire du remplacement de nom d'hypothèse existant, - suppression de Intro_replacing et du code sous-traitant - Nettoyage - Suppression cible et fichiers minicoq non portés depuis longtemps. (*) Extensions de syntaxe qu'il pourrait être opportun de discuter git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11300 85f007b7-540e-0410-9357-904b9bb8a0f7
* Now, -browser option is effective (and compiles)Gravatar glondu2008-07-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11273 85f007b7-540e-0410-9357-904b9bb8a0f7
* (Partially) Revert previous commit because of FTBFSGravatar glondu2008-07-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11272 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add -browser option to configure scriptGravatar glondu2008-07-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11271 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite commit 11236Gravatar notin2008-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11252 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from ↵Gravatar notin2008-07-18
| | | | | | de coqdoc (compatibilité) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11236 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quelques modifications autour du filtrage Ltac:Gravatar herbelin2008-07-16
| | | | | | | | | | | | | | | | | - Optimisation du filtrage sous-terme de Ltac (cf sub_match) pour le cas où c'est le n-ième sous-termes qui finalement réussit (passage à une complexité en n plutôt que n^2, via l'utilisation de continuations). - Sémantique du filtrage: suppression dans sub_match de la recherche dans le type des let (puisque ce n'est pas cencé être une information utilisateur) mais rajout de la recherche dans le champ cast qui lui est utilisateur. - Nouvelle fonctionnalité: récupération des noms des variables liantes filtrées (dans matches/sub_match) et utilisation de ces noms dans ltac (utile pour récupérer x dans "exists x, P x"); git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11226 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes in handling of implicit arguments:Gravatar msozeau2008-07-04
| | | | | | | | | | | | | - Now [ id : Class foo ] makes id an explicit argument, and [ Class foo ] is equivalent to [ {someid} : Class foo ]. This makes declarations such as "Class Ord [ eq : Eq a ]" have sensible implicit args. - Better handling of {} in class and record declarations, refactorize code for declaring structures and classes. - Fix merging of implicit arguments information on section closing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11204 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fichiers oubliés lors du 11188 :-(Gravatar herbelin2008-06-30
| | | | | | | | | On en profite pour faire dépendre l'avertissement de where_in_path du mode silencieux. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11193 85f007b7-540e-0410-9357-904b9bb8a0f7
* Création du fichier dumpglob.ml, qui rassemble les fonctions de ↵Gravatar notin2008-06-25
| | | | | | globalisation (add_glob* et dump_*) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11177 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de l'option -dump-glob et ajout d'une option -no-globGravatar notin2008-06-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11167 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Correction de la version simplifiée (filtrage sur deux sigGravatar herbelin2008-06-09
| | | | | | | | | | imbriqués) du bug 1834, mais le bug 1834 reste ouvert [cases.ml]. - Réactivation de l'interprétation des listes dans "generalize" cassée depuis 11072) [tacinterp.ml]. - Bricoles et petit nettoyage en passant [cases.ml et g_vernac.ml4]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11083 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Documentation de admit et Print Assumptions.Gravatar herbelin2008-06-09
| | | | | | | | | | | | - Relecture, mise à jour, correction d'erreurs et petite réorganisation du chapitre sur les commandes vernaculaires. - Correction bug #1865 (rafraichissement des univers algébriques). - Suppression de la dépendance du initial.coq en les noms longs des fichiers de façons à ce que les dépendances ne soient que purement logique. - Encore un (petit) bug undo ide. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11077 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
| | | | | | | | | | | | | | | | | - Ajout clause "in" à "remember" (et passage du code en ML). - Ajout clause "in" à "induction"/"destruct" qui, en ce cas, ajoute aussi une égalité pour se souvenir du terme sur lequel l'induction ou l'analyse de cas s'applique. - Ajout "pose t as id" en standard (Matthieu: j'ai enlevé celui de Programs qui avait la sémantique de "pose proof" tandis que le nouveau a la même sémantique que "pose (id:=t)"). - Un peu de réorganisation, uniformisation de noms dans Arith, et ajout EqNat dans Arith. - Documentation tactiques et notations de tactiques. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11072 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction terminologie et ajout plage unicode 1D400-1D7FF (mathematicalGravatar herbelin2008-06-06
| | | | | | | | | alphanumerical symbols) suite à remarques de Arnaud. Correction bugs d'affichage de l'option -translate. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11059 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-06 14:44:57 +0000