aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2012-12-04Identities over types satisfying Uniqueness of Identity Proofsherbelin
themselves satisfied Uniqueness of Identity Proofs. Otherwise said uniqueness of equality proofs is enough to characterize types whose equality has a degenerated "homotopical" structure (this is a short proof of a result inspired by Voevodsky's proof of inclusion of h-level n into h-level n+1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16017 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-04Coqmktop: use the atomic Filename.open_temp_fileletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16016 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-28Evarconv: Fix #2936 + commentspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16011 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-28Fix ocamldebug constr printerpboutill
In paterns, we do not try to put _ for params. (nb_params is found using Global table that ocamldebug to not have) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16010 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-28Reductionops uses Closure.redspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16009 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 19:50:00 +0000