aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Collapse)Author
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
2011-06-30Fix compilation errormsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14252 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-30Keep obligation source information in Programmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14251 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-29update of Micromega docfbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14248 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-28Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_defletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14244 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-28improved tactic namesfbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14242 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-24Numbers: a particular case of div_uniqueletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14238 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-21Follow-up concerning eqb / ltb / leb comparisonsletouzey
- All statement using reflect are made transparent. (Otherwise, since reflect isn't in Prop, extraction complains now about opaque Type definition). - remove two local Peqb_spec and Neqb_spec, now provided globally as Pos.eqb_spec and N.eqb_spec. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14232 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-21Cleaning debugging printer relative to new proof engine. Inherbelin
particular, new printer for evar_map which displays undefined evars + defined evars that were instantiated by these undefined evars and recursively, up to some arbitrary level n chosen to be in practice n=2 (thanks to Arnaud). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14231 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-18Relaxed the constraint introduced in r14190 that froze the existingherbelin
evars when rewriting. Use it for autorewrite and subst. Accept evars instantiation in multi_rewrite so that rewrite alone remains compatible (it is used in contribs, e.g. Godel, in places where it does not seem absurd to allow it), but there are no good reason for it. Comments welcome. + addition of some tests for rewriting (one being related to commit 14217) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14222 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-17Fix bug 2269, program typechecker not used in Instance conclusionsmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14212 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 18:45:50 +0000