aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2011-06-07- Fix restrict_hyps to not allow filtering on a variable required to ↵msozeau
typecheck the evar's conclusion - Prevent extend_evar from creating ill-formed evars with de Bruijn-open conclusions. - Minor fix of define_evars_as_lambda, another mixup of named and de Bruijn indices. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14163 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-06Typo.gmelquio
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14162 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-26Mini-test for etaherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14160 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-26Partial fix for accepting bound variables with same name as implicitherbelin
parameters of inductive types when these variables cannot bind the conclusion of the inductive type (done for "return" predicates but still to be done for non strictly positive binding occurrence, as e.g. in "Set Implicit Arguments. Inductive I A:A->Prop:=C a:(forall A, A)->I a." which should morally be accepted but is not). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14159 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-26Check if recursive calls are guarded before printing "Proof completed".herbelin
(G_decl_mode.pr_open_subgoals still not reactivated...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14158 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-26Fixing discriminate for identity.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14157 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-25Q2R -> IQRfbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14155 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-24Made the emacs-U option deprecated. Also removed the old codecourtieu
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
2011-05-24Applying Enrico Tassi's patch for giving priority to delta over eta inherbelin
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
2011-05-23git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14152 ↵fbesson
85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-23ported r14149 from v8.3 branch: bug in checker (redefined global)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14150 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-21Restore display of notation when printing an inductive such as sigletouzey
+ 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
2011-05-20added support to handle division by a constant over Rfbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14147 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-19Remove useless "open Gc"glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14146 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-19Remove System.process_time (dead code)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14145 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-19Extraction: avoid lots of late mind_of_knletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14142 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-19Extraction: global reference should be indexed on their user part (fix #2540)letouzey
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
2011-05-18cbv delta - [...] before calling liafbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14140 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-18apply zeta reduction before syntaxificationfbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14139 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-18Extraction: avoid printing of Recursive Extraction in coqide's consoleletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14138 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-18Coqide: allow the use of Abort (grant wish #2357)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14136 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-17Class_tactics: Pervasives.(=) don't work for named_context_val (fix ATBR)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14135 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-17Modops: the strengthening functions can work without any env argumentletouzey
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
2011-05-17More work on error handlingletouzey
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
2011-05-17Add simple test of bullet behaviour.aspiwack
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
2011-05-17Break circular dependency Proof_global -> Vernacexpr -> Proof_global.aspiwack
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
2011-05-17Fixes bug in [maximal_unfocus] introduced in r14120.aspiwack
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
2011-05-16Repair the "Fail" command after recent changes in exception handlingletouzey
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
2011-05-16test-suite: no more ..._beq in the output of the search testsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14128 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-16Fix order in Search tests.letouzey
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
2011-05-16Fixed my last patch: these files no longer use nat_beq (automaticallyvsiles
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
2011-05-16turn the automatic generation of boolean equalityvsiles
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
2011-05-15Test for bug 462 and 2342 fixed by Matthieu's 13990 (or so).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14124 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-15Failing instead of switching to the coercion mechanism when VMcastherbelin
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
2011-05-15Turning Sys_error into error by default instead of anomaly. After all,herbelin
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
2011-05-13A better procedure for checking presence of undefined evars.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14121 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-13The modules in proofs now use the Errors module to explain their exceptions ↵aspiwack
to the toplevel git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14120 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-13A new mechanism to handle errors.aspiwack
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
2011-05-13New option [Set Bullet Behavior] allows to select the behaviour of bullets.aspiwack
- 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
2011-05-11Print Module (Type) M now tries to print more detailsletouzey
"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
2011-05-09Improved lia + experimental nliafbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14116 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-09remove useless dependancy for csdpcertfbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14115 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-06Fixes in the test-suite after modularisation of ZArith and coletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14114 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-06Additionnal fix of romega after modularisation of ZArithletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14113 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-06update of the file list in doc/stdlibletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14112 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-05BinNat: N.binary_rect is now a definition instead of an opaque proofletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14111 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-05Peano recursion for positive: integration of Daniel Schepler's codeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14110 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-05Minimal lemmas about Z.gt, N.gt and coletouzey
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
2011-05-05Modularisation of Znat, a few name changed elsewhereletouzey
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
2011-05-05BinInt: Z.add become the alternative Z.add'letouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 19:05:53 +0000