aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2011-06-12Rather quick hack to avoid using notations involving "Type" whenherbelin
Universes Printing is on. Code of Topconstr.match_ becomes a bit cluttered, used abbreviation to shorten it (just) a little. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14189 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-11Coqide now need lablgtk2.14.0pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14188 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-10Updated CHANGES (info, Show Script, rephrasing).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14187 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-10Moved allow_K to a unification flagherbelin
- seized the opportunity to align unification flags for functional induction to the ones of induction - also tried to add delta in the elim_flags used in tactics.ml - also tried to unify the rewrite flags in concl or in hyp (removed allow_K in hyps) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14186 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-10Fixing another bug with "_" intro pattern.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14185 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-10Fixing the "buggy" first_name and prepare multi-induction.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14184 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-10Made use of "_" in repeated use of intros_patterns work (withherbelin
application to "destruct t as (_,H)" in the dependent case, and so on). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14183 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-10Integrating onLastHypId into intro so that we can get the introductionherbelin
name even when the hyp has not been introduced at the top of the context. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14182 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-10Call process_vernac_interp_error before calling Errors.print inherbelin
plugins so that errors are indeed processed. Not sure this is the best way to do it. Maybe funind should use with_heavy_rollback for delimitating its use of vernac commands. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14181 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-10Coqide Menubar integration in MacOSpboutill
Because of lablgtk issues, accel_maps can't be customized well on MacOS git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14180 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 12:42:03 +0000