aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2011-06-10no more errors at _stubs.c.d generationpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14179 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-10Menubar and toolbar in coqide using GtkUI & Gactions.pboutill
You'll need to remove/edit your ~/.coqiderc and ~/.coqide.keys. As it used to be, accelerator modifiers changes are only done after a reboot but we need more binding in lablgtk to improve that... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14178 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-10Revert "Check if recursive calls are guarded before printing "Proof completed"."pboutill
because guard condition is checked at Qed anyway and it can be expensivise to check it twice. Use explicitly "Guarded" if you want this information. But the wrong proof completed is now the right no more subgoals ... Of course, we would like an incrementally checked guard condition one day ! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14177 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-10Fixes in pruning, do not fail if pruning is impossible due to typing ↵msozeau
constraints but postpone evar-evar problems git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14176 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-10ring2, cring, nsatz avec type classe avec parametres plus notationspottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14175 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-09More fixes in pruning/restriction of evars during unification.msozeau
- Do not allow to filter variables that appear in the conclusion of an evar. - Do not attempt to restrict evars based on a substitution that does not contain only evars (fall back to the pattern fragment and do not lose solutions). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14174 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-08Make Notation works with anonymous-level "Type".herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14170 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-08Fixes in pruning in unification.msozeau
Properly normalize evars to reflect the already pruned evars in the type of dependent evars to allow more precise restriction of hyps. Directly check the type of an evar instance, allowing backtracking on ill-typed instanciations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14169 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-07Fix bug #2399 in Program: used to build an ill-formed term due to a de ↵msozeau
Bruijn bug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14168 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-07Fix bug #2335, fail if the search for reflexivity/symmetry/transitivity ↵msozeau
proofs create unsolved evars git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14167 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-07Catch AbstractionOverMeta as a unification failure in precatchable_exception.msozeau
Allows rewrite H in * |- to work in case a rewrite throws this exception. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14166 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-07Fix bug #2415: warn when closing modules or sections and some obligations ↵msozeau
are unresolved git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14165 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-07Fixed bug #2398: destruct ex2/sig2/sigT2 in Program, patch by Paolo Herms.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14164 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 15:49:58 +0000