aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2011-03-04checker: add eta-expansionglondu
Backport of changes introduced in r13443 and r13494. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13866 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-03Propagate recent kernel changes to the checkerletouzey
Cf in particular commits 13807 (about inlining) and 13835-13836 (changing the internal structure of delta_resolver and substitution). A pity we should duplicate so much code in the Checker... I tried to fix the corresponding val_* functions that check the integrity of the .vo, it seems to work, but I'm not familiar with this code. After this commit, apparently "make validate" accepts all the stdlib again, apart the new file setoid_ring/Ring2.v recently added by Loic, where it says "type error" on ring_syntax1. To be investigated... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13865 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-28- Allow rewriting under abitrary products, not just those in Prop.msozeau
- New [fold] rewrite strategy to do folding of terms up-to unification and under binders (might leave uninstantiated existentials). This does not build a proof, only a cast. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13864 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-28Add a flag to hide obligations in Program-generated terms under anmsozeau
application of a dummy "obligation" constant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13863 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-25Extraction: Add missing parenthesis around emulated pattern-match (fix #2478)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13861 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-25Fix indentation of default pattern in haskell case (bug #2476)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13859 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-25Filter out admitted subgoals from search resultsglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13858 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-25Ocamlbuild needs OCAML_LD_LIBRARY_PATH (bug #2502)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13857 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-25Revert "syntax for exponents"glondu
This reverts pottier's commit r13849. It references a ncring_plugin.cma for which there is no rule. I guess he forgot to commit something... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13856 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-24Mod_subst: improving sharing of subst_mpsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13854 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-23Some more simplification in Mod_substletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13852 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-23BigQ : setting correct arguments scopesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13851 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-22Try to fix the behavior of clenv_missing used when declaring hintsletouzey
Before this patch, hints such as "Hint Resolve -> a" in success/Hints.v were erroneously considered "eauto-only". We try to clarify the big boolean expression via "if", and for the moment we remove the detection of "nonlinearity" via duplicated_metas : on the example, some nonlinearity was found for strange reason (beta expansion ?), and after some discussion with Hugo, it is unclear whether this nonlinearity stuff is useful at all. The next coqbench might provide some answer to this question, we'll see git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13850 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-22syntax for exponentspottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13849 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-22anneaux commutatifs ou non, reification sans mlpottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13848 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-21Some fixes of the test-suite scriptsletouzey
In particular, the Fail meta-command cannot for the moment catch a Syntax Error, which is raised by Vernac.parse_sentence, before we even now that the line starts by a Fail... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13847 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-21Fix test-suite script.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13846 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-17In Program obligation, do not use auto on non-proposition goals bymsozeau
default. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13845 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-17- Use transparency information all the way through unification andmsozeau
conversion. - Fix trans_fconv* to use evars correctly. - Normalize the goal with respect to evars before rewriting in [rewrite], allowing to see instanciations from other subgoals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13844 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-16Fix compilation issues.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13843 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-14- Fix treatment of globality flag for typeclass instance hints (theymsozeau
were all declared as global). - Add possibility to remove hints (Resolve or Immediate only) based on the name of the lemma. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13842 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-12fix last commit about modules (subst_cl_typ may raise Not_found)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13841 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-11An automatic substitution of scope at functor applicationletouzey
For Argument Scope, we now record types (more precisely classes cl_typ) in addition to scope list. After substitution (e.g. at functor application), the new types are used to search for corresponding concrete scopes. Currently, this automatic scope substitution of argument scope takes precedence (if successful) over scope declared in the functor (even by the user). On the opposite, the manual scope substitution (cf last commit introducing annotation [scope foo to bar]) is done _after_ the automatic scope substitution. TODO: if this behavior is satisfactory, document it ... Note that Classops.find_class_type lose its env args since it was actually unused, and is now used for Notation.find_class git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13840 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-11Annotations at functor applications:letouzey
- The experimental syntax "<30>F M" is transformed into "F M [inline at level 30]" - The earlier syntax !F X should now be written "F X [no inline]" (note that using ! is still possible for compatibility) - A new annotation "F M [scope foo_scope to bar_scope]" allow to substitute foo_scope by bar_scope in all arguments scope of objects in F. BigN and BigZ are cleaned from the zillions of Arguments Scope used earlier. Arguments scope for lemmas are fixed for instances of Numbers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13839 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-11Mod_typing: some refactoring (common parts about MSEapply and co)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13838 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-11Safe_typing: some refactoring (avoiding copy-paste of record definitions)letouzey
Many of the record definitions for new safe_environment follow the same pattern, we factorize them in a generic add_field function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13837 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 10:01:58 +0000