aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Fixing bugs in previous commits about implicit arguments:Gravatar herbelin2010-10-04
| | | | | | | | | - fixing r13483 (supposed dead code in impargs was actually half-living: implicit arguments mode should merge with the {...} manually given implicit arguments but not with the "Implicit Arguments [...]" arguments), - fixing code of drop_first_implicits in r13484. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13490 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid raising an anomaly when an error encapsulated with a dummyGravatar herbelin2010-10-03
| | | | | | location is raised from a loaded/compiled file! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13488 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test for non-regression of the display bug fixed in r13486.Gravatar herbelin2010-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13487 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing printing of module_path names (was using a debuggingGravatar herbelin2010-10-03
| | | | | | message since r11177). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13486 85f007b7-540e-0410-9357-904b9bb8a0f7
* Using multiple lists of implicit arguments in Program for preservingGravatar herbelin2010-10-03
| | | | | | | | | | | | | | the compatibility with the rest of the theories. Used multiple lists of implicit arguments in Init only when the maximality status is not modified in Program (and thus the compatibility is strictly preserved). This improves the compatibility for the implicit arguments of eq_refl and JMeq_refl between 8.2 and 8.3 when using Program (up to the residual differences in the maximality status). For the constants Acc_inv, inl, inr, left, right, Vnil, Vcons, the compatibility with 8.2 is not improved but the consistency between Program and the rest of the library is. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13485 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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
* Dead code in impargs (afaics, no more need, since r11242, to mergeGravatar herbelin2010-10-03
| | | | | | automatic and manual implicit arguments twice). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13483 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
* Fixed a little printing bug with "About" on an undefined constant.Gravatar herbelin2010-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13481 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplify tactic(_)-bound arguments in TACTIC EXTEND rulesGravatar glondu2010-09-30
| | | | | | | | | | | | | | Arguments bound with tactic(_) in TACTIC EXTEND rules are now of type glob_tactic_expr, instead of glob_tactic_expr * tactic. Only the first component is kept, the second one can be obtained with Tacinterp.eval_tactic. Rationale: these declare parsing rules, and eval_tactic is a semantic action, and therefore should be done in the rule body instead. Moreover, having the glob_tactic_expr and its evaluation captured by these rules was quite confusing IMHO. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13480 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improve handling of metas as evars in unification (patch by Hugo)Gravatar letouzey2010-09-30
| | | | | | | Pratical situation: simple eapply foo on a goal ?123, while foo is a (forall f, exists ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13479 85f007b7-540e-0410-9357-904b9bb8a0f7
* Speed-up refine by avoiding some calls to Evd.foldGravatar letouzey2010-09-30
| | | | | | | | | | | Instead of the full Evd.fold, Evd.fold_undefined seems enough in - Evarutil.push_dependent_evars - the nf_evars call in Evarutil.evars_to_metas (we hence create a function nf_evars_undefined and use it there) This should bring back Compcert into reasonable compilation time git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13478 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
* Coqdoc patches from UPenn (thanks to C. Casinghino). This introduces theGravatar msozeau2010-09-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ability to format inference rules (delimited by [[[ ]]]) and adds some new flags. Here's the message from Chris: - coqdoc now has support for inference rules inside coqdoc comments. These should be enclosed in triple square brackets with the following format. [[[ |- t1 : Bool |- t2 : T |- t3 : T ---------------------------- (T_If) |- if t1 then t2 else t3 : T ]]] The rule's name is optional. Multiple inference rules may be included in the same [[[ ]]] block, separated by blank lines. See http://www.cis.upenn.edu/~bcpierce/sf/Stlc.html#lab469 for some examples of the output. The output will only be pretty in html - in other formats it is printed verbatim (though it shouldn't be hard to add latex support, and I may soon). - Two new coqdoc flags have been added. First, --inline-notmono causes inline code to be printed in a proportional width font (adjustable in the css file). Second, --no-glob tells coqdoc not to look for .glob files (no links will be inserted for identifiers when this flag is used). - Finally, the handling of paragraphs and whitespace around lists has been made somewhat saner. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13473 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes of 'make doc'Gravatar pboutill2010-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13472 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bvector.Vshiftin was wrong for agesGravatar pboutill2010-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13471 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
* Remove "init" label from Termops.it_mk* specialized functionsGravatar glondu2010-09-28
| | | | | | | | | | These functions are applied much more often without labels than with them (the alternate of adding the label wherever relevant changes 124 lines instead of 41). Moreover, this is more consistent with the Term module and there is no ambiguity in argument types. This commit goes towards elimination of occurrences of OCaml warning 6. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13468 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove kind_of_type, kind_of_term2 (dead code)Gravatar glondu2010-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13467 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug in implementation of setoid rewriting under cases andGravatar msozeau2010-09-27
| | | | | | | abstractions (reported by Pierre Courtieu). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13466 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
* Solving bug #2212 (unification under tuples now not allowed forGravatar herbelin2010-09-24
| | | | | | flexible types what seems a reasonable strategy). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13464 85f007b7-540e-0410-9357-904b9bb8a0f7
* Partial review of removed dead code (r13460)Gravatar herbelin2010-09-24
| | | | | | | | - The code detected unused in notation.ml revealed a bug. - In term.ml, restored a (short) useless function for consistency/symmetry of the interface. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13463 85f007b7-540e-0410-9357-904b9bb8a0f7
* Checker: remove some dead codeGravatar letouzey2010-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13462 85f007b7-540e-0410-9357-904b9bb8a0f7
* Dead code in extractionGravatar letouzey2010-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13461 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
* dev/Makefile.oug: how to run the Oug analyser, for instance for finding dead ↵Gravatar letouzey2010-09-24
| | | | | | code git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13459 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a section in the documentation of Vernacular commands about ↵Gravatar aspiwack2010-09-23
| | | | | | Set/Unset/Test. It allowed to document the behaviour of Local and Global on Set and Unset. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13456 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update CHANGES: Local/Global Set/Unset.Gravatar aspiwack2010-09-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13455 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix inconsistency in Prop/Set conversion checkGravatar glondu2010-09-23
| | | | | | | This commit fixes a bug that made the system inconsistent with proof irrelevance (the main idea being that Set = Prop by reflexivity). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13450 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report fix bug 2345 from v8.3 (Bad error message when functionalGravatar courtieu2010-09-21
| | | | | | | scheme was called on an unknown function anme). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13445 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added eta-expansion in kernel, type inference and tactic unification,Gravatar herbelin2010-09-20
| | | | | | | governed in the latter case by a flag since (useful e.g. for setoid rewriting which otherwise loops as it is implemented). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13443 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed test of bug #2360 (use of Fail to check a regular error insteadGravatar herbelin2010-09-20
| | | | | | of an anomaly). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13442 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: re-introduce some eta-expansions in rare situations leading to ↵Gravatar letouzey2010-09-20
| | | | | | | | | | | | | | | | | | | | | '_a types If there's no lambdas at the top of a constant body and its type is functional and this type contains type variable and we're extracting to Ocaml then we perform one eta-expansion to please the ML type-checker This might slow down things, if some computations are shared thanks to the partial application. But it seems quite unlikely to encounter both situations (clever partial application and non-generalizable variable) at the same time. Compcert is ok, for instance. As a consequence, no need for manual eta-expansion in AVL code (and by the way MSetAVL.element wasn't a problem, it is monomorphic) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13441 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2389 (keyword "Declare Instance" unknown from "coqdoc -g") butGravatar herbelin2010-09-19
| | | | | | | this lacks robustness since "coqdoc -g" will drop away any commands unknown from coqdoc, leading to possible synchronisation problems. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13440 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2360 (descend_in_conjunctions built ill-typed terms). Shouldn't weGravatar herbelin2010-09-19
| | | | | | revert the catch of anomalies in reductionops.ml now (commit 13353)? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13439 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reverting partial fix for #2335 committed by mistake in r13435. Sorry.Gravatar herbelin2010-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13438 85f007b7-540e-0410-9357-904b9bb8a0f7
* Hopefully a fix for #2176 (redirection not understood with some shells)Gravatar herbelin2010-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13437 85f007b7-540e-0410-9357-904b9bb8a0f7
* Addressing part 2 of bug report 2377 (removing intrusive warning whenGravatar herbelin2010-09-19
| | | | | | | coqide doc link is the canonical link to last released version of reference manual instead of link to corresponding coqide version). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13436 85f007b7-540e-0410-9357-904b9bb8a0f7
* Patch solving the bug but leaving open design choicesGravatar herbelin2010-09-19
| | | | | | | The patch does not address the possible use of evars by get_symmetric_proof in unify_eqn. Someting has still to be done there. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13435 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
* Added test for bugs 2242, 2337, 2339 + remove the use of name "ambiguous" inGravatar herbelin2010-09-18
| | | | | | coqdep since it is now deterministic (later -R's overwriting former ones). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13432 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
* Now prints an error instead of an anomaly when dynlink failsGravatar herbelin2010-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13430 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a problem introduced in r12607 after pattern_of_constr servedGravatar herbelin2010-09-17
| | | | | | | | | | both for interpreting ltac patterns and patterns of "change pat with term". In particular, in the current status, Goal evars needs mandatorily to have the hole_kind GoalEvar. If this is too complicated to enforce, we might eventually consider another approach to the question of interpreting patterns in general. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13428 85f007b7-540e-0410-9357-904b9bb8a0f7
* In the computation of missing arguments for apply, accept that theGravatar herbelin2010-09-17
| | | | | | | | | | | | | | user either gives all missing arguments not dependent in the concl or all missing arguments not *recursively* dependent in the concl (as introduced by commit 13367). In practice, this means that "apply f_equal with A" remains allowed even though the new, recursive, analysis detects that all arguments of f_equal are inferable, including the first type argument (which is inferable from the knowledge of the function). Sized the opportunity to better explain the behavior of clenv_dependent. Also made minor code simplification. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13426 85f007b7-540e-0410-9357-904b9bb8a0f7
* For the moment, two small manual eta-expansions to avoid '_a after extractionGravatar letouzey2010-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13425 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: multiple fixes related with the Not_found encountered by X. LeroyGravatar letouzey2010-09-17
| | | | | | | | | | | | | | | | | | | Cf. coqdev for the details of the bug report. - Protect some Hashtbl.find and other risky functions in order to avoid as much as possible to end with an irritating Anomaly : Not_found. - Re-enable in pp_ocaml_extern the case of a module-file used as a module (e.g. module A' := A for A.v) when doing modular extraction. - Rework the code that decides to "open" or not modules initially: opening A when A contains a submodule B hides the file B even when B isn't opened itself, we avoid that now. - Fix some tables (sets or maps) used by extraction for which it is critical to consider constants/inductives/global_reference _not_ modulo the equivalence of Elie, but rather via Pervasives.compare. Still to do : avoid appearance of '_a in extracted code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13424 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqdep_boot : misc improvementsGravatar letouzey2010-09-17
| | | | | | | | | | - modules names can include quote ' - errors when parsing .mllib files are now properly reported instead of dying ugly on some sort of Failure - same when coqdep has to parse the output of ocamldep -modules - lib/lib.mllib contains a typo (lowercase ident) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13423 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 04:12:05 +0000