aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Collapse)AuthorAge
* Added multiple implicit arguments rules per name.Gravatar herbelin2010-10-03
| | | | | | | | | Example: "Implicit Arguments eq_refl [[A] [x]] [[A]]". This should a priori be used with care (it might be a bit disturbing seeing the same constant used with apparently incompatible signatures). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13484 85f007b7-540e-0410-9357-904b9bb8a0f7
* Making display of various informations about constants more modular:Gravatar herbelin2010-10-03
| | | | | | | | | | | | | | - use list of non-newline-ended phrases instead of newline-separated texts because newline-separated texts does not support well being put in boxes (e.g. ''v 2 (str"a" ++ fnl()) ++ str"b" ++ fnl()'' prints "b" at indentation 2 while to get the expected output, one would have needed to have the fnl outside the box as in ''v 2 (str"a") ++ fnl() ++ str"b" ++ fnl()'' - also reason over lists of explicitly non-empty lines instead of checking for "mt" lines to skip The reason of this is to permit nesting of printing infos. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13482 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2321, allowing "_" named projections in classes. Not realizingGravatar msozeau2010-09-28
| | | | | | | | the wish to allow named projections to not be put in the canonical structures databases for Structures. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13474 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove some occurrences of "open Termops"Gravatar glondu2010-09-28
| | | | | | | Functions from Termops were sometimes fully qualified, sometimes not in the same module. This commit makes their usage more uniform. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13470 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix function applications without labels (OCaml warning 6)Gravatar glondu2010-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13469 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a bug in printing fix/cofix error messages when severalGravatar herbelin2010-09-24
| | | | | | instances of the same variable name occur. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13465 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
| | | | | | | | | | In particular, the unused lib/tlm.ml and lib/gset.ml are removed In addition, to simplify code, Libobject.record_object returning only the ('a->obj) function, which is enough almost all the time. Use Libobject.record_object_full if you really need also the (obj->'a). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13460 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing #2162 and #2367 (wrong order of Show Match) for branch 8.2 tooGravatar herbelin2010-09-18
| | | | | | | (see otherwise r12383). Seized the opportunity to remove useless (v7-style syntax) parentheses in Match printing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13433 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bugs #2347 (part 2) and #2388: error message printing was doneGravatar herbelin2010-09-18
| | | | | | | | | | | | | | | | | too late, in a global environment which was no longer the correct one, leading to the failure of error printing (hence an anomaly) in case the command modified the state in several steps. Now, errors raised by vernac commands are processed in the same (intermediate) state they were raised from, just before rolling back to the original state. that modify the state in several Now, errors raised by vernac commands that modify the state in several steps (say S1, S2, ..., Sn) are processed in the state they were produced in (S1, S2, ... Sn-1), git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13431 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE argv parsing delegated to coqtopGravatar vgross2010-09-14
| | | | | | | | | | Introduces some hacks to have a consistent user experience. When coqtop prints info on self then exit, return code is 2 if called with -filteropts, 0 else For now, no options are accepted by coqide. there is no way for now to specify a filename that begins with a dash. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13415 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix unescaped end-of-lines (OCaml warning 29)Gravatar glondu2010-09-13
| | | | | | See http://caml.inria.fr/mantis/view.php?id=4940 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13413 85f007b7-540e-0410-9357-904b9bb8a0f7
* * removed declare_constant and declare_internal_constant Gravatar vsiles2010-09-02
| | | | | | | | | | | | | | | (declare_constant_gen was not exported, leading to a lot of silly tests before calling those functions) and replaced them by declare_constant : ?internal:internal_flat -> ... declare_constant's default behaviour is the same as the old declare_constant. * fixed the default behaviour of inductive scheme failure during coq's compilation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13395 85f007b7-540e-0410-9357-904b9bb8a0f7
* v13392 port from v8.3 to trunk : correct message when defining inductive schemesGravatar vsiles2010-09-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13394 85f007b7-540e-0410-9357-904b9bb8a0f7
* * By default, load proof terms.Gravatar regisgia2010-08-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13389 85f007b7-540e-0410-9357-904b9bb8a0f7
* * scripts/Coqc toplevel/Usage:Gravatar regisgia2010-08-27
| | | | | | Export the -load-proofs officially. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13388 85f007b7-540e-0410-9357-904b9bb8a0f7
* * toplevel/Coqtop: Reactivate -dont-load-proofs option.Gravatar regisgia2010-08-27
| | | | | | (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
* * lib/Flags: Replace dont_load_proofs by load_proofs since not loadingGravatar regisgia2010-08-27
| | | | | | | | | | | 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
* Fix an error message ot having the ERror: prefix.Gravatar courtieu2010-08-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13373 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rather quick hack to make basic unicode notations available byGravatar herbelin2010-07-29
| | | | | | 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
* 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
* 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
* 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
* 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
* Amelioration dans FunctionGravatar jforest2010-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13292 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix goal display when backtrackingGravatar vgross2010-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13246 85f007b7-540e-0410-9357-904b9bb8a0f7
* Stronger checks on coqtop termination, warning when zombies.Gravatar vgross2010-07-05
| | | | | | Also, reindentation + typed_notebook simplification git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13241 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correct wrong handling of evars in instance definitions that preventedGravatar msozeau2010-06-29
| | | | | | | information going from the body to the type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13224 85f007b7-540e-0410-9357-904b9bb8a0f7
* change the flag "internal" in declare/ind_tables from bool toGravatar vsiles2010-06-29
| | | | | | | | | | | | | | a 3 state type to allow: * KernelVerbose / KernelSilent : handle the display of messages launch by Coq * UserVerbose : handle the display of messages launch by user actions Coq will still behaves the same way (TODOs in the code mark the places where we can now change the behaviour). I'll remove them in a few days when we'll have agreed on the correct behaviour. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13217 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made tclABSTRACT normalize evars before saying it does not supportGravatar herbelin2010-06-29
| | | | | | | | | | | | them. This was the cause of the failure of compilation of CyclicAxioms after "replace" starting supporting open constrs (r13206). Seized the opportunity to clean a little bit things around nf_evar, whd_evar, check_evars, etc. Removed obsolete printer mod_self_id from dev/db. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13214 85f007b7-540e-0410-9357-904b9bb8a0f7
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
| | | | | | Applied it to fix mli file headers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bug #2135 (second-order unification was raising cryptic message)Gravatar herbelin2010-06-12
| | | | | | | | | | | - made the example work (a call to whd_meta was missing) - replaced the internal error messages of w_unify_to_subterm_list into user-understandable messages - incidentally fixed the meaning of whd_meta (which now takes an evd) and meta_name (which now does what it means and do not treat differently the instantiated metas) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13122 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added regression tests for bugs + miscellaneous improvementsGravatar herbelin2010-06-12
| | | | | | | | | - #2095 (not fixed in v8.2 but fixed in v8.3 and trunk) - #2108 (fixed in v8.2, v8.3, trunk) - #2102 (moved warning to msg_warning to ensure flushing, but still open enhancement) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13121 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applying François' patch fixing grammar of uniform inheritance condition ↵Gravatar herbelin2010-06-12
| | | | | | | | message (see bug report #2331) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13120 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing spelling: pr_coma -> pr_commaGravatar herbelin2010-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13119 85f007b7-540e-0410-9357-904b9bb8a0f7
* Automatic introduction of names given before ":" in Lemma's andGravatar herbelin2010-06-09
| | | | | | | | | | Definition's is not so painless. It seems to however generally provide "nicer" scripts so let us keep it and update the contribs and test-suite accordingly. Also enforced that the actual introduced names to be exactly as given in the statements. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13097 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix treatment of {struct x} annotations in presence of generalizedGravatar msozeau2010-06-08
| | | | | | | binders. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13086 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixing error message display.Gravatar vgross2010-06-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13082 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added support for Ltac-matching terms with variables bound in the patternGravatar herbelin2010-06-06
| | | | | | | | | | | | | | | | | | - Instances found by matching.ml now collect the set of bound variables they possibly depend on in the pattern (see type Pattern.extended_patvar_map); the variables names are canonically ordered so that non-linear matching takes actual names into account. - Removed typing of matching constr instances in advance (in tacinterp.ml) and did it only at use time (in pretyping.ml). Drawback is that we may have to re-type several times the same term but it is necessary for considering terms with locally bound variables of which we do not keep the type (and if even we had kept the type, we would have to adjust the indices to the actual context the term occurs). - A bit of documentation of pattern.mli, matching.mli and pretyping.mli. - Incidentally add env while printing idtac messages. It seems more correct and I hope I did not break some intended existing behavior. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13080 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added command "Locate Ltac qid".Gravatar herbelin2010-06-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13067 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ide_blob: avoid direct use of Stdpp for compatibility with new camlp4Gravatar letouzey2010-06-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13063 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleanup: remove code specific for ocaml 3.06Gravatar letouzey2010-06-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13045 85f007b7-540e-0410-9357-904b9bb8a0f7
* restore handling of lexer errorsGravatar letouzey2010-06-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13044 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE goes multiprocessGravatar vgross2010-05-31
| | | | | | | | | | | | | | | This commit changes many things in CoqIDE, and several breakage are to be expected. So far, evaluation in standard tactic mode and backtracking seems to be working. Future work : - clean up the thread management crud remaining in ide/coqide.ml - rework the exception handling - rework the init system in Coqtop plus many other things git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13043 85f007b7-540e-0410-9357-904b9bb8a0f7
* More indirection.Gravatar vgross2010-05-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13042 85f007b7-540e-0410-9357-904b9bb8a0f7
* Introducing strong typing for IDE - toplevel IPCGravatar vgross2010-05-31
| | | | | | Obj.magic in toplevel/ide_blob.ml is the only way to simulate GADT. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13041 85f007b7-540e-0410-9357-904b9bb8a0f7
* deporting Coq specific code from ide to toplevel.Gravatar vgross2010-05-31
| | | | | | Still messy. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13040 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modifying startup sequenceGravatar vgross2010-05-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13039 85f007b7-540e-0410-9357-904b9bb8a0f7
* New pass on inductive schemesGravatar herbelin2010-05-29
| | | | | | | | | | | | | | - Made "is defined" message quiet when a tactic define (via find_scheme) a scheme for internal use (in ind_tables.ml) - Improved documentation of eqschemes.ml (and swiched l2r/r2l terminology when talking about rewriting in hypotheses) - Took benefit of the new support for commutative cuts in the fixpoint guard checker for reducing the collection of rewriting schemes needed to implement the various kinds of rewriting (dependent or not, with symmetrical equality or not, in hypotheses or in conclusion, from left-to-right or from right-to-left) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13038 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 16:39:04 +0000