aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Collapse)AuthorAge
* Extraction: cosmetics when using ocaml + Extract Inductive to symbolsGravatar letouzey2010-04-16
| | | | | | | | | | | - When using an infix constructor such as (::), whitespaces are to be given by the user, for instance Extract Inductive list => list [ "[]" "( :: )" ]. - Remove ugly whitespaces when using the ""-for-Pair trick: Extract Inductive prod => "(*)" [ "" ]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12944 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: restore (temporarily?) a very limited form of linear letin reductionGravatar letouzey2010-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12943 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: less eta in calls to global functions, better optimization phaseGravatar letouzey2010-04-16
| | | | | | | | | | | | - we saturate the normalize function : as long as (kill_dummy + simpl) isn't a nop, we do it again. - generalize_case allowed on all types of theories/Init/*.v instead of only bool,sumbool,sumor. NB: this optim cannot be performed on any type, it might produce untyped code. - common_branch allowed on match with one branch: in this situation it indicates whether the match can be removed or not. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12942 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: improvement of optimizations (kill_dummy, optim_fix)Gravatar letouzey2010-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12940 85f007b7-540e-0410-9357-904b9bb8a0f7
* Util: remove list_split_at which is a clone of list_chopGravatar letouzey2010-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12939 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: ad-hoc identifier type with annotations for reductionsGravatar letouzey2010-04-16
| | | | | | | | | | | | | | | | * An inductive constructor Dummy instead of a constant dummy_name * The Tmp constructor indicates that the corresponding MLlam or MLletin is extraction-specific and can be reduced if possible * When inlining a glob (for instance a recursor), we tag some lambdas as reducible. In (nat_rect Fo Fs n), the head lams of Fo and Fs are treated this way, in order for the recursive call inside nat_rect to be correctly pushed as deeper as possible. * This way, we can stop allowing by default linear beta/let reduction even under binders (can be activated back via Set Extraction Flag). * Btw, fix the strange definition of non_stricts for (x y). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12938 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: less _ in Haskell (typically for False_rect), less toplevel ↵Gravatar letouzey2010-04-16
| | | | | | eta-expansions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12936 85f007b7-540e-0410-9357-904b9bb8a0f7
* Look for csdp in $PATH at runtime, remove -csdpdir configure optionGravatar glondu2010-04-11
| | | | | | | | | The csdp path computed by the configure script wasn't used at all, but was forcing presence of csdp at configure time whereas it is not used at all in the build process. Instead, we replace the configure-time check with a runtime check for existence of csdp in $PATH. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12929 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove unused functions run_sdpaGravatar glondu2010-04-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12928 85f007b7-540e-0410-9357-904b9bb8a0f7
* Manual qualification of Mfourier.Proof in micromega to avoid ocamldep using ↵Gravatar letouzey2010-03-30
| | | | | | ide/proof git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12892 85f007b7-540e-0410-9357-904b9bb8a0f7
* Several bug-fixes and improvements of coqdocGravatar herbelin2010-03-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - make links to section variables working (used qualified names for disambiguation and fixed the place in intern_var where to dump them) (wish #2277) - mapping of physical to logical paths now follows coq (see bug #2274) (incidentally, it was also incorrectly seeing foobar.v as a in directory foo) - added links for notations - added new category "other" for indexing entries not starting with latin letter (e.g. notations or non-latin identifiers which was otherwise broken) - protected non-notation strings (from String.v) from utf8 symbol interpretation - incidentally quoted parseable _ in notations to avoid confusion with placeholder in the "_ + _" form of notation - improved several "Sys_error" error messages - fixed old bug about second dot of ".." being interpreted as regular dot - removed obsolete lexer in index.mll (and renamed index.mll to index.ml) - added a test-suite file for testing various features of coqdoc Things that still do not work: - when a notation is redefined several times in the same scope, only the link to the first definition works - if chars and symbols are not separated in advance, idents that immediately follow symbols are not detected (e.g. as in {True}+{True} where coqdoc sees a symbol "+{True}") - parentheses, curly brackets and semi-colon not linked in notations Things that can probably be improved: - all notations are indexed in the same category "other"; can we do better? - all non-latin identifiers (e.g. Greek letters) are also indexed in the same "other" category; can we do better? - globalization data for notations could be compacted (currently there is one line per each proper location covered by the notation) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12890 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oops, don't use zeta by default.Gravatar msozeau2010-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12869 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix splitting evars tactics and stop dropping evar constraints whenGravatar msozeau2010-03-15
| | | | | | | | | building a new goal evar defs. Allow customization of the reduction function applied to subtac obligations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12867 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed confusion between number of cstr arguments and number of pattern ↵Gravatar barras2010-03-12
| | | | | | variables (which include let-ins in cstr type) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12864 85f007b7-540e-0410-9357-904b9bb8a0f7
* Consider OccurCheck a catchable exception.Gravatar msozeau2010-03-08
| | | | | | | Fix minor bug in Program wellfounded definitions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12853 85f007b7-540e-0410-9357-904b9bb8a0f7
* Application des patches envoyés par F. Besson pour micromegaGravatar notin2010-03-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12852 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reorder resolution of type class and unification constraints.Gravatar msozeau2010-03-07
| | | | | | | | Fix a bug in dependent elimination when treating defined variables in the context. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12851 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix treatment of remaining unification constraints: raise a moreGravatar msozeau2010-03-07
| | | | | | | | | informative exception if some constraints do not unify. All calls except one used to raise a less informative exception when the constraints weren't solved. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12849 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improvements in generalized rewriting:Gravatar msozeau2010-03-05
| | | | | | | | | | | | | | - support a new strategy: reduction using any of the allowed reduction operators. This strategy does _not_ make the proof size grow. - support rewriting under arbitrary [match with] using a folding strategy. We fold matches to applications of registered [case] combinators and let the user declare the Proper instances for them. - fix the lemma application strategy to correctly report when no progress has been made (avoids loop when repeateadly rewriting with convertible terms). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12844 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a generic tactic option builder. Use it in firstorder to set theGravatar msozeau2010-03-05
| | | | | | | | | default solver (using "Set Firstorder Solver") and for program's obligation tactic. I don't understand exactly the reason of the warning when building states/initial.coq, anyone? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12842 85f007b7-540e-0410-9357-904b9bb8a0f7
* amelioration mineure dans FunctionGravatar jforest2010-03-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12826 85f007b7-540e-0410-9357-904b9bb8a0f7
* Win32 cross-compilation from debian: build of coqide.exe and other binariesGravatar letouzey2010-02-24
| | | | | | | | | | | | Details will follow. In a word, we use a gtk+ win32 bundle from gtk.org to build some (unofficial) mingw32-liblablgtk2 debian packages. Then ./configure -local && ./build win32 is enough to get all native win32 binaries and plugin cmxs from a confortable linux box. Next step: an auto-installer :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12804 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction of bug #2088Gravatar jforest2010-02-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12803 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix sort_dependencies for good, maintaining the initial order.Gravatar msozeau2010-02-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12780 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug in field_simplify_eq inGravatar barras2010-02-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12729 85f007b7-540e-0410-9357-904b9bb8a0f7
* Euclidean division for NArithGravatar letouzey2010-02-10
| | | | | | | | | There was already a Ndiv and Nmod, but hiddent in ZOdiv_def. We higlight it by putting it in a separate file, prove its specification without using Z (but for the moment can't avoid a detour via nat, though), and then instantiate general results from Natural/Abstract/NDiv git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12726 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix [Existing Class] impl and add documentation. Fix computation of theGravatar msozeau2010-02-10
| | | | | | | dependency order of obligations that was not backwards-compatible. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12719 85f007b7-540e-0410-9357-904b9bb8a0f7
* New command Declare Reduction <id> := <conv_expr>.Gravatar letouzey2010-01-28
| | | | | | | | Let's avoid writing huge "Eval ... in ..." lines :-) Will be used in particular soon in NMake for defining function via Definition ... := Eval ... in ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12699 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backport fixes in Instance declarations to Program Instance.Gravatar msozeau2010-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12694 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add [Next Obligation with tactic] support (wish #1953).Gravatar msozeau2010-01-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12691 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2086, error message when we match on an non-inductive type.Gravatar msozeau2010-01-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12669 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Show Obligation TacticGravatar msozeau2010-01-14
| | | | | | | - fix bug #1952. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12668 85f007b7-540e-0410-9357-904b9bb8a0f7
* Support "Local Obligation Tactic" (now the default in sections).Gravatar msozeau2010-01-11
| | | | | | | | Update Numbers that was implicitely using [simpl_relation] instead of the default tactic [program_simpl]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12647 85f007b7-540e-0410-9357-904b9bb8a0f7
* Specific syntax for Instances in Module Type: Declare InstanceGravatar letouzey2010-01-04
| | | | | | | | | NB: the grammar entry is placed in vernac:command on purpose even if it should have gone into vernac:gallina_ext. Camlp4 isn't factorising rules starting by "Declare" in a correct way otherwise... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12623 85f007b7-540e-0410-9357-904b9bb8a0f7
* Few misc. updates.Gravatar herbelin2010-01-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12622 85f007b7-540e-0410-9357-904b9bb8a0f7
* In "simpl c" and "change c with d", c can be a pattern.Gravatar herbelin2009-12-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12608 85f007b7-540e-0410-9357-904b9bb8a0f7
* Opened the possibility to type Ltac patterns but it is not fully functional yetGravatar herbelin2009-12-24
| | | | | | | | | | | | | | | - to type patterns w/o losing the information of what subterm is a hole would need to remember where holes were in "understand", but "understand" needs sometimes to instantiate evars to ensure the type of an evar is not its original type but the type of its instance (what can e.g. lower a universe level); we would need here to update evars type at the same time we define them but this would need in turn to check the convertibility of the actual and expected type since otherwise type-checking constraints may disappear; - typing pattern is apparently expensive in time; is it worth to do it for the benefit of pattern-matching compilation and coercion insertion? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12607 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generic support for open terms in tacticsGravatar herbelin2009-12-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We renounced to distribute evars to constr and bindings and to let tactics do the merge. There are now two disciplines: - the general case is that the holes in tactic arguments are pushed to the general sigma of the goal so that tactics have no such low-level tclEVARS, Evd.merge, or check_evars to do: - what takes tclEVARS and check_evars in charge is now a new tactical of name tclWITHHOLES (this tactical has a flag to support tactics in either the "e"- mode and the non "e"- mode); - the merge of goal evars and holes is now done generically at interpretation time (in tacinterp) and as a side-effect it also anticipates the possibility to refer to evars of the goal in the arguments; - with this approach, we don't need such constr/open_constr or bindings/ebindings variants and we can get rid of all ugly inj_open-style coercions; - some tactics however needs to have the exact subset of holes known; this is the case e.g. of "rewrite !c" which morally reevaluates c at each new rewriting step; this kind of tactics still receive a specific sigma around their arguments and they have to merge evars and call tclWITHHOLES by themselves. Changes so that each specific tactics can take benefit of this generic support remain to be done. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12603 85f007b7-540e-0410-9357-904b9bb8a0f7
* Const_omega: look for S in Init only (avoid future clash with S of Numbers)Gravatar letouzey2009-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12597 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction de la nouvelle option pour functional inductionGravatar jforest2009-12-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12593 85f007b7-540e-0410-9357-904b9bb8a0f7
* adding an option functional_induction_rewrite_dependent to make functional ↵Gravatar jforest2009-12-16
| | | | | | induction using not v8.2 version of subst. By default functional induction uses new version of subst git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12592 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed incorrect computation of possible guard in presence of `{ ... } contexts.Gravatar herbelin2009-12-12
| | | | | | | Also removed used of local_binders_length and local_assums_length which are now incorrect due to the possible presence of `{ ... } contexts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12579 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated compatibility for rewriting equality proofs that are dependentGravatar herbelin2009-12-12
| | | | | | | | | | - made the new "subst'" the default by renaming it "subst"; - renamed old "subst" into "simple subst"; - add option for non-rewriting of dependent proofs in general_rewrite and co - kept use of dependent proofs in the "subst" call of "functional induction", in spite it introduced incompatibilities (in Compcert). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12578 85f007b7-540e-0410-9357-904b9bb8a0f7
* Factorisation between Makefile and ocamlbuild systems : .vo to compile are ↵Gravatar letouzey2009-12-09
| | | | | | | | | | | | in */*/vo.itarget On the way: no more -fsets (yes|no) and -reals (yes|no) option of configure if you want a partial build, make a specific rule such as theories-light Beware: these vo.itarget should not contain comments. Even if this is legal for ocamlbuild, the $(shell cat ...) we do in Makefile can't accept that. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12574 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix the build of coq via ocamlbuildGravatar letouzey2009-12-08
| | | | | | | | - no more plugins/interface - a few missing files in theories.itarget - a few things required Unix now git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12572 85f007b7-540e-0410-9357-904b9bb8a0f7
* Sos.ml: no more warningsGravatar letouzey2009-12-08
| | | | | | | | | apart for a few non-exhaustive patterns, there was also some unused let-in variables. Hard to check whether the apparently useless code is doing some side-effect or not... It seems not, so I've removed completely the corresponding code. Frederic, is that ok ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12570 85f007b7-540e-0410-9357-904b9bb8a0f7
* Continuing r12485-12486 and r12549 (cleaning around name generation)Gravatar herbelin2009-12-02
| | | | | | | | | | - fixed misunderstanding of the role of nenv while simplifying code of occur_id in namegen.ml, - documented the possible incompatibilites in CHANGES - fixed output/Naming.v test, and fixed the count of misc. tests in test-suite/check. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12556 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove interface pluginGravatar glondu2009-12-02
| | | | | | It has moved to the contribs (Sophia-Antipolis/Interface). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12555 85f007b7-540e-0410-9357-904b9bb8a0f7
* Continuing r12485-12486 (cleaning around name generation)Gravatar herbelin2009-12-01
| | | | | | | | | | | | | | | | | | | | | | - backtrack on incompatibility introduced in intro while trying to simplify the condition about when to restart the subscript of a name (the legacy says: find a new name from x0 if the name xN exists in the context but find a new name from xN+1 if the name xN does not exists in the context but is a global to avoid). - made the names chosen by "intro" compliant with the ones printed in the goal and used for "intros until" (possible source of rare incompatibilities) [replaced the use of visibly_occur_id for printing the goal into a call to next_name_away_in_goal] - also made the names internal to T in "T -> U" printed the same in the goal as they are while printing T after it is introducted in the hypotheses [non contravariant propagation of boolean isgoal in detype_binder] - simplified a bit visibly_occur_id (the Rel and Var cases were useless as soon as the avoid list contained the current env); still this function is costly with polynomial time in the depth of binders - see file output/Naming.v for examples git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12549 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added support for definition of fixpoints using tactics.Gravatar herbelin2009-11-27
| | | | | | | | | | | | Fixed some bugs in -beautify and robustness of {struct} clause. Note: I tried to make the Automatic Introduction mode on by default for version >= 8.3 but it is to complicated to adapt even in the standard library. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12546 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-18 05:45:21 +0000