aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2011-07-29Ring: replaced various generic = on constr by eq_constr, destructors etc.puech
2011-07-29Quote: replaced various generic = on constr by eq_constr, destructors etc.puech
2011-07-29Newring: generic = on constr replaced by eq_constrpuech
2011-07-29Coq_micromega: generic = on constr replaced by eq_constrpuech
2011-07-29Field: generic Gmap on constr replaced by Cmappuech
2011-07-29Extract_env: generic = on prec_declaration replaced by prec_declaration_equalpuech
2011-07-29Extraction: replace generic = on mutual_inductive_body by mib_equalpuech
2011-07-29replaced some generic = on constr by eq_constrpuech
2011-07-29Subtac_cases: replaced some generic = on constr by destructorspuech
2011-07-29Ring: replaced some generic Pervasives.compare on constr by constr_ordpuech
2011-07-29Nsatz: replaced some generic = on constr by eq_constrpuech
2011-07-29Recdef: replaced some generic = on constr by eq_constrpuech
2011-07-29FourierR: replaced some generic Hashtbl on constr by Constrhashpuech
2011-07-29Refl_omega: replaced generic = on constr by eq_constrpuech
2011-07-29Newring: replaced some generic = on constr by eq_constrpuech
2011-07-29Refl_omega: replaced some generic = on constr by eq_constrpuech
2011-07-29Const_omega: replaced some generic = on constr by eq_constrpuech
2011-07-29Functional_principles_types: replaced some generic = on constr by eq_constrpuech
2011-07-29Newring: replaced generic = on constr by eq_constrpuech
2011-07-29Coq_omega: replaced generic = on constr by eq_constrpuech
2011-07-29Quote: replaced generic = on constr by eq_constrpuech
2011-07-29Coq_omega: replaced many generic = on constr by eq_constrpuech
2011-07-29Newring: generic Pervasives.compare on constr replaced by constr_ordpuech
2011-07-29Term: moved function constr_ord (a.k.a compare_constr) from Sequent to Termpuech
2011-07-29Ccalgo, Ccproof: multiple generic Hashtbl on constr and term replaced by Cons...puech
2011-07-29Newring: generic equality on constr replaced by constr_equalpuech
2011-07-29Ccproof: generic equality on term replaced by term_equalpuech
2011-07-29Sequent: generic equality on global_reference replaced by RefOrdered.comparepuech
2011-07-29Sequent: generic equality on kernel_name replaced by kn_ordpuech
2011-07-29Sequent: generic equality on constr replaced by destructorspuech
2011-07-29Sequent: generic equality on ident replaced by id_ordpuech
2011-07-29Instances: generic equality on global_reference replaced by RefOrdered.comparepuech
2011-07-29Unify: generic equality on constr replaced by eq_constrpuech
2011-07-26Integral domainspottier
2011-07-26Ring2 devient Ncring et la reification par les type classes est partageepottier
2011-07-22Add a syntax entry for fully applied constructor patternpboutill
2011-07-04Set Extraction KeepSingleton: an option for not decapsulating singleton typesletouzey
2011-07-04Extraction: in haskell, __ may have any type, no need to unsafeCoerce itletouzey
2011-07-04Extraction: in haskell, type signatures for __ and unsafeCoerce (fix #2552)letouzey
2011-07-04Extraction: forbid Prop-polymorphism of inductives when extracting to Ocamlletouzey
2011-06-30Fix compilation errormsozeau
2011-06-30Keep obligation source information in Programmsozeau
2011-06-29update of Micromega docfbesson
2011-06-28Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_defletouzey
2011-06-28improved tactic namesfbesson
2011-06-24Numbers: a particular case of div_uniqueletouzey
2011-06-21Follow-up concerning eqb / ltb / leb comparisonsletouzey
2011-06-21Cleaning debugging printer relative to new proof engine. Inherbelin
2011-06-18Relaxed the constraint introduced in r14190 that froze the existingherbelin
2011-06-17Fix bug 2269, program typechecker not used in Instance conclusionsmsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 08:11:37 +0000