aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
| | | | | | | | | | | | | - Added support for recursive notations with binders - Added support for arbitrary large iterators in recursive notations - More checks on the use of variables and improved error messages - Do side-effects in metasyntax only when sure that everything is ok - Documentation Note: it seems there were a small bug in match_alist (instances obtained from matching the first copy of iterator were not propagated). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13316 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplified the way internalization_data (i.e. bindings of bound varsGravatar herbelin2010-07-22
| | | | | | | to their signature of implicit positions and scopes) is computed. A bit of documentation in constrintern.mli. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13315 85f007b7-540e-0410-9357-904b9bb8a0f7
* Constrintern: unified push_name_env and push_loc_name_env; madeGravatar herbelin2010-07-22
| | | | | | | | | | location dumping for binders uniformly treated in constrintern.ml (and renamed the optional arg of interp_context from fail_anonymous to global_level since the flag now also decides whether to dump binders as global or local ones); added locations for the variables occurring in the "as in" clauses; git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13314 85f007b7-540e-0410-9357-904b9bb8a0f7
* Constrintern: Moved section about binders before section about notationGravatar herbelin2010-07-22
| | | | | | in preparation of supporting parameters for binders in notations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13313 85f007b7-540e-0410-9357-904b9bb8a0f7
* Switch to American spelling for "internalise" and "internalisation"Gravatar herbelin2010-07-22
| | | | | | (hence following the general convention about spelling in Coq's code). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13312 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).Gravatar herbelin2010-07-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13311 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made coercions active only when modules are imported.Gravatar herbelin2010-07-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13310 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backported r13308 (ConstructiveEpsilon.v) to branch v8.3Gravatar herbelin2010-07-22
| | | | | | Also removed trailing spaces of the file git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13309 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update of ConstructiveEpsilon.v by Jean-François Monin.Gravatar herbelin2010-07-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13308 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding the destauto tactic, that reduces match by destructing matchedGravatar courtieu2010-07-22
| | | | | | | term. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13307 85f007b7-540e-0410-9357-904b9bb8a0f7
* ported bug fix r13290 to checkerGravatar barras2010-07-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13304 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix for bug #2350 was really too quick. Here is a version that works better.Gravatar herbelin2010-07-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13303 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backporting fix to bug #2353 (fixpoint with recursively non-uniformGravatar herbelin2010-07-21
| | | | | | parameters) to branch 8.2. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13302 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 08:12:23 +0000