aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Quick fix for bug #2350 (ensuring enough "red" when refine calls fix tactic).Gravatar herbelin2010-07-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13301 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applied Pierre Letouzey's patch restoring Convert_concl VM casts in new proofGravatar herbelin2010-07-21
| | | | | | engine. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13300 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a bug in list_forall2eq (wrong exception was caught).Gravatar herbelin2010-07-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13298 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed parsing of "Generalizable Variable A" ("Variable" turns to be a keyword).Gravatar herbelin2010-07-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13295 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reverted 13293 commited mistakenly. Sorry for the noise.Gravatar herbelin2010-07-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13294 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tentative de suppression de l'import automatique des hints et coercions.Gravatar herbelin2010-07-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13293 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amelioration dans FunctionGravatar jforest2010-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13292 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed (serious) bug #2353: non-recursive parameters of nested inductive ↵Gravatar barras2010-07-16
| | | | | | 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
* removed a potentially dangerous try ... with _ -> ...Gravatar barras2010-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13289 85f007b7-540e-0410-9357-904b9bb8a0f7
* MSetPositive: mention MSetInterface instead of FSetInterfaceGravatar letouzey2010-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13288 85f007b7-540e-0410-9357-904b9bb8a0f7
* FSetPositive: sets of positive inspired by FMapPositive.Gravatar letouzey2010-07-16
| | | | | | | | | | 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
* Bool: shorter and more systematic proofs + an iff lemma about eqbGravatar letouzey2010-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13286 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed bug #2316 (ring_simplify)Gravatar barras2010-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13284 85f007b7-540e-0410-9357-904b9bb8a0f7
* Be more clever when trying to find out the relation inGravatar msozeau2010-07-15
| | | | | | | | 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
* Extraction: fix a bit the extraction under modulesGravatar letouzey2010-07-15
| | | | | | | | | | | | | | | | | | 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
* Ocamlbuild: adapt to last changes for camlp4 (use of tools/compat5*.cmo)Gravatar letouzey2010-07-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13280 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix compilation and test-suite of nsatzGravatar glondu2010-07-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13279 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: s/Sys.argv.(0)/Sys.executable_name/ for coqtop (cf #2341)Gravatar glondu2010-07-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13277 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bool: iff lemmas about or, a reflect inductive, an is_true functionGravatar letouzey2010-07-10
| | | | | | | | | | | 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
* Finish adding out-of-the-box support for camlp4Gravatar letouzey2010-07-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Extraction: restrict autoinling to csts whose body is globally visible (fix ↵Gravatar letouzey2010-07-08
| | | | | | | | | | | | | | | | #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
* Updating reference manual credits: gb is now nsatz.Gravatar herbelin2010-07-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13271 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: more factorization of common match branchesGravatar letouzey2010-07-08
| | | | | | | | | | | | | | 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
* Extraction: Unset Extraction AutoInline is now the defaultGravatar letouzey2010-07-08
| | | | | | | | | | | 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
* nsatz in an integral domain with specialization to Z and RGravatar pottier2010-07-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13265 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed compilation with statically-linked plugins (the decl_modeGravatar herbelin2010-07-07
| | | | | | 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
* Extraction Library Foo creates Foo.ml, not foo.ml (correct version)Gravatar letouzey2010-07-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13261 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction Library Foo creates Foo.ml, not foo.mlGravatar letouzey2010-07-07
| | | | | | | | | | 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
* CHANGES: mention last-minute improvements of extractionGravatar letouzey2010-07-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13250 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: get advantage of nicer, algebraic, module typesGravatar letouzey2010-07-07
| | | | | | | | | | | | 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
* Extraction: some more work on the (re)naming frameworkGravatar letouzey2010-07-07
| | | | | | | | | | | | | - 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
* Mod_typing: fix the content of the typ_expr_alg fieldGravatar letouzey2010-07-07
| | | | | | | 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
* Fix goal display when backtrackingGravatar vgross2010-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13246 85f007b7-540e-0410-9357-904b9bb8a0f7
* Robustness fix : clean restart of coqtop on pipe error + force matchingGravatar vgross2010-07-05
| | | | | | of coqtop return codes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13245 85f007b7-540e-0410-9357-904b9bb8a0f7
* Turned off Mac dynlink hack for 10.6.3+ on x86_64Gravatar thutchin2010-07-05
| | | | | | | | | 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
* Stronger checks on coqtop termination, warning when zombies.Gravatar vgross2010-07-05
| | | | | | Also, reindentation + typed_notebook simplification git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13241 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: (yet another) rework of the renaming codeGravatar letouzey2010-07-05
| | | | | | | | | | | | | | | - 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
* FSets/Msets: some renaming of module params to simplify the task of the ↵Gravatar letouzey2010-07-05
| | | | | | extraction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13239 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing tabs closing problems by removing activation infrastructure.Gravatar vgross2010-07-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13238 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: better support of modulesGravatar letouzey2010-07-02
| | | | | | | | | | | | | - 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
* Extraction: no more MPself hence no need for subst during ppGravatar letouzey2010-07-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13235 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove dependency to Unix from module ProfileGravatar glondu2010-07-02
| | | | | | | | | | | | | | 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
* Sorting library: export as hints only lemmas that obviously simplifyGravatar herbelin2010-07-02
| | | | | | | | | | | | 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
* Miscellaneous small updates:Gravatar herbelin2010-07-01
| | | | | | | - 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
* Move [delayed] to util and use [force_delayed] everywhere to forceGravatar msozeau2010-06-30
| | | | | | | 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
* Fix generalize_eqs tactic to not consider defined variables as being ↵Gravatar msozeau2010-06-30
| | | | | | generalizable. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13226 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.Gravatar msozeau2010-06-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13225 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correct wrong handling of evars in instance definitions that preventedGravatar msozeau2010-06-29
| | | | | | | information going from the body to the type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13224 85f007b7-540e-0410-9357-904b9bb8a0f7
* QArith: typo in name of hint db (fix #2346)Gravatar letouzey2010-06-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13220 85f007b7-540e-0410-9357-904b9bb8a0f7
* change the flag "internal" in declare/ind_tables from bool toGravatar vsiles2010-06-29
| | | | | | | | | | | | | | a 3 state type to allow: * KernelVerbose / KernelSilent : handle the display of messages launch by Coq * UserVerbose : handle the display of messages launch by user actions Coq will still behaves the same way (TODOs in the code mark the places where we can now change the behaviour). I'll remove them in a few days when we'll have agreed on the correct behaviour. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13217 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-29 23:57:07 +0000