aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Win32: let's directly make coqtop.exe and coqide.exe incorporate coq.icoGravatar letouzey2011-04-21
| | | | | | This is an adaptation of commit 13747 for 8.3 branch git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14038 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug fix: concurrent access of persistent_cacheGravatar fbesson2011-04-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14037 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: Fix the command separator for external cmds (#2363)Gravatar letouzey2011-04-20
| | | | | | | | | | | | We use "&&" instead of ";" which is - compatible with unix and win32 - more adequate anyway than ";" : no need to run the command if the cd has failed... Concerning coqdoc, since previous commit it should not be mandatory to provide the "--coqlib-path" option. We remove them... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14036 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqdoc: also try coqlib relative to the coqdoc binary locationGravatar letouzey2011-04-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14035 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allow betaiota when checking unification of the types of metas (fixes ATBR ↵Gravatar msozeau2011-04-20
| | | | | | contrib). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14032 85f007b7-540e-0410-9357-904b9bb8a0f7
* Don't force progress on instance applications, there is always progress when ↵Gravatar msozeau2011-04-20
| | | | | | refining dependent instances git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14031 85f007b7-540e-0410-9357-904b9bb8a0f7
* This is used in the rippling plugin. This also allows fixing bug #2188.Gravatar msozeau2011-04-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14030 85f007b7-540e-0410-9357-904b9bb8a0f7
* Declarative mode: fix escape and return.Gravatar aspiwack2011-04-19
| | | | | | The declarative mode should now work almost like in v8.3 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14029 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix thumb2-related build errorGravatar glondu2011-04-19
| | | | | | | | Bug-Debian: http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=622882 Signed-off-by: Konstantinos Margaritis <markos@genesi-usa.com> Signed-off-by: Stephane Glondu <steph@glondu.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14027 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix generated script for NMake, a rewrite necessitates full conversion forGravatar msozeau2011-04-18
| | | | | | checking types. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14023 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a flag to control betaiota reduction during unification to maintain ↵Gravatar msozeau2011-04-18
| | | | | | backward compatibility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14022 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix unification of types of metavariables and error message for sort ↵Gravatar msozeau2011-04-16
| | | | | | unification. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14020 85f007b7-540e-0410-9357-904b9bb8a0f7
* Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".Gravatar herbelin2011-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14018 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqc: fix the exit codeGravatar letouzey2011-04-15
| | | | | | Patch suggested by Benjamin Monate git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14016 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: nicer error when a toplevel module has no body (#2525)Gravatar letouzey2011-04-15
| | | | | | | | | I thought this situation wasn't possible, hence the Option.get. But it's apparently legal to use Declare Module anywhere, even outside a Module Type. No idea on how to handle that at extraction for the moment, hence a proper "unsupported" error message. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14013 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: allow extracting Ascii.ascii to native Char in Haskell (fix #2515)Gravatar letouzey2011-04-15
| | | | | | We simply factorize code that was already existing for Ocaml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14011 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation typo.Gravatar gmelquio2011-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14008 85f007b7-540e-0410-9357-904b9bb8a0f7
* More informative anomaly.Gravatar herbelin2011-04-14
| | | | | | Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14002 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add directories in COQPATH to search path.Gravatar herbelin2011-04-14
| | | | | | | | This is to allow users to install plugins when coq is installed system-wide. Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14001 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reorder search path order, so the standard library is search last.Gravatar herbelin2011-04-14
| | | | | | | | | This allows the construction of an extended library that shadows the standard library. Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14000 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: opaque terms are not traversed anymore by defaultGravatar letouzey2011-04-13
| | | | | | | | | | | | | In signatures, opaque terms are always seen as parameters. In implementations, a flag Set/Unset Extraction AccessOpaque allows to customize things: - Set : opacity is ignored (this is the old behavior) - Unset : opaque terms are extracted as axioms (default now) Some warnings are anyway emitted when extraction encounters informative opaque terms. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13999 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert "Add [Polymorphic] flag for defs"Gravatar msozeau2011-04-13
| | | | | | | | | | | This reverts commit 33434695615806a85cec88452c93ea69ffc0e719. Conflicts: kernel/term_typing.ml test-suite/success/polymorphism.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13998 85f007b7-540e-0410-9357-904b9bb8a0f7
* Put dependent subgoals first so as to allow backtracking on them, might ↵Gravatar msozeau2011-04-13
| | | | | | change resolution time quite a bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13997 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Make typeclass transparency information directly availableGravatar msozeau2011-04-13
| | | | | | | - Fix pretyping to consider remaining unif problems with the right transparency information. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13996 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Remove create_evar_defsGravatar msozeau2011-04-13
| | | | | | - Be careful with consider_remaining_unif_problems: it might instantiate an evar, including the current goal! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13995 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix merge.Gravatar msozeau2011-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13994 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Improve unification (beta-reduction, and same heuristic as evarconv for ↵Gravatar msozeau2011-04-13
| | | | | | reducing matches). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13993 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix scripts relying on unification not doing any beta reduction.Gravatar msozeau2011-04-13
| | | | | | They are actually simpler, sometimes using the [rewrite at] variant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13992 85f007b7-540e-0410-9357-904b9bb8a0f7
* Unify meta types with the right flags, add betaiotazeta reduction to ↵Gravatar msozeau2011-04-13
| | | | | | unification (potentially harmful) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13991 85f007b7-540e-0410-9357-904b9bb8a0f7
* Proper typing of metavariables, type errors were completely ignored ↵Gravatar msozeau2011-04-13
| | | | | | before... Use sort constraint checking as in evarconv as well git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13990 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Do not make constants with an assigned type polymorphic (wrong unfoldings).Gravatar msozeau2011-04-13
| | | | | | - Add Set Typeclasses Debug/Depth n options for typeclasses eauto. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13989 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add [Polymorphic] flag for defsGravatar msozeau2011-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13988 85f007b7-540e-0410-9357-904b9bb8a0f7
* Subtyping: align coqtop behavior concerning opaque csts on coqchk's oneGravatar letouzey2011-04-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | After discussion with Bruno and Hugo, coqtop now accepts that an opaque constant in a module type could be implemented by anything of the right type, even if bodies differ. Said otherwise, with respect to subtyping, an opaque constant behaves just as a parameter. This was already the case in coqchk, and a footnote in documentation is advertising for quite some time that: "Opaque definitions are processed as assumptions." Truly, it might seem awkward that "Definition x:=3" can implement "Lemma x:nat. Proof 2. Qed." but the opacity ensures that nothing can go wrong afterwards, since Coq is forced to ignore that the x in signature has body "2". Similarly, "T with Definition x := c" is now legal when T contains an opaque x, even when this x isn't convertible with c. By avoiding accesses to opaque bodies, we also achieve some speedup (less delayed load of .vo final sections containing opaque terms). Nota: the extraction will have to be adapted, since for the moment it might access the body of opaque constants: the warning emitted when doing that should become an error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13987 85f007b7-540e-0410-9357-904b9bb8a0f7
* remove old traces of SearchIsos (never ported to 7.x nor 8.x)Gravatar letouzey2011-04-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13986 85f007b7-540e-0410-9357-904b9bb8a0f7
* Catch NotArity exception and transform it into an anomaly in retyping.Gravatar msozeau2011-04-11
| | | | | | | | | | Add a temporary fix in solve_simple_eqn to catch anomalies coming from retyping because the unification algorithm with metas doesn't respect the precondition that evar instances should be well-typed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13985 85f007b7-540e-0410-9357-904b9bb8a0f7
* ocamlbuild: support again camlp5 in addition to camlp4Gravatar letouzey2011-04-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13984 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applying Tom Prince's patch to coqdep not correctly applying the -R visibilityGravatar herbelin2011-04-08
| | | | | | | discipline to files from stdlib or user library (also factorized code with add_known) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13982 85f007b7-540e-0410-9357-904b9bb8a0f7
* A kind of reply to bug 2444Gravatar pboutill2011-04-08
| | | | | | | coq_makefile uses ocaml{c,opt}.opt if it uses coqc -opt and ocaml‘c,opt} if it uses coqc -byte. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13980 85f007b7-540e-0410-9357-904b9bb8a0f7
* weak dependency of coqtop for coqide and coqc (bug 2390)Gravatar pboutill2011-04-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13979 85f007b7-540e-0410-9357-904b9bb8a0f7
* A module out of Program to have list notations (bug 2463)Gravatar pboutill2011-04-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13978 85f007b7-540e-0410-9357-904b9bb8a0f7
* @ in index of refman (last request of bug 2494)Gravatar pboutill2011-04-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13977 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add "make full-stdlib" to make all the doc in pdf as ask by bug 2395Gravatar pboutill2011-04-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13976 85f007b7-540e-0410-9357-904b9bb8a0f7
* More up to date About in coqideGravatar pboutill2011-04-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13975 85f007b7-540e-0410-9357-904b9bb8a0f7
* Macos integration step2 : shutdownGravatar pboutill2011-04-08
| | | | | | | | | You can quit coqide from the dock and reboot/shutdown will ask you if you want to save your unsavec files. Asks for a re"configure". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13974 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide shutdown process change (and out the main function)Gravatar pboutill2011-04-08
| | | | | | | | It now checks for 5 sec every 0.1 sec if is there is still running coqtop then it asks the user if he wants to leave zombies or cancel quit. (Cancel quit was continue to wait). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13973 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applying Tom Prince's patch for build_constant_by_tactic not able toGravatar herbelin2011-04-08
| | | | | | use a lemma name chosen by the caller (here tclABSTRACT) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made warning about ending comments in string less intrusive so as to supportGravatar herbelin2011-04-08
| | | | | | things like (* "forall X : (* Type *), X" *) without warnings git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13971 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applying and reworking Tom Prince's patch for test-suite/failure/universes2.vGravatar herbelin2011-04-08
| | | | | | which did not test what it was supposed to test git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13970 85f007b7-540e-0410-9357-904b9bb8a0f7
* Replaced printing number of ill-typed branch by printing name of constructorGravatar herbelin2011-04-08
| | | | | | | when a "match" is kernel-ill-typed (probably rarely visible from end user anyway but useful for debugging) + dead code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13969 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed "Eval ... in t" when t has still metavariables.Gravatar herbelin2011-04-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13968 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 04:43:45 +0000