aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2011-08-04Fix unification: detect invalid evar instantiations due to scoping earlier.msozeau
2011-08-03Fix nf_evars_undefined use in pr_constraintsmsozeau
2011-08-03Fix nf_evars_undefinedmsozeau
2011-08-02Patch to simplify is_open_canonical_projectionherbelin
2011-08-02More robust evar_map debugging printerherbelin
2011-08-01Term: simplify compare_constr by removing calls to decompose_apppuech
2011-08-01Added .dir-locals file to take advantage of emacs 23's new Directory-local va...puech
2011-08-01fixed bug 2580. Quick fix: copy emitcodes before patching itbarras
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-29generic = on named_context replaced by named_context_equalpuech
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-29Tactics: replace generic = on constr by destructorspuech
2011-07-29Auto: replace generic compare on pri_auto_tactic by pri_auto_tactic_ordpuech
2011-07-29Extraction: replace generic = on mutual_inductive_body by mib_equalpuech
2011-07-29Evarutil: replace generic list_distinct on constr by constr_list_distinctpuech
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-29Add printer dependency to Hashtbl_alt (used in Term)puech
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-29Evarutil: replaced some generic = on constr by destructorspuech
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-29Hahtbl_alt: separate generic combine functionspuech
2011-07-29Newring: generic equality on constr replaced by constr_equalpuech
2011-07-29Ccproof: generic equality on term replaced by term_equalpuech
2011-07-29Tactics: generic equality on constr replaced by eq_constrpuech
2011-07-29Class_tactics: generic equality on named_context_val replaced by eq_named_con...puech
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-11 12:22:30 +0000