aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2011-07-29Auto: replace generic compare on pri_auto_tactic by pri_auto_tactic_ordpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14367 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-29Evarutil: replace generic list_distinct on constr by constr_list_distinctpuech
This new function is a copy of Util's one, but working on Constrhash git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14365 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-29Add printer dependency to Hashtbl_alt (used in Term)puech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14361 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-29Evarutil: replaced some generic = on constr by destructorspuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14352 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-29Hahtbl_alt: separate generic combine functionspuech
... and report changes on Term git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14344 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-29Tactics: generic equality on constr replaced by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14341 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Class_tactics: generic equality on named_context_val replaced by ↵puech
eq_named_context_val git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14340 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-29Eqschemes: generic equality on constr replaced by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14333 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Evarutil: generic equality on constr replaced by destructorspuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14332 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Heads: generic equality on constr replaced by destructorpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14331 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Environ: generic equality on named_context replaced by named_context_equalpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14330 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Evarconv: generic equality on constr replaced by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14329 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Equality: generic equality on constr replaced by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14328 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Cases: generic equality on constr replaced by destructorspuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14327 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Tactics: generic equality on constr replaced by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14326 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Classops: generic equality on constr replaced by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14325 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Class: generic equality on constr replaced by destructorspuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14324 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Evarutil: generic equality on constr replaced by eq_constr (x2)puech
added array_equal in Util git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14323 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Equality: generic equality on constr replaced by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14322 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Tactics: generic equality on constr replaced by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14321 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Tactics: generic equality on named_declaration replaced by eq_named_declarationpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14320 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Term: added function eq_named_declarationpuech
We need to move eq_constr upwards git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14319 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Evarutil: generic equality on constr replaced by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14318 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-31 19:52:06 +0000