aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* nat_iter n f x -> nat_rect _ x (fun _ => f) nGravatar pboutill2012-12-21
| | | | | | | | It is much beter for everything (includind guard condition and simpl refolding) excepts typeclasse inference because unification does not recognize (fun x => f x b) a when it sees f a b ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16112 85f007b7-540e-0410-9357-904b9bb8a0f7
* Yet a new reduction tactic in Coq : cbnGravatar pboutill2012-12-21
| | | | | | | | | | | It is supposed to become the next generation of the simpl tactics (it "refolds" constant) but 1/it is a bit more aggresive than the old simpl 2/it cannot be customized as simpl start to be 3/(for now)it does not refold in reccursive calls constant such as compare x y := compare_cont x y Eq := (fix compare_cont x y s := ...) x y Eq git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16111 85f007b7-540e-0410-9357-904b9bb8a0f7
* Awful heuristic to refold mutual fixpoint in reductionopsGravatar pboutill2012-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16110 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixup and comment reductionopsGravatar pboutill2012-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16109 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reductionops reduction machine can refold constantGravatar pboutill2012-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16107 85f007b7-540e-0410-9357-904b9bb8a0f7
* Evarconv.Pseudorigid erasureGravatar pboutill2012-12-19
| | | | | | flex_kind is computed from the real term that blocks the reduction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16106 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: cleaner Coq.PrintOpt and session creationGravatar letouzey2012-12-19
| | | | | | | | | | | PrintOpt.set now only updates the state Hashtbl of options, a PrintOpt.enforce is mandatory to transmit them to coqtop. This enforce is done for instance by Coq.goals. The various signal handlers about coqide's buffer are now installed in session creation, and not anymore via the coqops initializer. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16105 85f007b7-540e-0410-9357-904b9bb8a0f7
* Array.create is deprecatedGravatar pboutill2012-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16104 85f007b7-540e-0410-9357-904b9bb8a0f7
* GtkData.set_default_modifiers and no access to <primary> in lablgtk -> ↵Gravatar pboutill2012-12-19
| | | | | | | | unsuable Coqide under MacOS makes Command not working on MacOS and consequently breaks all default shortcuts 'o' opens a file 'w' close the buffer ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16103 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix coqtop -config when absolute path have been given for ocaml*Gravatar pboutill2012-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16102 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rework of GenericMinMax and OrdersTac (helps extraction, cf. #2904)Gravatar letouzey2012-12-18
| | | | | | | | | | | | | | | | | | | | | | | Inner sub-modules with "Definition t := t" is hard to handle by extraction: "type t = t" is recursive by default in OCaml, and the aliased t cannot easily be fully qualified if it comes from a higher unterminated module. There already exists some workarounds (generating Coq__XXX modules), but this isn't playing nicely with module types, where it's hard to insert code without breaking subtyping. To avoid falling too often in this situation, I've reorganized: - GenericMinMax : we do not try anymore to deduce facts about min by saying "min is a max on the reversed order". This hack was anyway not so nice, some code was duplicated nonetheless (at least statements), and the module structure was complex. - OrdersTac : by splitting the functor argument in two (EqLtLe <+ IsTotalOrder instead of TotalOrder), we avoid the need for aliasing the type t, cf NZOrder. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16100 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of nameGravatar ppedrot2012-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16099 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of mod_bound_idGravatar ppedrot2012-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16098 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of LabelGravatar ppedrot2012-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16097 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing parsing of specific primitive tokens used as notations for patternsGravatar herbelin2012-12-18
| | | | | | (e.g. 1 for eq_refl). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16094 85f007b7-540e-0410-9357-904b9bb8a0f7
* Taking into account the possibility of having a type of type which isGravatar herbelin2012-12-18
| | | | | | | | an evar in typing.ml. Thanks to HoTT people for noticing the problem. Fixed behavior of e_typing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16092 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: qualified names in Extract Constant examples (fix #2878)Gravatar letouzey2012-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16089 85f007b7-540e-0410-9357-904b9bb8a0f7
* No more constant named "int" in Coq theories (cf bug #2878)Gravatar letouzey2012-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16088 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a little inefficiency of "set/destruct" over a pattern. NowGravatar herbelin2012-12-18
| | | | | | different instances of a meta are checked against full conversion. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16086 85f007b7-540e-0410-9357-904b9bb8a0f7
* Factorization of the elim unif flag with the default flag. SinceGravatar herbelin2012-12-18
| | | | | | | fine-tuning of unif flags is still ongoing, I prefer however not to go too far in factorization yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16085 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed interpretation of "x" as a binding variable for the returnGravatar herbelin2012-12-17
| | | | | | | | predicate in "match x return ... with" when x is a goal variable. Commit 4926 forbade it but too strongly. AFAICS, only notation variables have to be avoided. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16083 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do not display REVERTcast inserted by reduction tactics (unless printing all).Gravatar herbelin2012-12-17
| | | | | | Question of printing DEFAULTcast inserted by reduction tactics still open. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16081 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a bug in the algorithm trying to elaborate a "match" return predicate.Gravatar herbelin2012-12-17
| | | | | | | | | | | | | This occurred in a second choice strategy which is anyway probably not used in general, but the bug showed up in error messages since these messages reports on the second choice when the first choice has failed because of user-side typing error. Anyway, having two strategies for building a return predicate will probably eventually disappear with the increase of the strength of unification. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16078 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ide_slave: do not prepare debug messages in non-debug modeGravatar letouzey2012-12-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16077 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction of projections: restrict a hack to ocaml only (fix #2941)Gravatar letouzey2012-12-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16074 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing ocalmdoc commentGravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16073 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of dir_pathGravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16072 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of identifierGravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing CoqIDE compilationGravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16070 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving hcons_string to String namespace.Gravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16069 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved Stringset and Stringmap to String namespace.Gravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16068 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved Intset and Intmap to Int namespace.Gravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16067 85f007b7-540e-0410-9357-904b9bb8a0f7
* Implemented a full-fledged equality on [constr_expr]. By the way,Gravatar ppedrot2012-12-14
| | | | | | some cleaning of the interface and moving of code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16066 85f007b7-540e-0410-9357-904b9bb8a0f7
* Using library string functions.Gravatar ppedrot2012-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16065 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documented CString.Gravatar ppedrot2012-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16064 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renamed Option.Misc.compare to the more uniform Option.equal.Gravatar ppedrot2012-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16063 85f007b7-540e-0410-9357-904b9bb8a0f7
* Wg_ScriptView: avoid invalid iters during completionGravatar letouzey2012-12-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16061 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: allow editing even during a backtrackGravatar letouzey2012-12-11
| | | | | | | For that, we removing read-only tags on the backtracked zone only at the end of the backtrack git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16060 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_lex: direct accounting of utf8 extra bytes in offsetsGravatar letouzey2012-12-11
| | | | | | | | | We directly produce in Coq_lex a utf8 char offset instead of a byte offset, by counting the utf8 extra byte during the lexing. This way, no need anymore for converting later with complex byte_offset_to_char_offset. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16059 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: restore the tag removal of copy-pasted zonesGravatar letouzey2012-12-10
| | | | | | | | The handler for apply_tag removed in commit 16044 was probaly meant for that. We now proceed in a more simple way, in Sentence.split_slice_lax, instead of doing a remove_tag in a apply_tag handler (!). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16058 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: some more refactoring to lighten coqide.mlGravatar letouzey2012-12-10
| | | | | | | | | | | | | | | | | | | Main victim is analyzed_view : - some unnecessary methods have been killed (hep_for_keyword for instance) - some other migrated elsewhere (recenter_input, find_next_occurrence, ...) - analyzed_view is now split in two : fileops (filename, save, revert, ...) and coqops (process_next_phrase, ...) Four new files created: - Sentence (for tag_on_insert and alii) - FileOps (ex-first-half of analyzed_view) - CoqOps (ex-second-half of analyzed_view) - Session (ex-record viewable_script and functions about it) Also lots of renaming, trying to be shorter (but still meaningful) and more uniform git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16057 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_makefile: Better rule for subdirs when the subdir does not existGravatar pboutill2012-12-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16056 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tiny fix of r16049Gravatar pboutill2012-12-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16055 85f007b7-540e-0410-9357-904b9bb8a0f7
* * Implementing the "union by rank" optimisation in univ.mlGravatar pboutill2012-12-10
| | | | | | | | | | * Bugfixes in union by rank in univ.ml * kernel/univ.ml: clarify the rank union selection logic Author: Jacques-Henri Jourdan <jacques-henri.jourdan@inria.fr> Author: Gabriel Scherer <gabriel.scherer@inria.fr> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16054 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ensure that a function declared with a label is used with itGravatar letouzey2012-12-08
| | | | | | This correspond to ocaml4 warning 6 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16053 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finish patch for Hint Resolve, stopping to generate new constant names forGravatar msozeau2012-12-08
| | | | | | | hints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16052 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: use labels for all labelled functionsGravatar letouzey2012-12-08
| | | | | | | | This isn't mandatory, but it's a good practice. For instance it allows to easily locate all ~callback arguments. Cf. warning 6 of OCaml 4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16051 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: handle possible fragmentation in xml answersGravatar letouzey2012-12-08
| | | | | | | | | Experimentally, this occurs at least in win32 when sending commands quickly enough: one handle_input callback received only a part of an xml answer, the rest was available only during the next handle_input. So we store unterminated xml fragments across handle_input invocations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16050 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: get rid of threads, use gtk asynchronous i/o insteadGravatar letouzey2012-12-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Threads were only there to handle blocking dialogs with the different coqtops. But programming with threads have drawbacks : complex mutex infrastructure, possible deadlocks, etc. In particular gtk functions are not meant to be called from a thread which isn't the gtk main loop, (unless some gtk mutex have been taken). This seem to pose problem specifically in win32 (and macosx ?), hence the use of the GtkThread.(a)sync hack for scheduling code for execution in the gtk main loop. Instead, we now use the Glib.Io module to install a callback that will be runned when some answer of coqtop is available on the channel. This implies using now a continuation-passing style: for instance, instead of two sequential requests to coqtop, we'll now have the 2nd request inside the callback handling the answer to the 1st request. Remarks: - Also use asynchronous i/o for external commands (editor, coqc, make...). Launching an external editor or browser won't freeze coqide anymore. - Reworked handling of coqtop process, especially when closing them. A responsive coqtop should now hara-kiri immediatly when its input channel is closed. Otherwise we try later a soft kill, then some hard kills if necessary. If nothing work we warns the user. When quitting coqide, all this might induce a small delay (2s at worse). - Be careful now to avoid "long" computations (or blocking i/o) in a coqide function. Experimentally, it seems that loading/saving a .v file is quick enough. If necessary, we could use asynchronous i/o also for writing the .v, but for loading I've no clue. - In the Coqide module, we ensure that the current continuation k will indeed be run at the end thanks to an abstract return type (void = opaque copy of unit). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16049 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed a unused function in PpGravatar ppedrot2012-12-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16048 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 19:05:12 +0000