aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Reorder resolution of type class and unification constraints.Gravatar msozeau2010-03-07
| | | | | | | | Fix a bug in dependent elimination when treating defined variables in the context. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12851 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix lifting of constraints in generalized rewriting tactic.Gravatar msozeau2010-03-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12850 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix treatment of remaining unification constraints: raise a moreGravatar msozeau2010-03-07
| | | | | | | | | informative exception if some constraints do not unify. All calls except one used to raise a less informative exception when the constraints weren't solved. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12849 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes in rewrite and a Elimination/Case to Scheme:Gravatar msozeau2010-03-06
| | | | | | | | | | | | | | - disallow dynamic generation of [case] constructs through [find_scheme] during a rewrite, as it changes the global environment and subsequent manipulations of the tactic may use an outdated environment. - use local exception names so as not to catch and hide unexpected [Not_found] exceptions. - fix lifting of constraints for dependent function types - Allow rewriting on morphisms (terms in function position) even with [rewrite] (fixes bug #2178). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12848 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding Function as keyword for coqdocGravatar thery2010-03-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12847 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: some more cleanupGravatar letouzey2010-03-05
| | | | | | | | | | | | | - avoid recomputing CAMLP4DEPS in the %.ml:%.ml4 rule - a macro for compiling the tools by the best ocaml compiler - use of $(if ...) rather that $ifdef - some variables of Makefile.common were not that useful (e.g. $(COQCCMX), which is $(COQCCCMO:.cmo=.cmx), used only once) - the build of coqc.* should not depend upon coqtop, only its launch (or I'm missing something) - useless $(CAMLP4EXTENDFLAGS) variable git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12846 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes.Gravatar msozeau2010-03-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12845 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improvements in generalized rewriting:Gravatar msozeau2010-03-05
| | | | | | | | | | | | | | - support a new strategy: reduction using any of the allowed reduction operators. This strategy does _not_ make the proof size grow. - support rewriting under arbitrary [match with] using a folding strategy. We fold matches to applications of registered [case] combinators and let the user declare the Proper instances for them. - fix the lemma application strategy to correctly report when no progress has been made (avoids loop when repeateadly rewriting with convertible terms). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12844 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix [autounfold] to accept general [in] clauses.Gravatar msozeau2010-03-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12843 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a generic tactic option builder. Use it in firstorder to set theGravatar msozeau2010-03-05
| | | | | | | | | default solver (using "Set Firstorder Solver") and for program's obligation tactic. I don't understand exactly the reason of the warning when building states/initial.coq, anyone? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12842 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: a nicer hack concerning ocamlopt with no .mli: -intf-suffix .cmi ↵Gravatar letouzey2010-03-04
| | | | | | (thanks A. Frisch) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12841 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: cleanup of comments + a few words about recent changes in ↵Gravatar letouzey2010-03-04
| | | | | | dev/doc/build*.txt git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12840 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: no more separate stagesGravatar letouzey2010-03-04
| | | | | | | | | | | | | | - Instead of the separate stage mechanism, we let make handle the build and inclusion of all .d. Some initial calls to camlp4o will fail, but make tries again later, and this finally works great. These initial error message are made nice to avoid bad interaction with M-x next-error - The only recursive call to a sub-make is Makefile calling Makefile.build in which the includes of .d take place. This allows to avoid compiling anything for a make clean or make tags git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12839 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqdep_boot: when emultating ocamldep, avoid outputting empty answerGravatar letouzey2010-03-04
| | | | | | | | | | | When we emulate ocamldep via "coqdep_boot -mldep ocamldep", it's nicer to get something as output, even if there's no dependencies. Something like foo.cmo: foo.cmx: at least indicates that something has been done. Moreover it's closer to the behavior of ocamldep git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12838 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: try to avoid rare make failures related with make -j + ocamlopt + .cmiGravatar letouzey2010-03-04
| | | | | | | | | | | | | | | | | | As said now in a comment of Makefile.build: NB: for the moment ocamlopt erases and recreates .cmi if there's no .mli around. This can lead to nasty things with make -j (e.g. another process accessing a partial .cmi). To avoid that: 1) We make .cmx always depend on .cmi 2) This .cmi will be created from the .mli, or trigger the compilation of the .cmo if there's no .mli (see rule below about MLWITHOUTMLI) 3) We tell ocamlopt to output to temporary names, remove the temp .cmi (since the actual .cmi should already be there and up-to-date) and move the temp .cmx and .o back in place Ok, this is quite a hack. I'll make a proper bug report to ocaml asap... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12837 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: cleanup of variables containing lists of files, such as MLFILESGravatar letouzey2010-03-04
| | | | | | | | | | | | | | - We clarify their definition via some custom make function: find, diff... - We avoid duplications via some $(sort ...) - Some name changes: * old $(MLFILES) now corresponds to $(MLSTATICFILES) (but .ml from .mly and .mll aren't in it anymore). * new $(MLFILES) contains all .ml, either static or generated from .mly .mll .ml4 or _mod.ml made out of .mllib * $(ML4FILESML) is now $(GENML4FILES) ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12836 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: make devdocclean was not removing *.dep.ps, btw let's remove ↵Gravatar letouzey2010-03-04
| | | | | | | | *.dep.ps for svn the syntax for find is sooo intuitive ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12835 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: factorization of default rules for .cmi/.cmo/.cmxGravatar letouzey2010-03-04
| | | | | | | | We use some conditional variables $(if ...) to set the proper flags instead of fully duplicating the rules according to the path checker/%.cm? ide/%.cm? %.cm? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12834 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: the .ml of .ml4 are now produced explicitely (in binary ast form)Gravatar letouzey2010-03-04
| | | | | | | | | | | | | | | | - This way, the Makefile.build gets shorter and simplier, with a few nasty hacks removed. - In particular, we stop creating dummy .ml of .ml4 early "to please ocamldep". Instead, we now use ocamldep -modules, and process its output via coqdep_boot. This ways, *.cm* of .ml4 are correctly located, even when some .ml files aren't generated yet. - There is no risk of editing the .ml of a .ml4 by mistake, since it is by default in a binary format (cf pr_o.cmo and variable READABLE_ML4). M-x next-error still open the right .ml4 at the right location. - mltop.byteml is now mltop.ml, while mltop.optml keeps its name - .ml of .ml4 are added to .gitignore git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12833 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: hide the trick ...||(RV=$$?;rm $@; exit $${RV}) under a macro ↵Gravatar letouzey2010-03-04
| | | | | | $(TOTARGET) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12832 85f007b7-540e-0410-9357-904b9bb8a0f7
* amelioration mineure dans FunctionGravatar jforest2010-03-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12826 85f007b7-540e-0410-9357-904b9bb8a0f7
* New backtracking code + fix bug #2082.Gravatar vgross2010-02-26
| | | | | | Previous code checkings were too lax, and information was lost. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12823 85f007b7-540e-0410-9357-904b9bb8a0f7
* Introducing a dual stack setupGravatar vgross2010-02-26
| | | | | | | The first stack lives in coqide and tracks the tagging and locking, the second lives in coq and tracks the commands. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12822 85f007b7-540e-0410-9357-904b9bb8a0f7
* New API for backtracking.Gravatar vgross2010-02-26
| | | | | | | 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
* Redispatch of printing tweaking hooks.Gravatar vgross2010-02-26
| | | | | | | 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
* Some more adaptations for Debian-->mingw32Gravatar letouzey2010-02-26
| | | | | | | | | | | | | | | * 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
* Slight reorganisation of make clean, new entry cleankeepvoGravatar letouzey2010-02-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12818 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqc: on win32, let's call coqtop.exe by default, not coqtop.opt.exeGravatar letouzey2010-02-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12817 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #2214 + maj liens webGravatar notin2010-02-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12815 85f007b7-540e-0410-9357-904b9bb8a0f7
* mingw32 cross-compilation: coqide.exe as a GUI program, nicer ./build scriptGravatar letouzey2010-02-25
| | | | | | | 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
* ide/coq_lex.ml in .gitignoreGravatar letouzey2010-02-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12813 85f007b7-540e-0410-9357-904b9bb8a0f7
* Enabled natdynlink hack on Mac OS 10.6Gravatar thutchin2010-02-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12811 85f007b7-540e-0410-9357-904b9bb8a0f7
* In the git-specific part of Makefile.build, call to hostname gave optionGravatar thutchin2010-02-25
| | | | | | | | | --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
* Various fixes in interp, session switching and backtrackingGravatar vgross2010-02-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12809 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changes in lexing and tagging.Gravatar vgross2010-02-25
| | | | | | | | 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
* Ignoring .spit/.spot files from OCamlSpotterGravatar thutchin2010-02-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12806 85f007b7-540e-0410-9357-904b9bb8a0f7
* Win32 cross-compilation from debian: build of coqide.exe and other binariesGravatar letouzey2010-02-24
| | | | | | | | | | | | 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
* correction of bug #2088Gravatar jforest2010-02-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12803 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improve unification when evars and metas are mixed.Gravatar msozeau2010-02-22
| | | | | | | | | 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
* added validation of delta_resolver (which seem to have an impact on typing)Gravatar barras2010-02-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12800 85f007b7-540e-0410-9357-904b9bb8a0f7
* [checker] fixed vo validation problems, module incompatibilities remainGravatar barras2010-02-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12799 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing compilation issuesGravatar vgross2010-02-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12798 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed redundant and ill-named technical lemma.Gravatar gmelquio2010-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12797 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed SeqProp's dependency on Classical.Gravatar gmelquio2010-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12796 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed Rtrigo's dependency on Classical.Gravatar gmelquio2010-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12795 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing modules names.Gravatar vgross2010-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12794 85f007b7-540e-0410-9357-904b9bb8a0f7
* Experimental build of coqtop.exe + plugins via cross-compilation linux-->win32Gravatar letouzey2010-02-18
| | | | | | | | | | | 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
* Adding uim filesGravatar vgross2010-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12791 85f007b7-540e-0410-9357-904b9bb8a0f7
* Polishing the setup of CoqIDE Input MethodGravatar vgross2010-02-18
| | | | | | | | 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
* Removed Rseries' dependency on Classical.Gravatar gmelquio2010-02-17
| | | | | | | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-13 08:30:01 +0000