aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* simplification in deps of some g_*.ml4Gravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15377 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pattern as a mli-only file, operations in PatternopsGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15376 85f007b7-540e-0410-9357-904b9bb8a0f7
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15375 85f007b7-540e-0410-9357-904b9bb8a0f7
* Glob_term now mli-only, operations now in Glob_opsGravatar letouzey2012-05-29
| | | | | | Stuff about reductions now in genredexpr.mli, operations in redops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15374 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tacexpr as a mli-only, the few functions there are now in TacopsGravatar letouzey2012-05-29
| | | | | | | NB: former Tacexpr.no_move is now Tacexpr.MoveLast (when introducing, intro with no move is intro as last) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15373 85f007b7-540e-0410-9357-904b9bb8a0f7
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
| | | | | | | | | Corresponding operations in locusops.ml and miscops.ml The type of occurrences is now a clear algebraic one instead of a bool*list hard to understand. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15372 85f007b7-540e-0410-9357-904b9bb8a0f7
* Evar_kinds.mli containing former Evd.hole_kind, avoid deps on EvdGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15371 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile.build: a rule for building grammar.dotGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15370 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pfedit: two superfluous openGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15369 85f007b7-540e-0410-9357-904b9bb8a0f7
* Decl_kinds becomes a pure mli file, remaining ops in new file kindops.mlGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15368 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vernacexpr is now a mli-only file, locality stuff now in locality.mlGravatar letouzey2012-05-29
| | | | | | Adds a directory ./intf for pure interfaces. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15367 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: avoid too much exported vars (for win32)Gravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15366 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bugs revealed by playing with contribsGravatar pboutill2012-05-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15364 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix r15259 to get rid of bug 2783Gravatar pboutill2012-05-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15363 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed #2769.Gravatar ppedrot2012-05-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15362 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed #2789.Gravatar ppedrot2012-05-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15360 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rewritten the handling of coq sentence processing, hopefully beingGravatar ppedrot2012-05-23
| | | | | | | | smarter and more asynchronous-friendly. Some aditional cleaning is needed to factorize other parts of the code, but this is a first milestone. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15359 85f007b7-540e-0410-9357-904b9bb8a0f7
* CHANGES: fix a typo + an entry in the wrong sectionGravatar letouzey2012-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15357 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed #2538 by adding an option to reset coqtop on tab switch, as suggested.Gravatar ppedrot2012-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15355 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaned prerr_endline use.Gravatar ppedrot2012-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15354 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert copy/pasted function in to minilib thanks to clib.cmaGravatar pboutill2012-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15352 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed #2782.Gravatar ppedrot2012-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15351 85f007b7-540e-0410-9357-904b9bb8a0f7
* configure: camlp4 is now tried when camlp5 isn't foundGravatar letouzey2012-05-23
| | | | | | | | | * When both camlp4 and camlp5 are installed, camlp5 is used by default, except when -usecamlp4 flag is given to ./configure. * Otherwise, ./configure pick automatically the available camlpX git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15349 85f007b7-540e-0410-9357-904b9bb8a0f7
* configure: add support of MinGW Win32 environment (fix #2526)Gravatar letouzey2012-05-23
| | | | | | | | | | | | | | * Since MinGW/Msys doesn't provide a cygpath utility, we emulate it via an ocaml script tools/mingwpath.ml * Avoid the crazy sed portions for backslash escaping, instead use a more robust ocaml script tools/escape_string.ml based on String.escaped * No more config/Makefile.template + sed on it, but rather a "cat << EOF > ..." as for config/coq_config.ml * Normally, support of Cygwin should be preserved, as well as mingw32 cross-compilation from linux (cf. myocamlbuild.ml) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15348 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reducing CoqIDE start option queries.Gravatar ppedrot2012-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15344 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minilib: Always add the Coq_config.dirs to xdg_dirs (again)Gravatar letouzey2012-05-22
| | | | | | Sorry, my last commit in Minilib annihilated by mistake commit 15265. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15342 85f007b7-540e-0410-9357-904b9bb8a0f7
* Permutation: remove a compatibility notation which doesn't help MathClassesGravatar letouzey2012-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15341 85f007b7-540e-0410-9357-904b9bb8a0f7
* SetoidList: explicit the fact that InfA_compat won't use ltA_strorderGravatar letouzey2012-05-22
| | | | | | | | For that, we use the new "Proof using ...". This way, we're sure that a later change in the behavior of intuition or any other tactics will not create an artificial dependency again (cf. r15180). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15340 85f007b7-540e-0410-9357-904b9bb8a0f7
* List + Permutation : more results about nth_error and nthGravatar letouzey2012-05-18
| | | | | | | | | | In particular, characterisation of NoDup and Permutation in term of nth_error and nth Some of these results have been suggested last year by Bas Spitters (cf. MathClasses). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15336 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bug #2781... (We hope so.)Gravatar ppedrot2012-05-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15335 85f007b7-540e-0410-9357-904b9bb8a0f7
* Trying to fix bug #2780, by short-circuiting the Gtk signals. A bit hackish.Gravatar ppedrot2012-05-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15334 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: make some paths win32-compliantGravatar letouzey2012-05-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15332 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert commit 15287 : the env variables are indeed access at launch-timeGravatar letouzey2012-05-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15331 85f007b7-540e-0410-9357-904b9bb8a0f7
* Intuition: temporary(?) restore the unconditional unfolding of notGravatar letouzey2012-05-15
| | | | | | | | Let's check tomorrow the impact on contribs: are the recent build failures related to the "not" unfolding stategy or to the new handling of conjonction-like constructors ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15330 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: minor formatting improvement of an error messageGravatar letouzey2012-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15329 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: in win32 command given to cmd.exe should be more quotedGravatar letouzey2012-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15328 85f007b7-540e-0410-9357-904b9bb8a0f7
* when cross-compiling with mingw32, let's fix the Filename.dir_sepGravatar letouzey2012-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15327 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: Really avoid locales in $(DATE)Gravatar letouzey2012-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15326 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: display initial connection errors in popups instead of on stderrGravatar letouzey2012-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15325 85f007b7-540e-0410-9357-904b9bb8a0f7
* Notations are back in the "in" clause of pattern matching.Gravatar pboutill2012-05-15
| | | | | | Fixes the test-suite. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15324 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added semantic completion in CoqIDE. (Should also add an option for that...)Gravatar ppedrot2012-05-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15317 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tweaking options of CoqIDE.Gravatar ppedrot2012-05-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15316 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some cosmetic changes w.r.t. the previous commit.Gravatar ppedrot2012-05-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15315 85f007b7-540e-0410-9357-904b9bb8a0f7
* Heavily rewritten the coqtop management process of coqide. The coqtopGravatar ppedrot2012-05-13
| | | | | | | | | | object is now responsible for restarting itself, and handles unexpected crashes. Fixes a lot of errors in file descriptor management, but may introduce lurking deadlocks and nasty bugs waiting to be discovered. Only (quickly) tested under Linux, any callbacks from Windows are welcome. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15314 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a SearchAbout-like primitive in coqtop interface.Gravatar ppedrot2012-05-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15313 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added an interface primitive to ask coqtop for its internal versions.Gravatar ppedrot2012-05-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15312 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vectors takes advantage of pattern matching compiler fixupGravatar pboutill2012-05-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15308 85f007b7-540e-0410-9357-904b9bb8a0f7
* Impossible branches inference fixup (bug 2761)Gravatar pboutill2012-05-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15307 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile.build typo in echoGravatar pboutill2012-05-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15306 85f007b7-540e-0410-9357-904b9bb8a0f7
* Slightly modified the coqtop interface by adding an identifier inGravatar ppedrot2012-05-11
| | | | | | goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15303 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-10 01:38:05 +0000