aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Collapse)Author
2013-05-24Code cleaning in Matching.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16531 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-14Mini documentation (evar_absorb_arguments).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16527 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-14Delayed the computation of parameters in sort polymorphism ofherbelin
inductive types. This saves some computation, but also allows incidentally to retype terms with evars without failing if an inductive type as an argument whose type is an evar. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16526 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-14"change ... in ..." and "simpl ... in ..." now consider nestedherbelin
occurrences (possible source of incompatibilities since this alters the numbering of occurrences). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16525 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-05-14Removing Gmap from Classops. Fold order only mattered for printing.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16521 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-14Removing useless uses of Gmap.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16520 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-14Replacing compatibility layer for Fmap in Typeclasses. Code wasppedrot
actually almost fold-order irrelevant (only changes printing order). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16518 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-14More semantical-friendly function.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16517 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-12Use the Hook module here and there.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16510 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-11Fixing a source of evars leak, revealed by contrib QuicksortComplexityherbelin
after r16499 which replaced a check for visible undefined evars (check_evars) by a check for undefined evars in the evar map (check_evars_are_solved). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16508 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-10Little oversight in commit r16489 (fix for bug #3036).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16506 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-09A uniformization step around understand_* and interp_* functions.herbelin
- Clarification of the existence of three algorithms for solving unconstrained evars: - the type-class mechanism - the heuristics for solving pending conversion problems and multi-candidates - Declare Implicit Tactic (when called from tactics) Main function for solving unconstrained evars (when not using understand): Pretyping.solve_remaining_evars - Clarification of the existence of three corresponding kinds of errors when reporting about unsolved evars: Main function for checking resolution of evars independently of the understand functions: Pretyping.check_evars_are_solved - Introduction of inference flags in pretyping for governing which combination of the algorithms to use when calling some understand function; there is also a flag of expanding or not evars and for requiring or not the resolution of all evars - Less hackish way of managing Pretyping.type_constraint: all three different possibilities are now represented by three different constructors - Main semantical changes done: - solving unconstrained evars and reporting is not any longer mixed: one first tries to find unconstrained evars by any way possible; one eventually reports on the existence of unsolved evars using check_evars_are_solved - checking unsolved evars is now done by looking at the evar map, not by looking at the evars occurring in the terms to pretype; the only observed consequence so far is in Cases.v because of subterms (surprisingly) disappering after compilation of pattern-matching - the API changed, see dev/doc/changes.txt Still to do: - Find more uniform naming schemes: - for distinguishing when sigma is passed as a reference or as a value (are used: suffix _evars, prefix e_) - for distinguishing when evars are allowed to remain uninstantiated or not (are used: suffix _evars, again, suffix _tcc, infix _open_) - be more consistent on the use of names evd/sigma/evars or evdref/evars - By the way, shouldn't "understand" be better renamed into "infer" or "preinfer", or "pretype". Grammatically, "understanding a term" looks strange. - Investigate whether the inference flags in tacinterp.ml are really what we want (e.g. do we really want that heuristic remains activated when typeclasses are explicitly deactivated, idem in Tacinterp.interp_open_constr where flags are strange). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16499 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-09A few comments in evarconv.mli.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16498 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-09Uniformization: isevars -> evdref/sigma/evdherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16497 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-08Uniformizing the [if_warn] flag used for warning printing and putppedrot
it into the standard logger instead. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16491 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-08Protection against "Bad recursive type" in w_unify0 (bug #3036).herbelin
Morally, unification wants to unify "fun x:Meta => Meta" with "fun x:nat => match x with ... end". Retyping is asked to type "match x with ... end" in the context "x:Meta" where the type of x has de facto been lost. Retyping fails. I don't see an easy remedy since w_unify0 builds the unifier lazily, and I'm not sure it is worth to propagate the unifier to retyping so that it knows it. After all, the call to retyping in w_unify0 is not so critical. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16489 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-06Fixing ocamldoc compilation.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16483 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-06Small cleaning of Evd interface.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16482 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-06States: frozen states can hold closuresgareuselesinge
States.freeze takes ~marshallable:bool, so that (only) when we want to marshal data to disk/network we can ask the freeze functions of the summary to force lazy values. The flag is propagated to Lib and Summary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16478 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-05Hack to solve a "Bad recursive type" anomaly.herbelin
Retyping expects its argument already well-typed. However, if unification problems are not fully solved, a term to match can have an evar type together with the constraint that this evar has to be convertible to some given inductive type. One could have tried to have a more eager resolution of unification constraint but I'm afraid of the cost in comparing c=c' in general in "?x[c] = c'" unification problems, so I instead added a hack in retyping to recover the constraint. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16471 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-03Removing a redundant function from Evd.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16465 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-30Fix wrong computation of dependency signature in cases raising an uncaught ↵msozeau
exception later. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16464 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-29Merging Context and Sign.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16463 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-04-22code simplifications concerning Summaryletouzey
- Most of the time, the table registered via Summary.declare_summary is just a single reference. A new function Summary.ref now allows to both declare this ref and register it to summary in one shot. - Clarifications concerning the role of [init_function]. For statically registered tables that don't need a special initializer, just do nothing there (see the new Summary.nop function). Beware: now that Summary exports a function named "ref", any code that do an "open Summary" will probably fail to compile. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16441 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-18Finer fix for bug 3017, mark unresolvability only of goals that aremsozeau
instances of metas in clenvtac. Makes Math-Classes compile again. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16429 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-18Fix #3001 (rename arg of global cst inside section)gareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16426 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-17Matching patterns: fixed allow_partial_app which was not working onherbelin
unnamed Metas; also added matching an applicative prefix (with non-meta head) of a term against a pattern, to be used by "Search" (i.e. SearchHead). This allows "Search" and "SearchPattern" to behave as in 8.4. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16422 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-17Fix of r16257 in r16205 for "errors raised by check_evar_instance wereherbelin
no longer trapped by solve_simple_eqn" was incomplete because "try ... with E as e | e when f e -> ..." means "try ... with (E as e | e) when f e -> ..." and not "try ... with E as e | (e when f e) -> ...". This was the cause for examples 2615.v and 2670.v failing since March 1. The need for "as e" should have warned me. Sorry for the mistake. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16420 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-17Like in r16346, do not filter local definitions (here in theherbelin
type-based second-order unification algorithm). In type-based second-order unification algorithm, protect local definitions in instances of evars to wrongly be considered as potentially flexible. Altogether, this fixes the anomaly in #3003 (even if some additional work has to be done to improve the resulting error message, see next commit). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16414 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-03Fix for bug #3017: wrong handling of the unresolvability statusmsozeau
in clenvtac and error-printing code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16383 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-30Continuation of r16346 on filtering local definitions. Refinedherbelin
the "choose less dependent" constraint-solving heuristic so that it is not disturbed by local definitions. This is a quick fix. A deeper analysis of the structure of constraints of the form ?x[args] = y, determining if variable y can itself be a local def or not, and whether args can be let-ins aliasing other variables, would allow to know if the fix needs to be refined further. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16376 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-25Native compiler: timing info for reification in debug mode.mdenes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16357 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-25Fix bug #2989: make unification.ml able to deal with canonical structure in ↵pboutill
any context + reindenting noise git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16354 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-25 Comments in mlipboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16352 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-23Minor code cleaning in CArray / CList.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16351 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-22Fix bug# 2994, 2971 about better error messages.msozeau
Fix bug# 2956, porting fix from 8.4 branch git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16349 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-21Using hnf instead of "intro H" for forcing reduction to a product.herbelin
Added full betaiota in hnf. This seems more natural, even if it changes the strict meaning of hnf. This is source of incompatibilities as "intro" might succeed more often. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16338 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-21Fixing an old pecularity of "red": head betaiota redexes are nowherbelin
reduced in order to find some head constant to reduce. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16337 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-20Check a list length before doing a List.chop (fix #3000)letouzey
I'm not completely sure that raising Not_found is the right thing to do here, but it seems reasonable... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16326 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-17Avoid a few overzealous "when Errors.noncritical"letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16309 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-14Typo in an error messageletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16303 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-03-13Restrict (try...with...) to avoid catching critical exn (part 7)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16283 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 5)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16281 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 15:38:10 +0000