aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2011-03-21Documentation of the timeout tactical (cf r13917)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13921 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-21Init: some results in Type should rather be Defined than Qedletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13920 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-21Makefile.build: states/initial.coq was wrongly done with -dont-load-proofsletouzey
This was breaking the FireSquad extraction test git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13919 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-18Makefile.build: compile the stdlib with -dont-load-proofs by defaultletouzey
Since library files aren't meant to contain queries like Print Assumptions nor extractions, it is safe (and quite quicker) to compile them with -dont-load-proofs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13918 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-18A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> secondsletouzey
Note: even if this new tactical can be quite handy during the development phase, (for instance to bound the time allocated to some search tactics), please be aware of its main drawback: with it, scripts are no longer machine-independant, something that works on a quick machine may fail on a slow one. The converse is even possible if you combine this "timeout" with other tactic combinators. We strongly advise to not leave any "timeout" in the final version of a development. In addition, this feature won't probably work on native win32, since Unix.alarm isn't implemented. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13917 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-17An option "Set Default Timeout n."letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13916 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-17Goptions: repair Unset for int optionsletouzey
Previous code was trying to do a bool write, and in case of error, a int write. But for compatibility reason, bool write error were turned into warnings, preventing Unset Foo Bar to work when Foo Bar is an int option. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13915 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-17CompareSpec: a slight generalization/reformulation of CompSpecletouzey
CompareSpec expects 3 propositions Peq Plt Pgt instead of 2 relations eq lt and 2 points x y. For the moment, we still always use (Peq=eq x y), (Plt=lt x y) (Pgt=lt y x), but this may not be always the case, especially for Pgt. The former CompSpec is now defined in term of CompareSpec. Compatibility is preserved (except maybe a rare unfold or red to break the CompSpec definition). Typically, CompareSpec looks nicer when we have infix notations, e.g. forall x y, CompareSpec (x=y) (x<y) (y<x) (x?=x) while CompSpec is shorter when we directly refer to predicates: forall x y, CompSpec eq lt x y (compare x y) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13914 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-16Adapt printers.mllib after my last commitletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13913 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-16Finish branching functions handling module errors (cf. r13886)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13912 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-16Remove some weird syntax "fun ... ," that used to be accepted (cf r13876)letouzey
Probably something related with the unicode lambda syntax... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13911 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-16Adapt test-suite/output/Extraction_matchs_2413 to new indentation of extractionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13910 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-13Fix inductive_template building ill-typed evars, and update test-suite scriptsmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13909 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-13- Add modulo_delta_types flag for unification to allow fullmsozeau
conversion when checking types of instanciations while having restricted delta reduction for unification itself. This makes auto/eauto... backward compatible. - Change semantics of [Instance foo : C a.] to _not_ search for an instance of [C a] automatically and potentially slow down interaction, except for trivial classes with no fields. Use [C a := _.] or [C a := {}] to search for an instance of the class or for every field. - Correct treatment of transparency information for classes declared in sections. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13908 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-11Keep information on which fields are subclasses in class declarations,msozeau
in preparation for adding forward reasoning to typeclass resolution. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13907 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-11Inference of match predicate produces ill-typed unification problem,msozeau
revert to manual building of the predicate. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13906 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-11Tentative to make unification check types at every instanciation of anmsozeau
evar, and simultaneously make type inference with universes work better. This only exports more functions from kernel/univ, to be able to work with a set of universe variables during type inference. Universe constraints are gradually added during type checking, adding information necessary e.g. to lower the level of unknown Type variables to Prop or Set. There does not seem to be a disastrous performance hit on the stdlib, but might have one on some contribs (hence the "Tentative"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13905 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-11- Better error messages taking unif. constraints into account.msozeau
- Normalize evars in typeclasses eauto also before [intro]. - Disallow use of nf_evars variants that drop unif. constraints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13904 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-10Forgot a use of evars_reset_evd in nf_evars, add an optional argument asmsozeau
in the 8.3 patch. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13903 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-10Do not forget conv_pbs when resetting an evm: msozeau
- In clenv, this used to forget the existing constraints, there are none in the other evar_map. - Other uses (evar_refiner, class_tactics) always reset with an enriched version of the same evar_map. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13901 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-10ZBits,ZdivEucl,ZDivFloor: a few lemmas with weaker preconditionsletouzey
Initial patch by Robbert Krebbers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13900 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-08Solve evar instantiations in the right environment.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13899 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-08Fix declarations of [Add Setoid/Morphism...] in sections to not exportmsozeau
by default (bug introduced in r13842). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13898 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-08syntax for exponentspottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13897 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-08adding eta in the vmbgregoir
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13896 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-07Reverted commit r13893 about propagation of more informativeherbelin
unification failure messages (it is not fully usable and was not intended to be committed now, sorry for the noise). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13895 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-07Revert commit r13883: instantiating ?n by a lambda when "?n a" has toherbelin
be unified with a (truly) rigid term would need to be able to project non-atomic arguments of evars what is not done (consider e.g. "Check (fun m n (H:m+n=n) => ((f_equal _ H) : S (m+n) = S n))."). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13894 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-07Added propagation of evars unification failure reasons for betterherbelin
error messages. The architecture of unification error handling changed, not helped by ocaml for checking that every exceptions is correctly caught. Report or fix if you find a regression. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13893 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-07CHANGES: mentionning quickly Separate Extractionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13892 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-07Extraction: a warning when an opaque constant is enterredletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13891 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-07Extraction: fix printing of haskell modular namesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13890 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-07Extraction: avoid printing unused mutual fix components (fix #2477)letouzey
This happens for instance when the main component of the fixpoint block has been provided via Extract Constant git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13889 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-07A new command "Separate Extraction"letouzey
This is a mix of "Recursive Extraction" and "Extraction Library": - like "Extraction Library", the extracted code is splitted in separated files, one per coq source file. - unlike "Extraction Library", but similarly to "Recursive Extraction", not everything gets extracted, but only dependencies of some initially-given elements We prepare for a more clever dependency selection inside sub-modules. For the moment all needed sub-modules are still fully extracted (other we would need to fix signatures accordingly). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13888 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-05Added a table for using reserved names for binding names to typesherbelin
(in addition of types to names) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13887 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-05Moving printing of module typing errors upwards to himsg.ml so as toherbelin
be able to call term printers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13886 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-05Starting being more explicit on the reasons why module subtyping fails.herbelin
Note: I'm unsure about some subtyping error case apparently involving aliases of inductive types (middle of Subtyping.check_inductive); I bound it to some NotEqualInductiveAliases error, but this has to be checked. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13885 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-05A few more betaiota on environments and types of error messages. Seems toherbelin
be convenient in general. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13884 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-05Added support for instantiation of ?n by a lambda when "?n a" has toherbelin
be unified with a (truly) rigid term. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13883 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-05Reorganized a bit evarconv.ml:herbelin
- Made a distinction between truly rigid constructions (Rigid) and possibly flexible constructions (match/fix/meta, now called PseudoRigid) that are currently assimilated to rigid by lack of appropriate study of their flexibility. One day, the flexibility of these pseudo-rigid constructions will have to considered seriously. - Removed useless Cast/Cast cases in Rigid/Rigid block (Cast are removed in advance and LetIn are not considered Rigid). - Moved LetIn into the MaybeFlexible class. - Moved the Lambda/Lambda case upwards to factorize the rules for eta-expansion. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13882 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-05Improved define_evar_as_lambda which was creating an unrelated new evarherbelin
for the domain instead of retrieving the known domain of the initial evar. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13881 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-05Instantiate evar by a lambda when "?n args" has to unify with Prodherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13880 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-05Fixed a "feature" about subtyping records: one was expected not onlyherbelin
that the fields had the same names but that the parameters of the record had exactly the same names too. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13879 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-05Restore documentation of library String which was removed in 2007 (r10049)herbelin
probably inadvertantly since it is not reported in the commit log. (Thanks to Cédric who noticed it.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13877 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-05Forgotten removal of ',' in 'fun' rule: it has to come with the lambda notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13876 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-05Fixing injection bug #2493 (regression introduced by fixing injectionherbelin
bug #2255 from 8.2pl2: use of unification might support cumulativity). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13873 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-04CHANGES: update of syntax for annotations of functor applicationletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13871 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-04Extraction: improved indentation of extracted code (fix #2497)letouzey
For Haskell, we still try to provide readable indentation, but we now avoid relying on this indentation for correctness. Instead, we use layout-independant syntax with { } when necessary (after "case of" and "let"). It is much safer this way, even if the syntax gets a bit more cumbersome. For people allergic to {;}, they can most of the time do a tr -d "{;}" without changing the meaning of the program. Be careful nonetheless: since "case of" is now delimited, some parenthesis that used to be mandatory are now removed. Note also that the initial "module ... where" is still without { }: even when Format goes crazy it doesn't tamper with column 0. Other modifications: - Using "Set Printing Width" now affects uniformly the extraction pretty-printers. You can set a greater value than the default 78 before extracting a program that you know to be "really deep". - In ocaml (and also a bit in Haskell), we now try to avoid abusing of 2-char-right-indentation. For instance | is now aligned with the "m" of match. This way, max_indent will be reached less frequently. - As soon as a pretty-print box contains an explicit newline, we set its virtual size to a big number, in order to prevent this box to be part of some horizontal arrangement. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13870 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-04Simplify proofs in Permutation using generalized rewriting.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13869 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-04- Allow to set a particular transparent_state for the local hintmsozeau
database - Fix [specialize] to properly resolve typeclass constraints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13868 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-04checker: cleanupglondu
Backport of changes introduced in r13443. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13867 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-11 05:02:30 +0000