aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Made the emacs-U option deprecated. Also removed the old codeGravatar courtieu2011-05-24
| | | | | | | | | inserting special chars for proof by pointing with emacs. This was interacting badly with utf8. It may be implemented back with xml-like tags instead of special chars. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14154 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applying Enrico Tassi's patch for giving priority to delta over eta inGravatar herbelin2011-05-24
| | | | | | | unification (evarconv.ml). Works better for compiling math. comp. library while seems ok on other examples. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14153 85f007b7-540e-0410-9357-904b9bb8a0f7
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14152 ↵Gravatar fbesson2011-05-23
| | | | 85f007b7-540e-0410-9357-904b9bb8a0f7
* ported r14149 from v8.3 branch: bug in checker (redefined global)Gravatar barras2011-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14150 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restore display of notation when printing an inductive such as sigGravatar letouzey2011-05-21
| | | | | | + minor pp improvement for Print Module Type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14148 85f007b7-540e-0410-9357-904b9bb8a0f7
* added support to handle division by a constant over RGravatar fbesson2011-05-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14147 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove useless "open Gc"Gravatar glondu2011-05-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14146 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove System.process_time (dead code)Gravatar glondu2011-05-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14145 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: avoid lots of late mind_of_knGravatar letouzey2011-05-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14142 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: global reference should be indexed on their user part (fix #2540)Gravatar letouzey2011-05-19
| | | | | | | | | Since in Extract_env we recreate constant and mind whose canonical part might be inaccurate, we shouldn't use an Hashtbl on global_reference derived from these constant and mind, otherwise equivalent refs could be considered distinct. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14141 85f007b7-540e-0410-9357-904b9bb8a0f7
* cbv delta - [...] before calling liaGravatar fbesson2011-05-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14140 85f007b7-540e-0410-9357-904b9bb8a0f7
* apply zeta reduction before syntaxificationGravatar fbesson2011-05-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14139 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: avoid printing of Recursive Extraction in coqide's consoleGravatar letouzey2011-05-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14138 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: allow the use of Abort (grant wish #2357)Gravatar letouzey2011-05-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14136 85f007b7-540e-0410-9357-904b9bb8a0f7
* Class_tactics: Pervasives.(=) don't work for named_context_val (fix ATBR)Gravatar letouzey2011-05-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14135 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modops: the strengthening functions can work without any env argumentGravatar letouzey2011-05-17
| | | | | | | The env was used for a particular case of Cbytegen.compile_constant_body, but we can actually guess that it will answer a particular BCallias con. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14134 85f007b7-540e-0410-9357-904b9bb8a0f7
* More work on error handlingGravatar letouzey2011-05-17
| | | | | | | | | | | | | | Anomalies are now meant to be the exceptions that are *not* catched and handled by the new Errors.handle_stack. Three variants of [Errors.print] allow to customize how anomalies are treated. In particular, [Errors.print_no_anomaly] is used for the Fail command, instead of a classification function Cerrors.is_user_error which wasn't customizable. No more AnomalyOnError, its only occurrence is now a regular anomaly git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14133 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add simple test of bullet behaviour.Gravatar aspiwack2011-05-17
| | | | | | | Signed-off-by: Tom Prince <tom.prince@ualberta.net> Signed-off-by: Arnaud Spiwack <arnaud@spiwack.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14132 85f007b7-540e-0410-9357-904b9bb8a0f7
* Break circular dependency Proof_global -> Vernacexpr -> Proof_global.Gravatar aspiwack2011-05-17
| | | | | | Fixes bug #2547 ( http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2547 ) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14131 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes bug in [maximal_unfocus] introduced in r14120.Gravatar aspiwack2011-05-17
| | | | | | Fixes bug #2546 ( http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2546­ ). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14130 85f007b7-540e-0410-9357-904b9bb8a0f7
* Repair the "Fail" command after recent changes in exception handlingGravatar letouzey2011-05-16
| | | | | | | | | | | | For that, I introduce a explicit classification function is_user_error : exn -> bool, instead of the previous hack of explain_exn_default_aux (fun () -> raise e). By the way, clean a bit explain_exn_default_aux : many cases are just printed fine by default's Printexn.to_string (for example Not_found). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14129 85f007b7-540e-0410-9357-904b9bb8a0f7
* test-suite: no more ..._beq in the output of the search testsGravatar letouzey2011-05-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14128 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix order in Search tests.Gravatar letouzey2011-05-16
| | | | | | Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14127 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed my last patch: these files no longer use nat_beq (automaticallyGravatar vsiles2011-05-16
| | | | | | | | generated) but rather use beq_nat (Arith.EqNat) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14126 85f007b7-540e-0410-9357-904b9bb8a0f7
* turn the automatic generation of boolean equalityGravatar vsiles2011-05-16
| | | | | | | | off, as it should be since 8.3 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14125 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test for bug 462 and 2342 fixed by Matthieu's 13990 (or so).Gravatar herbelin2011-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14124 85f007b7-540e-0410-9357-904b9bb8a0f7
* Failing instead of switching to the coercion mechanism when VMcastGravatar herbelin2011-05-15
| | | | | | involves evars (seem cleaner) at type-inference time. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14123 85f007b7-540e-0410-9357-904b9bb8a0f7
* Turning Sys_error into error by default instead of anomaly. After all,Gravatar herbelin2011-05-15
| | | | | | | they are in general internal Coq error. If a Coq code needs to catch a Sys_error for some purpose, it can still do it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14122 85f007b7-540e-0410-9357-904b9bb8a0f7
* A better procedure for checking presence of undefined evars.Gravatar aspiwack2011-05-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14121 85f007b7-540e-0410-9357-904b9bb8a0f7
* The modules in proofs now use the Errors module to explain their exceptions ↵Gravatar aspiwack2011-05-13
| | | | | | to the toplevel git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14120 85f007b7-540e-0410-9357-904b9bb8a0f7
* A new mechanism to handle errors.Gravatar aspiwack2011-05-13
| | | | | | | Instead of the monolitic Cerrors, I introduce a lightweight Errors module whose error message can be expanded by module introducing exceptions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14119 85f007b7-540e-0410-9357-904b9bb8a0f7
* New option [Set Bullet Behavior] allows to select the behaviour of bullets.Gravatar aspiwack2011-05-13
| | | | | | | | | - Two predefined behaviours : "None" where bullet have no effect and "Strict Subproofs" (default) which acts as previously. - More behaviours can be registered by plugins via [Proof_global.Bullet.register_behavior]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14118 85f007b7-540e-0410-9357-904b9bb8a0f7
* Print Module (Type) M now tries to print more detailsGravatar letouzey2011-05-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | "Print Module M" prints now by default both a signature (fields with their types) and a body (fields with their types and transparent bodies). "Print Module Type M" could be used both when M is a module or a module Type, it will only display th signature of M. The earlier minimalist behavior (printing only the field names) could be reactivated by option "Set Short Module Printing". For the moment, the content of internal sub-modules and sub-modtypes are not displayed. Note: this commit is an experiment, many sitations are still unsupported. When such situations are encountered, Print Module will fall back on the earlier minimalist behavior. This might occur in particular in presence of "with" annotations, or in the conjonction of a non-global module (i.e. functor or module type) and internal sub-modules. Side effects of this commit: - a better compare function for global_reference, with no allocations at each comparison - Nametab.the_globrevtab is now searched according to user part only of a kernel_name - The printing of an inductive block is now in Printer, and rely less on the Nametab. Instead, we use identifiers in mind_typename and mind_consnames. Note that Print M.indu will not display anymore the pseudo-code "Inductive M.indu ..." but rather "Inductive indu..." git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14117 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved lia + experimental nliaGravatar fbesson2011-05-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14116 85f007b7-540e-0410-9357-904b9bb8a0f7
* remove useless dependancy for csdpcertGravatar fbesson2011-05-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14115 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes in the test-suite after modularisation of ZArith and coGravatar letouzey2011-05-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14114 85f007b7-540e-0410-9357-904b9bb8a0f7
* Additionnal fix of romega after modularisation of ZArithGravatar letouzey2011-05-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14113 85f007b7-540e-0410-9357-904b9bb8a0f7
* update of the file list in doc/stdlibGravatar letouzey2011-05-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14112 85f007b7-540e-0410-9357-904b9bb8a0f7
* BinNat: N.binary_rect is now a definition instead of an opaque proofGravatar letouzey2011-05-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14111 85f007b7-540e-0410-9357-904b9bb8a0f7
* Peano recursion for positive: integration of Daniel Schepler's codeGravatar letouzey2011-05-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14110 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minimal lemmas about Z.gt, N.gt and coGravatar letouzey2011-05-05
| | | | | | | The use of these predicate isn't recommended, but let's at least allow converting > >= and < <= git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14109 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modularisation of Znat, a few name changed elsewhereGravatar letouzey2011-05-05
| | | | | | For instance inj_plus is now Nat2Z.inj_add git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14108 85f007b7-540e-0410-9357-904b9bb8a0f7
* BinInt: Z.add become the alternative Z.add'Gravatar letouzey2011-05-05
| | | | | | | It relies on Z.pos_sub instead of a Pos.compare followed by Pos.sub. Proofs seem to be quite easy to adapt, via some rewrite Z.pos_sub_spec. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14107 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modularization of BinInt, related fixes in the stdlibGravatar letouzey2011-05-05
| | | | | | | | | | | All the functions about Z is now in a separated file BinIntDef, which is Included in BinInt.Z. This BinInt.Z directly implements ZAxiomsSig, and instantiates derived properties ZProp. Note that we refer to Z instead of t inside BinInt.Z, otherwise ring breaks later on @eq Z.t git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14106 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modularization of NnatGravatar letouzey2011-05-05
| | | | | | | | For instance, nat_of_Nplus is now N2Nat.inj_add Note that we add an iter function in BinNat.N git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14105 85f007b7-540e-0410-9357-904b9bb8a0f7
* Setoid_ring: some cleanups related with BinPos and BinNatGravatar letouzey2011-05-05
| | | | | | | In particular, positive_eq and N_eq and Neq_bool are now Pos.eqb and N.eqb git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14104 85f007b7-540e-0410-9357-904b9bb8a0f7
* Wf.iter_nat becomes Peano.nat_iter (with an implicit arg)Gravatar letouzey2011-05-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14103 85f007b7-540e-0410-9357-904b9bb8a0f7
* BinNatDef containing all functions of BinNat, misc adaptations in BinPosGravatar letouzey2011-05-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14102 85f007b7-540e-0410-9357-904b9bb8a0f7
* BinPosDef: a module with all code about positive, later Included in BinPosGravatar letouzey2011-05-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14101 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modularization of BinNat + fixes of stdlibGravatar letouzey2011-05-05
| | | | | | | | | | | | A sub-module N in BinNat now contains functions add (ex-Nplus), mul (ex-Nmult), ... and properties. In particular, this sub-module N directly instantiates NAxiomsSig and includes all derived properties NProp. Files Ndiv_def and co are now obsolete and kept only for compat git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14100 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-09 10:02:03 +0000