aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2011-06-21Follow-up concerning eqb / ltb / leb comparisonsletouzey
- All statement using reflect are made transparent. (Otherwise, since reflect isn't in Prop, extraction complains now about opaque Type definition). - remove two local Peqb_spec and Neqb_spec, now provided globally as Pos.eqb_spec and N.eqb_spec. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14232 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-21Cleaning debugging printer relative to new proof engine. Inherbelin
particular, new printer for evar_map which displays undefined evars + defined evars that were instantiated by these undefined evars and recursively, up to some arbitrary level n chosen to be in practice n=2 (thanks to Arnaud). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14231 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-20Some migration of results from BinInt to Numbersletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14230 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-20Zcompare.destr_zcompare subsumed by case Z.compare_specletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14229 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-20Clean-up of Zcompare and Zorderletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14228 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-20Arithemtic: more concerning compare, eqb, leb, ltbletouzey
Start of a uniform treatment of compare, eqb, leb, ltb: - We now ensure that they are provided by N,Z,BigZ,BigN,Nat and Pos - Some generic properties are derived in OrdersFacts.BoolOrderFacts In BinPos, more work about sub_mask with nice implications on compare (e.g. simplier proof of lt_trans). In BinNat/BinPos, for uniformity, compare_antisym is now (y ?= x) = CompOpp (x ?=y) instead of the symmetrical result. In BigN / BigZ, eq_bool is now eqb In BinIntDef, gtb and geb are kept for the moment, but a comment advise to rather use ltb and leb. Z.div now uses Z.ltb and Z.leb. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14227 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-20Some simplifications in NZDomainletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14226 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-20Add compatibility option "-compat 8.3".herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14225 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-20Fixing two typos introduced in r14217 and r14223herbelin
(due to unreverted debugging stuff): - wrong revert of betaiota flag to false in r14223 - wrong exception raised in r14217 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14224 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-19Ensured that the transparency state is used when flag betaiota is on for apply.herbelin
+ small typo fix in r14217 + added compatibility of betaiota flag with 8.3 when "-compat 8.3" is given git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14223 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-18Relaxed the constraint introduced in r14190 that froze the existingherbelin
evars when rewriting. Use it for autorewrite and subst. Accept evars instantiation in multi_rewrite so that rewrite alone remains compatible (it is used in contribs, e.g. Godel, in places where it does not seem absurd to allow it), but there are no good reason for it. Comments welcome. + addition of some tests for rewriting (one being related to commit 14217) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14222 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-18Generalizing flag use_evars_pattern_unification into a flagherbelin
use_pattern_unification common for evars and metas. As a compensation, add a flag use_meta_bound_pattern_unification to restore the old mechanism of pattern unification for metas applied to rels only (this is used e.g. by auto). Not sure yet, what could be the most appropriate set of flags. Added documentation of the flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14221 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-18Activating flags betaiota by default for applyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14220 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-18r14204 and 14218 continued: completely removing test for bug #2490,herbelin
leaving the decision of what to do with it to Matthieu; sorry for the confusion. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14219 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-18Partial backtrack on wrong r14204: bug #2490 still open.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14218 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-18The ad hoc version for first-order unification at toplevel of "?n argsherbelin
= t" introduced in r14199 (w_typed_unify_list) tried to check types of metas more than what w_typed_unify used to before (and these types need delta to be convertible). Don't know if it is a weakness of the test for checking types but since checking types should not be necessary here, w_typed_unify_list now follows what w_unify_core_0 does more closely. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14217 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-18Typo in CHANGESherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14216 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-18add names of theorems in outputjnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14215 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-17Customized accelerator maps for macos are globally installed (end to fix 2462)pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14214 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-17Fix 2516: Utf8 font in Coqide Command panelpboutill
Not perfect, font of unactives command panels won't change on the fly. (As it is for others GtextArea.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14213 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-17Fix bug 2269, program typechecker not used in Instance conclusionsmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14212 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-16refman nsatzpottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14211 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-16Tests de nsatz avec la geometriepottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14210 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-15git rebase -i mess consequencepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14209 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-14Revert "Coqide now need lablgtk2.14.0" + Ide build system debuggingpboutill
We can be easily substitute Gdk.Windowing by a glance of configure work... This reverts commit 8b6f6b1c4b60e74dccd5d8c49bdd433e19d53bf4. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14208 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-14Making printing of backtick in Program reparsable (avoiding collision with "`(")herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14205 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-14Regression files for bugs #2304 and #2490.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14204 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-14Fixing bug #2181 (Class mechanism can create dependencies over unnamedherbelin
fields of records). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14201 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-13A few comments and a dev file to summarize issues with unificationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14200 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-13Added full pattern-unification on Meta for tactic unification.herbelin
No way to control it yet; maybe flag use_evars_pattern_unification should be generalized for that purpose. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14199 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-13Added a flag to restrict conversion in tactic unification on theherbelin
strict subterms of the initial unification problem (inspired from ssreflect rewriting strategy). Not activated however (a few applications of setoid rewrite use this possibility on closed terms in the stdlib, e.g. "flip le p (min n m)" identified with "le (min n m) p"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14198 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-13Another bug of Scheme Induction (generated names dep/nodep were swapped).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14195 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-13Fixing an anomaly in Scheme Induction.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14193 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-12Oups, typo in previous commitherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14192 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-12Removed what looks like a (very old) useless f.o. unification passherbelin
made after s.o. unification succeeds. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14191 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-12Added a new flag for freezing evars in tactic unification. Used thisherbelin
flag to forbid rewriting tactics to instantiate an evar of the goal while looking for subterms (this is not clear that we always want that for rewrite but we certainly want it for autorewrite; see comments by Charguéraud on coqdev Oct 2010). In a few cases in the theories, a pre-existing evar of an hyp used for rewriting is instantiated by the rewriting step. Let's accept this at the current time. We have to make progress towards documenting and stabilizing the strategy for matching/unifying subterms in rewrite/induction/set... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14190 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 16:41:53 +0000