aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* kernel conversion and reduction do not raise assert failure on ill-typed ↵Gravatar barras2010-07-29
| | | | | | 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
* test-case for bug #2105Gravatar barras2010-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13352 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed bug #2105 (compilation of free de Bruijn) and missing lift of ↵Gravatar barras2010-07-29
| | | | | | predicate in branch read-back (2) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13350 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed bug #2105 (compilation of free de Bruijn) and missing lift of ↵Gravatar barras2010-07-29
| | | | | | predicate in branch read-back git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13349 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2209, don't use the fragile argument name "y" to pass theGravatar msozeau2010-07-28
| | | | | | | missing argument to a transitivity call. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13347 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rewrite Heap merging so that it extracts to an O(n log n) definition.Gravatar msozeau2010-07-28
| | | | | | | Fixes bug #2047. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13345 85f007b7-540e-0410-9357-904b9bb8a0f7
* unification des tactiques nsatz pour R Z avec celle des anneaux integresGravatar pottier2010-07-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13343 85f007b7-540e-0410-9357-904b9bb8a0f7
* oops. commited files I shouldn't have. reverting on r13341Gravatar barras2010-07-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13342 85f007b7-540e-0410-9357-904b9bb8a0f7
* ported r13340 to trunkGravatar barras2010-07-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13341 85f007b7-540e-0410-9357-904b9bb8a0f7
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13338 ↵Gravatar pottier2010-07-28
| | | | 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed bug #2139: compiled cofix loops, missing offset to evaluate cofix bodiesGravatar barras2010-07-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13337 85f007b7-540e-0410-9357-904b9bb8a0f7
* nstaz pour les anneaux integres et les setoides, R Z et QGravatar pottier2010-07-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13336 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix computation of fix annotation index: only consider assumptions andGravatar msozeau2010-07-27
| | | | | | | 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
* Minor fixes:Gravatar msozeau2010-07-27
| | | | | | | | | - 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
* Documentation of Set Automatic Coercions Import.Gravatar herbelin2010-07-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13327 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix installation of emacs filesGravatar glondu2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13325 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated COPYRIGHT file and header. Improved and fixed header updater.Gravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13322 85f007b7-540e-0410-9357-904b9bb8a0f7
* correcting a bug in funind introduced in r 13292Gravatar jforest2010-07-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13320 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix a bug found by S.Glondu. coq-db.el did not compile.Gravatar courtieu2010-07-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13319 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some fine-tuning after removal of automatic imports of coercions in r13310Gravatar herbelin2010-07-23
| | | | | | | | | | | - 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
* Made notations for exists, exists! and notations of Utf8.v recursive notationsGravatar herbelin2010-07-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13317 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
| | | | | | | | | | | | | - 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
* Simplified the way internalization_data (i.e. bindings of bound varsGravatar herbelin2010-07-22
| | | | | | | 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
* Constrintern: unified push_name_env and push_loc_name_env; madeGravatar herbelin2010-07-22
| | | | | | | | | | 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
* Constrintern: Moved section about binders before section about notationGravatar herbelin2010-07-22
| | | | | | 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
* Switch to American spelling for "internalise" and "internalisation"Gravatar herbelin2010-07-22
| | | | | | (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
* Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).Gravatar herbelin2010-07-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13311 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made coercions active only when modules are imported.Gravatar herbelin2010-07-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13310 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backported r13308 (ConstructiveEpsilon.v) to branch v8.3Gravatar herbelin2010-07-22
| | | | | | 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
* Update of ConstructiveEpsilon.v by Jean-François Monin.Gravatar herbelin2010-07-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13308 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding the destauto tactic, that reduces match by destructing matchedGravatar courtieu2010-07-22
| | | | | | | term. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13307 85f007b7-540e-0410-9357-904b9bb8a0f7
* ported bug fix r13290 to checkerGravatar barras2010-07-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13304 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix for bug #2350 was really too quick. Here is a version that works better.Gravatar herbelin2010-07-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13303 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backporting fix to bug #2353 (fixpoint with recursively non-uniformGravatar herbelin2010-07-21
| | | | | | parameters) to branch 8.2. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13302 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quick fix for bug #2350 (ensuring enough "red" when refine calls fix tactic).Gravatar herbelin2010-07-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13301 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applied Pierre Letouzey's patch restoring Convert_concl VM casts in new proofGravatar herbelin2010-07-21
| | | | | | engine. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13300 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a bug in list_forall2eq (wrong exception was caught).Gravatar herbelin2010-07-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13298 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed parsing of "Generalizable Variable A" ("Variable" turns to be a keyword).Gravatar herbelin2010-07-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13295 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reverted 13293 commited mistakenly. Sorry for the noise.Gravatar herbelin2010-07-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13294 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tentative de suppression de l'import automatique des hints et coercions.Gravatar herbelin2010-07-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13293 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amelioration dans FunctionGravatar jforest2010-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13292 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed (serious) bug #2353: non-recursive parameters of nested inductive ↵Gravatar barras2010-07-16
| | | | | | types were seen as real constructor arguments... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13290 85f007b7-540e-0410-9357-904b9bb8a0f7
* removed a potentially dangerous try ... with _ -> ...Gravatar barras2010-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13289 85f007b7-540e-0410-9357-904b9bb8a0f7
* MSetPositive: mention MSetInterface instead of FSetInterfaceGravatar letouzey2010-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13288 85f007b7-540e-0410-9357-904b9bb8a0f7
* FSetPositive: sets of positive inspired by FMapPositive.Gravatar letouzey2010-07-16
| | | | | | | | | | Contributed by Alexandre Ren, Damien Pous, and Thomas Braibant. I've also included a MSets version, hence FSetPositive might become soon a mere wrapper for MSetPositive, as for other FSets implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13287 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bool: shorter and more systematic proofs + an iff lemma about eqbGravatar letouzey2010-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13286 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed bug #2316 (ring_simplify)Gravatar barras2010-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13284 85f007b7-540e-0410-9357-904b9bb8a0f7
* Be more clever when trying to find out the relation inGravatar msozeau2010-07-15
| | | | | | | | reflexivity/symmetry/transitivity, reabstracting arguments if necessary. Makes instances on [_ <> _] work. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13283 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: fix a bit the extraction under modulesGravatar letouzey2010-07-15
| | | | | | | | | | | | | | | | | | Extraction under modules is highly experimental, and just work a bit. Don't expect too much of it. With this commit, I simply avoid a few "assert false" to occur when we are under modules. But things are still quite wrong, for instance with: Definition foo. Module M. Definition bar := foo. Recursive Extraction bar. Extraction of bar is ok, but foo isn't displayed, since extraction can't get it: Lib.contents_after doesn't mention it, it is probably in some frozen summary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13281 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 08:11:41 +0000