aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2013-01-27Avoid failure in debugger when printing Ltac names.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16152 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-26updating ide/coq documentationppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16151 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-26Monadification of coqtop queries in CoqIDEppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16150 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-26Uniformization of Coq tasksppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16149 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-25Better handling of escape find in CoqIDEppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16148 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-25Better Undo/Redo mechanismppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16147 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-25Trying to fix CoqIDE undo/redo mechanismppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16146 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-25Fixing autocompletion in CoqIDEppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16145 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-25Fixup last commitppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16144 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-25Hugo request: CoqIDE find on enterppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16143 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-24Reductionops: whd_state_gen can take and answers a cst_stack toopboutill
+ cst_stack is kept en a meta/evar is "unfold". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16142 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-24Fixed parsing of -no-native-compiler flag.mdenes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16141 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-24Native compiler: warnings were not turned off for OCaml 3.11mdenes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16140 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-23Coqide: limit read buffer size to 4096 (pipe size in win32)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16139 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-22Coqide: avoid potentially blocking read on coqtop channelletouzey
With Pierre-Marie, we discovered the hard way that Glib.Io reads are *not* non-blocking by default as I thought. My bad... This was causing nasty freezes of coqide in the rare cases where the final read was exactly filling the buffer (which was of size 1024). Now: - the input channels from coqtop (and various other external commands) are given to Unix.set_nonblock - Exceptions in our io_read_all (typically a kind of EAGAIN) terminate the read - We can now switch to Glib.Io.read_chars instead of the deprecated Glib.Io.read. - Btw, we use a larger buffer (8192). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16138 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-22Added .native to .gitignoreppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16137 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
native OCaml code. Warning: the "retroknowledge" mechanism has not been ported to the native compiler, because integers and persistent arrays will ultimately be defined as primitive constructions. Until then, computation on numbers may be faster using the VM, since it takes advantage of machine integers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16136 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-22Revert "remove -rectypes except for term.ml"mdenes
Preparing landing of the native compiler, which requires -rectypes flag. This reverts commit f975575187d0a19e7cc1afc43459a92eeb12b3f1. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16135 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-22- Fix evarconv so that we have complete eta-conversion:msozeau
- In the maybeflex/rigid (lambda) case, try eta if the maybeflex doesn't actually unfold (e.g. vars, or the transparent state says it's opaque). - In the flexible/rigid(lambda) case, try eta if miller-pfenning fails (as the stack might not be a purely applicative one). This will zip the flexible term (a case construct most likely) and try eta expansion on it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16134 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-21Fix bug 2958: Inductive deep in in clause are impossiblepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16133 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-21Last test-suite not in Symmetric Patterns syntaxpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16132 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-18I forget to use git log before git svn dcommit ...pboutill
Revert "Revert "coq_makefile: use coqdep instead of ocamldep on .ml4 files"" This reverts commit 7b9856f2eae3bd652d99864c9901f7c4af290323. The reason for my private revert is that coqdep does not find the dependencies of .ml4 files in AACTactics user-contrib correctly but it is a coqdep bug not a coq_makefile one ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16131 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-18Evarconv: Check stack before term in Canonical Structure approuvalpboutill
3 days of work to swap 2 lines ... but this fixes LemmaOverloading (and hopfully makes Feit-Thomson compilation time back to "normal") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16130 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-18Unset Asymmetric Patternspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16129 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-18Revert "coq_makefile: use coqdep instead of ocamldep on .ml4 files"pboutill
This reverts commit d14b9f6a017347e59cf037ff576f282785105080. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16128 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-12Envar: in w32, add .exe when searching for caml binariesletouzey
Based on a patch by Pierre-Yves Strub git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16124 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-12Coqmktop and camlp4 : sequel to commit 16113letouzey
Actually I don't see any reason to link q_utils and q_coqast in coqtop.byte specifically when using camlp4 (and not camlp5). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16121 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-07Coq_makefile: quoting pathspboutill
Global paths (binaries & install dir) are quoted, local paths are never ! From a patch by Jason Gross. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16119 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-07Coq_makefile: -extra & -phony-extra for user defined makefile rulepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16118 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-07Fixup notation printing in patternspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16117 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-06* Kernel/Terms:regisgia
Fix an inconsistency in the hashing function of [constr]s. (Thanks to Thomas Braibant for having pointed this out.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16116 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-22Avoiding collision between Camlp4 Loc.Exc_located and Coq's Loc.Exc_located.herbelin
Also fixing coqmktop for use with Camlp4. Don't know if this is the fix intended by coqmktop experts or not, though. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16113 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-21nat_iter n f x -> nat_rect _ x (fun _ => f) npboutill
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
2012-12-21Yet a new reduction tactic in Coq : cbnpboutill
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
2012-12-21Awful heuristic to refold mutual fixpoint in reductionopspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16110 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-21Fixup and comment reductionopspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16109 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-19Reductionops reduction machine can refold constantpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16107 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-19Evarconv.Pseudorigid erasurepboutill
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
2012-12-19Coqide: cleaner Coq.PrintOpt and session creationletouzey
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
2012-12-19Array.create is deprecatedpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16104 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-19GtkData.set_default_modifiers and no access to <primary> in lablgtk -> ↵pboutill
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
2012-12-19Fix coqtop -config when absolute path have been given for ocaml*pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16102 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-18Rework of GenericMinMax and OrdersTac (helps extraction, cf. #2904)letouzey
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
2012-12-18Modulification of nameppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16099 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-18Modulification of mod_bound_idppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16098 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-18Modulification of Labelppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16097 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-18Fixing parsing of specific primitive tokens used as notations for patternsherbelin
(e.g. 1 for eq_refl). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16094 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-18Taking into account the possibility of having a type of type which isherbelin
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
2012-12-18Extraction: qualified names in Extract Constant examples (fix #2878)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16089 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-18No more constant named "int" in Coq theories (cf bug #2878)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16088 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 23:25:39 +0000