aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2010-08-27* kernel/Safe_typing.LightenLibrary:regisgia
Fix an incorrect initialization of the index counter. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13386 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-08-27* (checker|kernel)/Safe_typing:regisgia
Rename "lighten_*" into "traverse_*" inside the [traverse_library] function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13385 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-08-27* (checker|kernel)/Safe_typing:regisgia
Fix a bug in traverse_library. The extraction was not satisfied with [mod_expr] set to [None]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13384 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-08-27* toplevel/Coqtop: Reactivate -dont-load-proofs option.regisgia
(This is simply the default behavior from now.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13383 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-08-27* library/Library: Reformulate a comment.regisgia
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13382 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-08-27* library/Library: Document.regisgia
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13381 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-08-27* checker/SafeTyping kernel/SafeTyping:regisgia
Fix typos. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13380 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-08-27* lib/Flags: Replace dont_load_proofs by load_proofs since not loadingregisgia
proofs is now the default behavior of coqtop. * lib/Coqtop: Update accordingly. * checker/Check library/Library: Pass the right "load_proofs" flag to LightenLibrary.load. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13379 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-08-27* Improve documentation of LightenLibrary.regisgia
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13378 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-08-27* (checker|kernel)/Safe_typing: New LightenLibrary.regisgia
This module introduces an indirection behind opaque const_body to enable the optional demarshalling of them. * library/Library checker/Check: Use LightenLibrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13377 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 16:26:32 +0000