aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2010-09-20Fixed test of bug #2360 (use of Fail to check a regular error insteadherbelin
of an anomaly). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13442 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-20Extraction: re-introduce some eta-expansions in rare situations leading to ↵letouzey
'_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
2010-09-19Fixing bug #2389 (keyword "Declare Instance" unknown from "coqdoc -g") butherbelin
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
2010-09-19Fixing bug #2360 (descend_in_conjunctions built ill-typed terms). Shouldn't weherbelin
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
2010-09-19Reverting partial fix for #2335 committed by mistake in r13435. Sorry.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13438 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-19Hopefully a fix for #2176 (redirection not understood with some shells)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13437 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-19Addressing part 2 of bug report 2377 (removing intrusive warning whenherbelin
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
2010-09-19Patch solving the bug but leaving open design choicesherbelin
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
2010-09-18Fixing #2162 and #2367 (wrong order of Show Match) for branch 8.2 tooherbelin
(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
2010-09-18Added test for bugs 2242, 2337, 2339 + remove the use of name "ambiguous" inherbelin
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
2010-09-18Fixing bugs #2347 (part 2) and #2388: error message printing was doneherbelin
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
2010-09-18Now prints an error instead of an anomaly when dynlink failsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13430 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-17Fixed a problem introduced in r12607 after pattern_of_constr servedherbelin
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
2010-09-17In the computation of missing arguments for apply, accept that theherbelin
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
2010-09-17For the moment, two small manual eta-expansions to avoid '_a after extractionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13425 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-17Extraction: multiple fixes related with the Not_found encountered by X. Leroyletouzey
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
2010-09-17Coqdep_boot : misc improvementsletouzey
- 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
2010-09-16Explicit Mod_checking signatureglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13422 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-15Sharing is not anymore broken by traverse_module.soubiran
+commit r13412 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13418 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-15Fix likely semantic typosglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13417 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-14CoqIDE argv parsing delegated to coqtopvgross
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
2010-09-13Fix unescaped end-of-lines (OCaml warning 29)glondu
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
2010-09-13commit 13400 and 13409.soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13410 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-11Improving a few error messages in Ltac interpretationherbelin
- improving error message when a reference to unfold is not found - repairing anomaly when an evaluable reference exists at internalisation-time but not at run time, and similarly for an arbitrary term (but the latter is new from 8.3 because of the new use of retyping instead of understand for typing Ltac values) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13408 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-10files introduce in commit 13401 aren't erased anymore by 'make clean'pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13404 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-10Bugfix: A notation for a constructor where some arguments are _pboutill
is now allowed on the left side of a match. You can write 'match v with |Vnil => 0 |h :: q => 1 end.' if 'h :: q' stands for the vector 'Vcons _ h _ t'. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13403 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-09NMake : another round of heavy reworkletouzey
- generic iterator [iter] factorized in the same way as [same_level] - as a consequence, remaining operations [mul] [compare] [div_gt] are now defined and proved in a short and nice way and moved to NMake.v. - lots of other simplifications / factorisations in NMake_gen. This file is still macro-generated, but is much shorter, and the major part of it is now invariant. - As advised by B. Gregoire, try to (re)create clever partial applications in code of operators, in order to avoid projecting ZnZ fields all the time in base cases. Case 0 can still be improved, but it's already better this way :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13402 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-06Added doc/refman/coqide.eps and coqide-queries.eps to remove the need for ↵emakarov
pngtopnm and pnmtops git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13401 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-02fixed bug #2375 (congruence)corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13399 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-02* removed declare_constant and declare_internal_constant vsiles
(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
2010-09-02v13392 port from v8.3 to trunk : correct message when defining inductive schemesvsiles
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13394 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-02Clarified role of Set Boolean Equality Schemes wrt Set Equality Scheme +herbelin
backport of 13391 from 8.3 to trunk. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13393 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-02Improved printing of Unfoldable constants in hints databases (usedherbelin
user-level pr_constant instead of debugging-level pr_con + used ppnl and boxes instead of explicit fnl's so as not to disturb formatting). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13390 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-08-31* By default, load proof terms.regisgia
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13389 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-08-27* scripts/Coqc toplevel/Usage:regisgia
Export the -load-proofs officially. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13388 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-08-27* checker/Safe_typing.LightenLibrary:regisgia
Remove the function "save" as the checker only needs to read vo files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13387 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 18:31:18 +0000