aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2010-02-26New API for backtracking.vgross
Aside the command stack, the only parameter is the number of step to go back. Went back and forth without sync losses on tests-suite/ide/undo.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12821 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-26Redispatch of printing tweaking hooks.vgross
We want to tweak the printing options when we want to display the results, not when we are evaluating vernac. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12820 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-26Some more adaptations for Debian-->mingw32letouzey
* Remove option -mwindows which isnt working : the GUI binary refuses to launch in a real windows. * simplification of ./build. New way of use : ./configure -prefix "" -arch win32 && ./build win32 This way we avoid any tricks with coq_config.ml. It is also best to avoid ./configure -local otherwise Envars.coqbin () will be wrong later. * Avoid creation of an ad-hoc coq_config in myocamlbuild.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12819 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-26Slight reorganisation of make clean, new entry cleankeepvoletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12818 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-26Coqc: on win32, let's call coqtop.exe by default, not coqtop.opt.exeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12817 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-26Correction du bug #2214 + maj liens webnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12815 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-25mingw32 cross-compilation: coqide.exe as a GUI program, nicer ./build scriptletouzey
we pass -mwindows to the mingw32 linker, this allows coqide.exe to be considered as a GUI windows program instead of as a console one. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12814 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-25ide/coq_lex.ml in .gitignoreletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12813 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-25Enabled natdynlink hack on Mac OS 10.6thutchin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12811 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-25In the git-specific part of Makefile.build, call to hostname gave optionthutchin
--fqdn. Changed this to -f (which has the same behavior) so it will work on Mac OS 10.6 Note: Previous versions of Mac OS 10 don't have this option. Most BSD's don't either. Their default behavior is to output the FQDN where Linux defaults to outputting the short name. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12810 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-25Various fixes in interp, session switching and backtrackingvgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12809 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-25Changes in lexing and tagging.vgross
Lexing send back an offset couple delimiting beginning and ending of sentences. This couple is used to apply a tag on the whole sentence. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12808 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-25Ignoring .spit/.spot files from OCamlSpotterthutchin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12806 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-24Win32 cross-compilation from debian: build of coqide.exe and other binariesletouzey
Details will follow. In a word, we use a gtk+ win32 bundle from gtk.org to build some (unofficial) mingw32-liblablgtk2 debian packages. Then ./configure -local && ./build win32 is enough to get all native win32 binaries and plugin cmxs from a confortable linux box. Next step: an auto-installer :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12804 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-24correction of bug #2088jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12803 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-22Improve unification when evars and metas are mixed.msozeau
If we can't mimick a rhs in an ?evar = rhs situation, we first turn all metas in rhs into evars before trying to solve the equation. Problem reported by Eelis van der Weegen. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12801 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-19added validation of delta_resolver (which seem to have an impact on typing)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12800 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-19[checker] fixed vo validation problems, module incompatibilities remainbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12799 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-19Fixing compilation issuesvgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12798 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-18Removed redundant and ill-named technical lemma.gmelquio
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12797 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-18Removed SeqProp's dependency on Classical.gmelquio
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12796 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-18Removed Rtrigo's dependency on Classical.gmelquio
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12795 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-18Fixing modules names.vgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12794 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-18Experimental build of coqtop.exe + plugins via cross-compilation linux-->win32letouzey
Ideally, just install the cross-compiler (mingw32-ocaml on debian) and launch ./configure -local && ./build win32 For the moment, this needs some twicking of mingw32-ocaml, plus a mingw32-camlp5 which is not yet distributed. If you want to play with that, contact me... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12792 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-18Adding uim filesvgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12791 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-18Polishing the setup of CoqIDE Input Methodvgross
autodetection via ./configure, automated installation target "install-im", and no more patching. Plus documentation of the procedure in the reference manual. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12790 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-17Removed Rseries' dependency on Classical.gmelquio
This is a tradeoff: the Archimedean property is used instead through the discrete logarithm. Thanks to P-M. Pedrot for demonstrating this proof scheme on coq-club. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12787 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-17RelationClasses: adapt eq_Reflexive and co to avoid Universe Inconsistenciesletouzey
We explicitely take care of the argument A to be given to eq_refl,sym,trans when proving that Logic.eq is an instance of Equivalence. This should solve the recent Universe Inconsistencies encountered in CoLoR and FingerTree. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12786 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-17Kill some useless dependencies (Bvector, Program.Syntax)letouzey
Bvector uses only Minus, so let's avoid loading Arith (and hence ArithRing and hence parts of Z, N) Program.Syntax no longer need Lists now that list is in Datatypes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12785 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-17Arith's min and max placed in Peano (+basic specs max_l and co)letouzey
This allow for instance to remove the dependency of List.v toward Min.v To prove max_l and co, we push Le.le_pred and Le.le_S_n into Peano. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12784 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-17Removed Rlimit's dependency on Classical.gmelquio
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12783 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-17Removed Rderiv's dependency on Classical.gmelquio
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12782 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-16Compute the correct generalization information when discharging a classmsozeau
by a class variable. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12781 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-16Fix sort_dependencies for good, maintaining the initial order.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12780 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-16Makefile.build: avoid warning about undefined variable during make installletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12778 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-16Makefile: also install the .cmi of pluginsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12776 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-16Uniformisation Sorting/Mergesort and Structures/Ordersletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12772 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-15Change the customization of modifiers (bug #2210)vgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12771 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-15Util.lowercase_unicode: avoid creating the segmenttree each time (speeds ↵letouzey
some contribs by >30%) (BACKPORT 12768) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12769 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-14update CHANGES : ocamlbuild, Structures, Numbers, MSets ... (cf. commit 8.3 ↵letouzey
r12766) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12767 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-13CompSpec2Type is used to build functions, it should be Defined, not Qedletouzey
This solves in particular the compilation failure of contrib ATBR git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12765 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-13Fix NumbersSyntax.outletouzey
Having to alias the inductive BigN.t_ by a constant BigN.t for satisfying the NSig interface is just a pain. Let's hope it could change someday. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12763 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-12Mycamlbuild: change name of autogenerated file : NMake -> Nmake_genletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12759 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-12Simplify backtrackingvgross
As we can now jump right onto a closed segment, there is no need for complicated pattern matching. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12758 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-12Fixing closing of segments.vgross
You can now BackTo directly inside segments git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12757 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-12Delineating a API for Coq inside toplevel/vernac.mlvgross
Coq use case are mostly thoses : - parsing a char stream to get a vernac expr - evaluating a vernac expr with backtracking - turning a knob with a vernac expr, no backtracking - loading an entire file - compiling an entire file - backtracking (no clean API for this yet) - peeking Coq state info (no clean API for this yet) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12756 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-12Refactoring of the printing optionsvgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12755 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-12CompSpecType, a clone of CompSpec but in Type instead of Propletouzey
In interfaces fields like compare_spec, a CompSpec is prefered to get nice extraction, but then no "destruct (compare_spec .. ..)" is possible in a Type context. Now you can say there "destruct (CompSpec2Type (compare_spec ... ...))" This translate to the Type variant, and make the analysis on it (which is equivalent to analysing the comparison directly). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12753 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-12Remove LocallySorted.v added by mistake at the root of the archiveletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12751 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-11Cleanup in Classes, removing unsupported code.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12748 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 22:33:07 +0000