aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2012-12-07Coqide: opening non-existing files won't create them immediately anymoreletouzey
... and many more code cleanup concerning file loading git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16034 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-07Coqide: nicer creation of timersletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16033 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-07Coqide: code cleanupletouzey
- indentation, wrap long lines - factorize some code - split Coqide.main in many subfunctions - Put the callbacks in modules (e.g. File.load) - ... Normally this commit shouldn't change coqtop behavior git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16032 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-07* lib/Envars:regisgia
Beautify. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16031 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-07* lib/Envars:regisgia
- Document interface file. - Now export references to ocaml compilers used to compile Coq. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16030 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-07Revert "* tools/Coq_makefile:"regisgia
This reverts commit 9a2f43eca179436f0581751b93c989fd30a5c13c. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16029 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-07* tools/Coq_makefileregisgia
Export $(COQMKTOP) in generated Makefiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16028 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-07* tools/Coq_makefile:regisgia
Add '-I config' in the options of the ocaml compilers. This is useful to reuse site configuration in plugins. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16027 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-06Restoring flush of Welcome message lost in r15148herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16026 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-05Making subset_eq_compat applying over more general domain "Type" (see #2938).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16025 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-04Backtrack on activating scopes with type casts (was r15978).herbelin
IT happens that there are some other uses of casts, e.g. in nat_int de MathClasses which uses a notation 0 for some class constructor zero, and a cast (0:nat) to force this notation 0 to represent the instance O in nat of the class of types having a zero (eventually, 0, i.e. "zero nat O" and "O" are convertible but the information of being a class instance is lost). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16024 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-04Removed Compat.Exc_located outside of compat.ml4, as a consequence ofherbelin
previous commit. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16023 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-04Early translation of camlp4/camlp5 located errors into coq-locatedherbelin
errors so as to be able to work only with Loc.Exc_located inside main Coq. This fixes the anomaly (probably introduced by commit 15847) when a syntax error arrives in coqc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16022 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-04Low-level hack to get some more informative message from dynamic loading errors.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16021 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-04Fixing a comment.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16020 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-04Revised the strategy for automatic insertion of spaces when printingherbelin
notations: - hopefully never 2 spaces when the user did not ask for - more systematic default insertion of spaces around symbols - e.g. have space before "[" if after a non-terminal - have spaces between consecutive terminals git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16019 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-04Display Menu now called View Menu (in CoqIDE preferences).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16018 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 05:33:29 +0000