aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evarsolve.ml
AgeCommit message (Collapse)Author
2014-04-23Better representation of evar filters: we represent the vacuous filters ofPierre-Marie Pédrot
any length with a [None] representation and ensure that this representation is canonical through the restricted interface.
2014-04-04Fixing #3262 which revealed a non-progressing, hence looping,Hugo Herbelin
refinement of evars (in filter_candidates). Incidentally introduced a copy of type "option", "update", which highlights the specific intention of "updating" or not.
2014-04-01Propagating conversion_problem towards (postponed) evar/evar problems.Hugo Herbelin
Incidentally simplifies where evar/evar problems are treated (in evar_define and imitate rather than solve_simple_eqn).
2014-04-01Fixing bug #2900 (evar/evar unif was supposed to be treated inHugo Herbelin
solve_simple_eqn but in case the second evar was hidden behind a local variable, it arrived in evar_define and imitate, wrongly assuming progress).
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
The removed code isn't used locally and isn't exported in the signature
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
2013-10-29- install evar printer for debuggingmsozeau
- make unification try canonical structures before expansion as in evar_conv - add a fast path to evar inversion (patch from B. Ziliani). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16945 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-27Removing useless filter allocation in evar construction.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16940 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-27Abstracting evar filter away. The API is not perfect, but better than nothing.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16939 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
To reduce the amount of syntactic noise, we now provide a few inner modules Int.List, Id.List, String.List, Sorts.List which contain some monomorphic (or semi-monomorphic) functions such as mem, assoc, ... NB: for Int.List.mem and co we reuse List.memq and so on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16936 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-23cList: a few alternative to hashtbl-based uniquize, distinct, subsetletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16924 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-22Removing some generic equalities.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16915 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-22Removing useless array-to-list and converse casts used inppedrot
Evar{conv,solve} files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16913 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-22Optimizing evar filters. It seems to cost quite a lot in unification,ppedrot
as witnessed by profiling on time-consuming files. I suspect we can do better by using a smarter representation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16912 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-27Removing a bunch of generic equalities.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ↵xclerc
with OCaml 3.12.1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
casts of ints to evars. - 2 in Evarutil and Goal which are really needed, even though the Goal one could (and should) be removed; - 2 in G_xml and Detyping that are there for completeness sake, but that might be made anomalies altogether; - 1 in Newring which is quite dubious at best, and should be fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16786 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-14Fixing a regression in unification introduced in r16205 (error raisedherbelin
by solve_candidates was not anymore handled at the expected time). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16524 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
1. sorts.ml: A small file utility for sorts; 2. constr.ml: Really low-level terms, essentially kind_of_constr, smart constructor and basic operators; 3. vars.ml: Everything related to term variables, that is, occurences and substitution; 4. context.ml: Rel/Named context and all that; 5. term.ml: derived utility operations on terms; also includes constr.ml up to some renaming, and acts as a compatibility layer, to be deprecated. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16462 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-21Fixing unfolding of local definitions during unification that appearedherbelin
with commit r16233. This commit added a more precise filtering of variables on which an evar was allowed to be dependent, but) but it also broke some Ssreflect scripts. The reason why that filtering was incorrectly applied, sometimes, to local definitions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16346 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-21Cosmetic code contraction in evarsolve.ml + test sur unification avec let-in.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16344 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-18Fix for bug #3004 (thanks Hugo!)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16317 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-17Retyping.get_type_of: a lax version raising no anomaliesletouzey
There are at least two situations (in Evarsolve and Pretyping) where Retyping.get_type_of may be called on ill-typed terms, leading to possible anomalies that used to be immediately catched and discarded. Instead, retyping.get_type_of now has an extra optional arg ~lax that makes it fail with a regular exception instead of anomalies. Of course, it would be best someday to be able to avoid using get_type_of on possibly ill-typed terms... If somebody wants to investigate this: - example that leads the get_type_of in Pretyping to a failure: test-suite/succes/ltac.v - example that leads the get_type_of in Evarsolve to a failure: MathClasses/implementations/list.v, a rewrite line 42 (* :-) *) cf bench failure on 2013-3-15. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16308 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 12)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16289 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-28Repairing r16205: errors raised by check_evar_instance were no longerherbelin
trapped by solve_simple_eqn. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16257 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-21A slightly more efficient test of well-typedness of restriction ofherbelin
evars (though this might be slighty more costly). This incidentally solves Appel's part of bug #2830 even though a conceptual problem around the interaction of unification with the proof engine has to be solved. Indeed, what to do when unification, called as part of a tactic, solves or refines the current goal by side effect. Somehow, unifyTerms or tclEVARS should take this possibility into consideration, either by forbidding the refinement of the current goal by side effect, or by acknowledging this refinement by producing new subgoals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16232 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-17Added propagation of evars unification failure reasons for betterherbelin
error messages. The architecture of unification error handling changed, not helped by ocaml for checking that every exceptions is correctly caught. Report or fix if you find a regression. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16205 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-10Splitted Evarutil in two filesppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16195 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 16:28:15 +0000