aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2010-07-22Adding the destauto tactic, that reduces match by destructing matchedcourtieu
term. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13307 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-22ported bug fix r13290 to checkerbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13304 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-21Fix for bug #2350 was really too quick. Here is a version that works better.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13303 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-21Backporting fix to bug #2353 (fixpoint with recursively non-uniformherbelin
parameters) to branch 8.2. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13302 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-21Quick fix for bug #2350 (ensuring enough "red" when refine calls fix tactic).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13301 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-21Applied Pierre Letouzey's patch restoring Convert_concl VM casts in new proofherbelin
engine. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13300 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-20Fixed a bug in list_forall2eq (wrong exception was caught).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13298 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-18Fixed parsing of "Generalizable Variable A" ("Variable" turns to be a keyword).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13295 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-18Reverted 13293 commited mistakenly. Sorry for the noise.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13294 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-18Tentative de suppression de l'import automatique des hints et coercions.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13293 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-16Amelioration dans Functionjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13292 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-16fixed (serious) bug #2353: non-recursive parameters of nested inductive ↵barras
types were seen as real constructor arguments... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13290 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-16removed a potentially dangerous try ... with _ -> ...barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13289 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-16MSetPositive: mention MSetInterface instead of FSetInterfaceletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13288 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-16FSetPositive: sets of positive inspired by FMapPositive.letouzey
Contributed by Alexandre Ren, Damien Pous, and Thomas Braibant. I've also included a MSets version, hence FSetPositive might become soon a mere wrapper for MSetPositive, as for other FSets implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13287 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-16Bool: shorter and more systematic proofs + an iff lemma about eqbletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13286 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-16fixed bug #2316 (ring_simplify)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13284 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-15Be more clever when trying to find out the relation inmsozeau
reflexivity/symmetry/transitivity, reabstracting arguments if necessary. Makes instances on [_ <> _] work. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13283 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-15Extraction: fix a bit the extraction under modulesletouzey
Extraction under modules is highly experimental, and just work a bit. Don't expect too much of it. With this commit, I simply avoid a few "assert false" to occur when we are under modules. But things are still quite wrong, for instance with: Definition foo. Module M. Definition bar := foo. Recursive Extraction bar. Extraction of bar is ok, but foo isn't displayed, since extraction can't get it: Lib.contents_after doesn't mention it, it is probably in some frozen summary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13281 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-15Ocamlbuild: adapt to last changes for camlp4 (use of tools/compat5*.cmo)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13280 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-12Fix compilation and test-suite of nsatzglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13279 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-12coqide: s/Sys.argv.(0)/Sys.executable_name/ for coqtop (cf #2341)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13277 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-10Bool: iff lemmas about or, a reflect inductive, an is_true functionletouzey
For the moment, almost no lemmas about (reflect P b), just the proofs that it is equivalent with an P<->b=true. is_true b is (b=true), and is meant to be added as a coercion if one wants it. In the StdLib, this coercion is not globally activated, but particular files are free to use Local Coercion... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13275 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-09Finish adding out-of-the-box support for camlp4letouzey
If you want to try, it should be now as simple as: make clean && ./configure -local -usecamlp4 && make For the moment, the default stays camlp5, hence ./configure -usecamlp5 and ./configure are equivalent. Thanks to a suggestion by N. Pouillard, the remaining incompatibilities are now handled via some token filtering in camlp4. See compat5*.mlp. Morally, these files should be named .ml4, but I prefer having them not in $(...ML4) variables, it might confuse the Makefile... The empty compat5*.ml are used to build empty .cmo for making camlp5 happy. For camlp4, - tools/compat5.cmo changes GEXTEND into EXTEND. Safe, always loaded - tools/compat5b.cmo changes EXTEND into EXTEND Gram. Interact badly with syntax such that VERNAC EXTEND, we only load it for a few files via camlp4deps TODO: check that my quick adaptation of camlp5-specific code in tactics/extratactics.ml4 is ok. It seems the code by Chung-Kil Hur is hiding information in the locations ?! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13274 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-08Extraction: restrict autoinling to csts whose body is globally visible (fix ↵letouzey
#2241) Here, the constants "without body" we don't want to autoinline are constants made opaque by the rigid signature of their module. As mentionned by X.L. inlining them might lead to untypable code. The current solution is safe, but not ideal: we could want to inline such constants at least inside their own module, and we could also want to inline constants that are not globally visible (functors...). NB: AutoInline is anyway not activated by default anymore git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13273 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-08Updating reference manual credits: gb is now nsatz.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13271 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-08Extraction: more factorization of common match branchesletouzey
In addition to the "| _ -> cst" situation, now we can also reconstruct a "| e -> f e" final branch. For instance, this has a tremenduous effect on Compcert/backend/Selection.v. NB: The "fun" factorisation is almost more general than the "cst" situation, but not always. Think of A=>A|B=>A, 1st branch will be recognized as (fun x->x), not (fun x->A). We also add a fine detection of inductive types with phantom type variables, for which this optimisation is type-unsafe. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13267 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-08Extraction: Unset Extraction AutoInline is now the defaultletouzey
The auto-inlining has always been cumbersome. We only keep the inlining of recursors (foo_rect for inductive foo), and a short list of specific constants declared in mlutil.ml. In particular we inline andb and orb to keep their lazy behavior. The previous behavior is available via Set Extraction AutoInline git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13266 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-08nsatz in an integral domain with specialization to Z and Rpottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13265 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-07Fixed compilation with statically-linked plugins (the decl_modeherbelin
plugins has to be linked before the xml plugin). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13262 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-07Extraction Library Foo creates Foo.ml, not foo.ml (correct version)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13261 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-07Extraction Library Foo creates Foo.ml, not foo.mlletouzey
And similarly for Haskell: we do not force capitalized/uncapitalized filenames anymore, but we rather follow the name of the .v file (with new extensions of course). Ok, this is an incompatible change, but it is really convenient, some people where actually already doing some hacks to have this behavior (cf. Compcert). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13260 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-07CHANGES: mention last-minute improvements of extractionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13250 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-07Extraction: get advantage of nicer, algebraic, module typesletouzey
We use the mod_type_alg and typ_expr_alg field when they aren't empty. As a consequences, many signatures are now simple abbreviations, or "with" constructions, leading to .mli that are _way_ shorter this way. Various fixups concerning the "with Definition" syntax. In extract_seb_spec, we propagate both the alg and non-alg versions of the structure, for handlying nicely the "with" situation, and expanding situations not possible in ocaml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13249 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-07Extraction: some more work on the (re)naming frameworkletouzey
- MPbound can be part of visible_mps (when printing the type of a module parameter, or when printing body of a With), hence the locality test base_mp mp = base_mp (top_visible_mp ()) isn't accurate. - new organisation, pp_ocaml_gen is splitted in many sub-functions, attempt to be clearer - the shortcut (if List.length ls = 1 then ...) isn't safe, we might detect name conflict even in this case. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13248 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-07Mod_typing: fix the content of the typ_expr_alg fieldletouzey
Fix suggested by Elie. Without that, typ_expr_alg may contain Foo instead of Bar when Foo is a module of type Bar. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13247 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-05Fix goal display when backtrackingvgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13246 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-05Robustness fix : clean restart of coqtop on pipe error + force matchingvgross
of coqtop return codes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13245 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-05Turned off Mac dynlink hack for 10.6.3+ on x86_64thutchin
I don't have access to an x86_64 computer with 10.6 Maybe for 10.6.0/1/2 special cases aren't required Reverted commit r13083 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13243 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-05Stronger checks on coqtop termination, warning when zombies.vgross
Also, reindentation + typed_notebook simplification git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13241 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-05Extraction: (yet another) rework of the renaming codeletouzey
- Add module parameters in the structure of visible_layer, in order for module params to be part of name clash detection, avoiding this way a source of potentially wrong code. - In case of clash, module params are alpha-renamed to something unique (Foo__XXX where XXX is the number contained in the mbid). This solves some situations that were unsupported by extraction. for instance the "Module F (X:T). Module X:=X. ... End F." - We now check in Coq identifiers the presence of the extraction-reserved string __. If it is found, we issue a warning (which might become an error someday). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13240 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-05FSets/Msets: some renaming of module params to simplify the task of the ↵letouzey
extraction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13239 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-02Fixing tabs closing problems by removing activation infrastructure.vgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13238 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-02Extraction: better support of modulesletouzey
- For Haskell, modules abbreviations and applied functors are expanded. The only remaining sitation that isn't supported is extracting functors and applying them after extraction. - Add a module extraction for Scheme with the same capabilities as for Haskell (with no Extraction Library, though). - Nicer extracted module types (use of the mb.mod_type_alg if present) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13236 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-02Extraction: no more MPself hence no need for subst during ppletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13235 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-02Remove dependency to Unix from module Profileglondu
Looking at the source code of Sys.time reveals that it is exactly what is computed by Profile.get_time. This can also be tested by evaluating: Sys.time () -. Unix.(let x = times () in x.tms_utime +. x.tms_stime);; in an OCaml toplevel with Unix. This allows to put Profile in grammar.cma without the dependency to unix.cma while preprocessing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13233 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-02Sorting library: export as hints only lemmas that obviously simplifyherbelin
the size of the problem to solve. This is still more powerful than what 8.2 provided since no hints were exported yet when Permutation was in List.v in 8.2. Whether no hints should be exported at all, and whether hints should be exported in a specific database or not is unclear. At least, the contribs apparently supported the extra added power of auto introduced in r12585 (date of the revision of the Sorting library), so let's continue with it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13231 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-01Miscellaneous small updates:herbelin
- removed call to obsolete ppmsid printer in 8.3 - updated COMPATIBILITY file git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13229 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-30Move [delayed] to util and use [force_delayed] everywhere to forcemsozeau
thunks. Move from [lazy] to [delayed] in subtac. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13227 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-30Fix generalize_eqs tactic to not consider defined variables as being ↵msozeau
generalizable. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13226 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 17:43:18 +0000