aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Collapse)Author
2011-09-16Omega: for non-arithmetical goals, try proving False from context (wish #2236)letouzey
This way, no more error messages like "Unrecognized predicate". Some code simplification and reorganization on the way, in particular a few tests like "is_Prop ..." or "closed0 ..." were actually useless. Also add support for the situation H:~Zne x y for uniformity. Beware: scripts relying negatively on the strength of omega may have to be adapted (e.g. "try omega. some_more_tactics_in_case_omega_fails."). For instance, one line deletion in PermutSetoid.v Probably more cumbersome : "auto with *" becomes stronger since it may call omega. Todo : check the impact on contribs tomorrow. Btw, this commit seems to solve a bug where omega was to be guided by some (set foo:= ...) before being able to succeed (cf PermutSetoid.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14474 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-15Omega aware of Z.pred (fix #1912)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14472 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-09correction du bug 2047jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14465 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-06Improved ltac code for zify (fix #2575).letouzey
Note nonetheless that the underlying bug is still active (cf. #2602), I've just written the ltac stuff in a nicer way (no nested match goal), and things happen to work now :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14461 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-05Extraction Implicit: fix the numbering of constructor argumentsletouzey
For constructors, the numbers of parameters used to be wrongly ignored. Consider for instance : Inductive listn (A:Type) : nat -> Type := | niln : listn A 0 | consn : forall n, A -> listn A n -> listn A (S n). Saying "Extraction Implicit consn [n]" should now work correctly, and correspond to the alternative syntax "Extraction Implicit consn [2]", where 2 is the position of the argument n when counting with inductive parameters. Note that saying "Extraction Implicit consn [1]" (or [A]) is now a no-op : constructors have always been cleaned-up from their parameters during extraction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14449 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-02Bug 2589: Documentation patch of Hendrik Tewspboutill
+ s/cbv/lazy of bug 2542 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14446 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-25Extraction: allow extraction of records with anonymous fields (fix #2555)letouzey
For Ocaml, we now use the extraction-reserved substring "__" : The name foo__i will be pick for i-th field of record foo if it is anonymous. For Haskell, still no printing of records as native records, hence nothing to do. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14420 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-08New proposition "rewrite Heq in H" for eq_rect (assuming that there isherbelin
a smaller risk that "rewrite" clashes with a name used for constr). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14390 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-08Esubst: make types of substitutions & lifts privatepuech
Allows to be sure that we apply the smart constructors. Propagate the change to Closure, Reduction, Term, Cbv and Newring git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14386 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-04moins de reification inutile, noatations standardspottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14385 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Ring: replaced various generic = on constr by eq_constr, destructors etc.puech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14375 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Quote: replaced various generic = on constr by eq_constr, destructors etc.puech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14374 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Newring: generic = on constr replaced by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14372 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Coq_micromega: generic = on constr replaced by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14371 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Field: generic Gmap on constr replaced by Cmappuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14370 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Extract_env: generic = on prec_declaration replaced by prec_declaration_equalpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14369 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Extraction: replace generic = on mutual_inductive_body by mib_equalpuech
Term: add function eq_rel_declaration git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14366 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29replaced some generic = on constr by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14364 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Subtac_cases: replaced some generic = on constr by destructorspuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14363 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Ring: replaced some generic Pervasives.compare on constr by constr_ordpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14362 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Nsatz: replaced some generic = on constr by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14360 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Recdef: replaced some generic = on constr by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14359 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29FourierR: replaced some generic Hashtbl on constr by Constrhashpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14358 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Refl_omega: replaced generic = on constr by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14357 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Newring: replaced some generic = on constr by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14356 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Refl_omega: replaced some generic = on constr by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14355 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Const_omega: replaced some generic = on constr by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14354 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Functional_principles_types: replaced some generic = on constr by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14353 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Newring: replaced generic = on constr by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14351 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Coq_omega: replaced generic = on constr by eq_constrpuech
Util: Added list_assoc_f git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14350 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Quote: replaced generic = on constr by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14349 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Coq_omega: replaced many generic = on constr by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14348 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Newring: generic Pervasives.compare on constr replaced by constr_ordpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14347 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Term: moved function constr_ord (a.k.a compare_constr) from Sequent to Termpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14346 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Ccalgo, Ccproof: multiple generic Hashtbl on constr and term replaced by ↵puech
Constrhash and Termhash We need a function hash_constr (added in Term) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14345 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Newring: generic equality on constr replaced by constr_equalpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14343 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Ccproof: generic equality on term replaced by term_equalpuech
... and define term_equal git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14342 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Sequent: generic equality on global_reference replaced by RefOrdered.comparepuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14339 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Sequent: generic equality on kernel_name replaced by kn_ordpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14338 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Sequent: generic equality on constr replaced by destructorspuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14337 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Sequent: generic equality on ident replaced by id_ordpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14336 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Instances: generic equality on global_reference replaced by RefOrdered.comparepuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14335 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Unify: generic equality on constr replaced by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14334 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-26Integral domainspottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14299 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-26Ring2 devient Ncring et la reification par les type classes est partageepottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14298 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-22Add a syntax entry for fully applied constructor patternpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14292 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-04Set Extraction KeepSingleton: an option for not decapsulating singleton typesletouzey
A informative inductive type with one constructor C and one informative arg to C is normally extracted as an identity, with C removed, see for example the "sig" type. When this new option is set, these singleton types are left untouch, providing extracted code which is closer to the initial Coq development. Feature requested by Wouter Swiestra. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14260 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-04Extraction: in haskell, __ may have any type, no need to unsafeCoerce itletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14258 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-04Extraction: in haskell, type signatures for __ and unsafeCoerce (fix #2552)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14257 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-04Extraction: forbid Prop-polymorphism of inductives when extracting to Ocamlletouzey
A particular case in sort-polymorphism of inductive types allows an informative type (such as prod) to have instances in Prop: (I,I) : True * True : Prop This is due to the fact that prod is a singleton type: indeed (I,I) has no informative content. But this invalidates an important invariant for the correctness of the extraction: inductive constructors stop having always the same sort as their inductive type. Consider for instance: Definition f (X:Type)(x:X*X)(g:X->nat) := g (fst x). Definition test := f _ (I,I) (fun _ => 0). Then the inductive element (I,I) is extracted as a logical part __, but during a strict evaluation (i.e. in Ocaml, not Haskell), this __ will be given to fst, and hence to a match, leading to a nasty result (potentially segfault). Haskell is not affected, since fst is never evaluated. This patch adds a check for this situation during any Ocaml extraction, leading for the moment to a fatal error. Some functions in inductive.ml and retyping.ml now have an extra optional argument ?(polyprop=true) that should stay untouched in regular Coq usage, while type-checking done during extraction will disable this prop-polymorphism. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14256 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 10:27:04 +0000