aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
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
2011-06-16Tests de nsatz avec la geometriepottier
2011-06-10Moved allow_K to a unification flagherbelin
2011-06-10Call process_vernac_interp_error before calling Errors.print inherbelin
2011-06-10Revert "Check if recursive calls are guarded before printing "Proof completed"."pboutill
2011-06-10ring2, cring, nsatz avec type classe avec parametres plus notationspottier
2011-06-07Fix bug #2399 in Program: used to build an ill-formed term due to a de Bruijn...msozeau
2011-06-07Fix bug #2415: warn when closing modules or sections and some obligations are...msozeau
2011-05-26Check if recursive calls are guarded before printing "Proof completed".herbelin
2011-05-25Q2R -> IQRfbesson
2011-05-24Made the emacs-U option deprecated. Also removed the old codecourtieu
2011-05-23git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14152 85f007b7-540e-0...fbesson
2011-05-20added support to handle division by a constant over Rfbesson
2011-05-19Extraction: avoid lots of late mind_of_knletouzey
2011-05-19Extraction: global reference should be indexed on their user part (fix #2540)letouzey
2011-05-18cbv delta - [...] before calling liafbesson
2011-05-18apply zeta reduction before syntaxificationfbesson
2011-05-18Extraction: avoid printing of Recursive Extraction in coqide's consoleletouzey
2011-05-16Fixed my last patch: these files no longer use nat_beq (automaticallyvsiles
2011-05-13A new mechanism to handle errors.aspiwack
2011-05-11Print Module (Type) M now tries to print more detailsletouzey
2011-05-09Improved lia + experimental nliafbesson
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 11:11:28 +0000