aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2012-11-28Kernel/closure: add eta red_kindpboutill
The purpose is to the same reds datastructure in closure and in reductionops. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16008 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-26Removed some FIXME related to equality on universes.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16007 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-26Small cleaning of interface in Univppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16006 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-26Monomorphization (toplevel)ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16005 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-26Fixed a monomorphization error.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16004 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-25Monomorphization (tactics)ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16003 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-25Monomorphization (proof)ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16002 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-25Monomorphization (library)ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16001 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-25Monomorphization (parsing)ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16000 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-25Monomorphization (interp)ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15999 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-25More equality functionsppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15998 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-25Fixed bug #2930: folded let-in's were hiding a violation to the occurherbelin
check condition in pattern-unification, resulting in the instantiation of evars by terms depending on themselves, henceforth leading eventually to a stack overflow. Occur-check in the arguments of evars was also missing. [Also fixed what looked like a typo in the env passed to project_evar_on_evar on line 1611.] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15996 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-23Added a constr_pattern_eqppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15995 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-22Monomorphization (pretyping)ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15994 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-22Monomorphization (library)ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15993 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-22Monomorphization (kernel)ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15992 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-22Monomorphization (lib)ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15991 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-21Fixing test-suite: Scope.vppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15990 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-21Print univ constraints generated by a constant or inductive (when flag is set)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15989 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-20Cleaning and small optimization in CList.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15988 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-19Serialize: no need anymore to export of_value / to_value in the mliletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15986 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-19Serialize: dead codeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15985 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-19Serialize: fix dyn-typing of GetOptions (oups), also adapt of_answerletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15984 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-19Serialize.to_answer: dynamically check that answer & call correspondletouzey
Without this, it was probably possible to crash Coqide by forging inadequate answers to a call. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15983 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-18Hurkens' paradox on Type (r15973 and r15977) needs two (non-Set)herbelin
universes. As it uses eq_rect on Type(2), the arguments of eq_rect has to be in Type(3) and compiling the standard library now needs one more universe! If needed, we could avoid this by inlining the definition of (eq_rect Type2) in Hurkens.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15981 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-17Update output/Search.out after hint-related extra defs in Peanoletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15980 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-17Print Assumptions: restore a final \nletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15979 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-17Taking into account the type of a definition (if it exists), and theherbelin
type in "cast" to activate the temporary interpretation scope. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15978 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-15Isolating the ingredients of the proof of Prop<>Type (r15973). Seeingherbelin
it as a consequence of the derivability of Hurkens' paradox in the presence of a retract from Type to Prop. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15977 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-15Some lemmas on property of rewriting. It will probably be worth atherbelin
some time to provide a library stating the groupoid structure of equality proofs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15976 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-15backtrack too much commited files in the last commit.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15975 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-15Fixing emacs diff bug with .dir-locals.el.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15974 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-15Added a proof that Prop<>Type, for arbitrary fixed Type.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15973 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-15A decidability property of functional relations over decidable codomains.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15972 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-15For the record, two examples of short proofs of uniqueness of identityherbelin
proofs, on bool and nat. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15971 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-13Small uniformization in Stringppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15970 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-13More monomorphizationsppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15969 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-13Added a CString module.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15968 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-13coq_makefile: use coqdep instead of ocamldep on .ml4 filesgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15967 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-13Another GC testppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15965 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-12Add an option -nodoc to configure, same (but shorter) than -with-doc noletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15962 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-12Coqide : allow properly closing communication pipes with coqtopletouzey
NB: it's important to close coqide's descriptors (ide2top_w and top2ide_r) in coqtop. We do this indirectly via [Unix.set_close_on_exec]. This way, coqide has the only remaining copies of these descriptors, and closing them later will have visible effects in coqtop. Cf man 7 pipe for more details. This should avoid the need for Unix.kill on coqtop clients (at least when they aren't inside a long computation). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15961 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-12Ide_slave: do not attempt to answer broken requestsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15960 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-12Xml_parser: detect immediate EOF + disable check_eof by defaultletouzey
Without this immediate EOF detection, coqtop -ideslave loops when its input channel is closed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15959 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-12Removed the modification of the GC pressure coefficient, in orderppedrot
to see if that really changes anything. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15958 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
the new Int module. Only the most obvious were removed, so there are a lot more in the wild. This may sound heavyweight, but it has two advantages: 1. Monomorphization is explicit, hence we do not miss particular optimizations of equality when doing it carelessly with the generic equality. 2. When we have removed all the generic equalities on integers, we will be able to write something like "let (=) = ()" to retrieve all its other uses (mostly faulty) spread throughout the code, statically. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15957 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-08Added an Int module with dummy utility functions.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15956 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-08Removing another bunch of generic equalitiesppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15955 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-07Fix reference_or_constr grammar rule to accept @t as a constrgareuselesinge
With the previous formulation extra parentheses had to be added, now they are only necessary for compound expressions, like an application. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15954 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-06Coq is a heavy user of persistent data structures and symbolic ASTs, so theppedrot
minor heap is heavily sollicited. Unfortunately, the default size is far too small, so we enlarge it a lot (128 times larger). To better handle huge memory consumers, we also augment the default major heap increment and the GC pressure coefficient. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15953 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 03:51:25 +0000