aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2011-08-08Term: fix hash_constr to hash modulo casts & names (like compare_constr)puech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14387 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-08Esubst: make types of substitutions & lifts privatepuech
Allows to be sure that we apply the smart constructors. Propagate the change to Closure, Reduction, Term, Cbv and Newring git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14386 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-04moins de reification inutile, noatations standardspottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14385 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-04Fix unification: detect invalid evar instantiations due to scoping earlier.msozeau
Add a debug printer for existential sets (used for frozen_evars in w_unify). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14384 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-03Fix nf_evars_undefined use in pr_constraintsmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14383 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-03Fix nf_evars_undefinedmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14382 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-02Patch to simplify is_open_canonical_projectionherbelin
(courtesy from François Garillot) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14381 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-02More robust evar_map debugging printerherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14380 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-01Term: simplify compare_constr by removing calls to decompose_apppuech
I think the additional check was here for historical reasons (before the invariant on Apps was enforced) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14379 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-01Added .dir-locals file to take advantage of emacs 23's new Directory-local ↵puech
variables. These variables are set whenever we open a file in the source tree. It sets: * the default directory where to launch compilation (the root directory) * the TAGS file location * the camldebug command git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14378 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-01fixed bug 2580. Quick fix: copy emitcodes before patching itbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14376 85f007b7-540e-0410-9357-904b9bb8a0f7
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-29generic = on named_context replaced by named_context_equalpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14373 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-29Tactics: replace generic = on constr by destructorspuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14368 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 11:08:26 +0000