aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2010-08-27* library/Library: Remove the use of the old-fashioned lighten_library.regisgia
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13376 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-08-27* library/Library: Remove lighten_library definition.regisgia
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13375 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-08-26Fix an error message ot having the ERror: prefix.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13373 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-08-03Export printing functions for extra arguments. Maybe there's a way tomsozeau
get them from the grammar entries? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13369 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-08-02Fix [clenv_missing] to compute a better approximation of missingmsozeau
dependent arguments. It breaks compatibility as some [apply with] clauses are not necessary anymore. Typically when applying [f_equal], the domain type of the function can be infered even if it does not appear directly in the conclusion of the goal. Fixes bug #2154. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13367 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-31Fixed commit r13359 which was incomplete for its "trunk" part. Thanksherbelin
to Julien for noticing it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13366 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-30adpated the checker to handle coomutative cuts and lazynessbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13365 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-30Removed information in COMPATIBILITY that were intended before all forherbelin
developers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13364 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-30better fix to bug #2319: types are compiled in the env of the bodiesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13362 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-30Updated test on Nsatz after Loïc moved NsatzR to Nsatz.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13361 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-30Capitulation wrt "change pat with term": instead of solving theherbelin
problem raised by taral on coq-club Goal forall X : Prop, X -> False -> False. intro. change (?t -> False) with (not t). we just fail with an error message of "mauvaise foi". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13360 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-30r13359 continued: removed native treatment for λ (lambda) and Π (Pi)herbelin
what frees the tokens for other uses in non-unicode mode. For Π, users will have to introduce their own recursive notation. For λ, this is provided by the -unicode option (which actually is not documented nor as an option nor in the reference manual; maybe it should simply be now removed since "Require Import Utf8_core" has the same effect). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13359 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-29Rather quick hack to make basic unicode notations available byherbelin
requiring a file Utf8_core. That needs to be improved... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13358 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-29Fixed a bug introduced (r13316/r13329) in the printing of notationsherbelin
with non-recursive binders. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13357 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-29kernel conversion and reduction do not raise assert failure on ill-typed ↵barras
terms, but an anomaly instead. It is caught in pretyping git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13353 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-29test-case for bug #2105barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13352 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-29fixed bug #2105 (compilation of free de Bruijn) and missing lift of ↵barras
predicate in branch read-back (2) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13350 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-29fixed bug #2105 (compilation of free de Bruijn) and missing lift of ↵barras
predicate in branch read-back git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13349 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-28Fix bug #2209, don't use the fragile argument name "y" to pass themsozeau
missing argument to a transitivity call. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13347 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-28Rewrite Heap merging so that it extracts to an O(n log n) definition.msozeau
Fixes bug #2047. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13345 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-28unification des tactiques nsatz pour R Z avec celle des anneaux integrespottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13343 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-28oops. commited files I shouldn't have. reverting on r13341barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13342 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-28ported r13340 to trunkbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13341 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-28git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13338 ↵pottier
85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-28fixed bug #2139: compiled cofix loops, missing offset to evaluate cofix bodiesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13337 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-27nstaz pour les anneaux integres et les setoides, R Z et Qpottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13336 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-27Fix computation of fix annotation index: only consider assumptions andmsozeau
not let-ins in the binding list. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13335 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-27Minor fixes:msozeau
- Document and fix [autounfold] - Fix warning about default Firstorder tactic object not being defined - Fix treatment of implicits in Program Lemma. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13334 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-25Documentation of Set Automatic Coercions Import.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13327 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-24Fix installation of emacs filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13325 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-24Updated all headers for 8.3 and trunkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-24Updated COPYRIGHT file and header. Improved and fixed header updater.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13322 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-23correcting a bug in funind introduced in r 13292jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13320 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-23Fix a bug found by S.Glondu. coq-db.el did not compile.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13319 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-23Some fine-tuning after removal of automatic imports of coercions in r13310herbelin
- Moved Global Set from Keep to Substitute to ensure it is activated in real time and not only after the main parts of the module - Renamed Importation into Import in option name - Made "Print Libraries" prints the modules in the importation order (which is the most relevant order for non-commutative declarations) instead of load order git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13318 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-22Made notations for exists, exists! and notations of Utf8.v recursive notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13317 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-22Extension of the recursive notations mechanismherbelin
- Added support for recursive notations with binders - Added support for arbitrary large iterators in recursive notations - More checks on the use of variables and improved error messages - Do side-effects in metasyntax only when sure that everything is ok - Documentation Note: it seems there were a small bug in match_alist (instances obtained from matching the first copy of iterator were not propagated). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13316 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-22Simplified the way internalization_data (i.e. bindings of bound varsherbelin
to their signature of implicit positions and scopes) is computed. A bit of documentation in constrintern.mli. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13315 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-22Constrintern: unified push_name_env and push_loc_name_env; madeherbelin
location dumping for binders uniformly treated in constrintern.ml (and renamed the optional arg of interp_context from fail_anonymous to global_level since the flag now also decides whether to dump binders as global or local ones); added locations for the variables occurring in the "as in" clauses; git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13314 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-22Constrintern: Moved section about binders before section about notationherbelin
in preparation of supporting parameters for binders in notations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13313 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-22Switch to American spelling for "internalise" and "internalisation"herbelin
(hence following the general convention about spelling in Coq's code). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13312 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-22Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13311 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-22Made coercions active only when modules are imported.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13310 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-22Backported r13308 (ConstructiveEpsilon.v) to branch v8.3herbelin
Also removed trailing spaces of the file git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13309 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-22Update of ConstructiveEpsilon.v by Jean-François Monin.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13308 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-22Adding the destauto tactic, that reduces match by destructing matchedcourtieu
term. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13307 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-22ported bug fix r13290 to checkerbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13304 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-21Fix for bug #2350 was really too quick. Here is a version that works better.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13303 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-21Backporting fix to bug #2353 (fixpoint with recursively non-uniformherbelin
parameters) to branch 8.2. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13302 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-21Quick fix for bug #2350 (ensuring enough "red" when refine calls fix tactic).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13301 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 14:03:40 +0000