aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Collapse)Author
2011-02-03Repair Class_tactics.split_evars, broken by r13717 (should fix #2481)letouzey
After r13717, we concentrate on undefined evars. But doing so too naively was breaking Class_tactics.split_evars, since defined evars may point to undefined ones. We should not ignore them, but rather traverse them, which is now done by functions Evarutil.undefined_evars_of_* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13809 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-27Make simpl use the proper constant when folding (mutual) fixpointsletouzey
Before this commit, when simpl was finding the constant name for folding some (mutual) fixpoint, this was done via some repr_con followed by make_con. Problem: this doesn't preserve the canonical part of a Names.constant. For instance the following script was buggish: Module M. Fixpoint foo n := match n with O => O | S n => bar n end with bar n := match n with O => O | S n => foo n end. End M. Module N. Include M. (* foo, bar have here "user name" N but "canonical name" M *) Eval simpl in (fun x => bar (S x)). (* Anomaly: uncaught exception Failure "Cannot print a global reference". *) (* since simpl has produce a different bar with both user and canonical N *) TODO : check all other uses of make_con in the rest of the sources... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13803 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-11ratrapage exception, deja fait ...bgregoir
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13782 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-07Fixing an uncaught exception bug with use of vmcastherbelin
(backport from 8.3) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13781 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-07mli comments for docpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13773 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-25Rename mkR* smart constructors (mostly in funind)glondu
perl -pi -e 's/(mk)R(Ref|Var|Evar|PatVar|App|Lambda|Prod|LetIn|Case s|LetTuple|If|Rec|Sort|Hole|Cast|Dynamic|Prop|Type|Fix|CoFix|Struct Rec|WfRec|MeasureRec)/\1G\2/g' **/*.ml* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13758 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-24More {raw => glob} changes for consistencyglondu
perl -pi -e 's/(\W|_)raw((?:sort|_prop|terms?|_branch|_red_flag|pat tern|_constr_of|_of_pat)(?:\W|_))/\1glob_\2/g;s/glob__/glob_/g;s/(\ W)R((?:Prop|Type|Fix|CoFix|StructRec|WfRec|MeasureRec)\W)/\1G\2/g;s /glob_terms?/glob_constr/g' **/*.ml* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13756 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-23Rename rawterm.ml into glob_term.mlglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13744 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
There was a discrepancy of the notions "raw" and "globalized" between constrs and tactics, and some confusion of the notions in e.g. genarg.mli (see all globwit_* there). This commit is a first step towards unification of terminology between constrs and tactics. Changes in module names will be done separately. In extraargs.ml4, the "ARGUMENT EXTEND raw" and related stuff, even affected by this change, has not been touched and highlights another confusion in "ARGUMENT EXTEND" in general that will be addressed later. The funind plugin doesn't respect the same naming conventions as the rest, so leave some "raw" there for now... they will be addressed later. This big commit has been generated with the following command (wrapped here, but should be on a *single* line): perl -pi -e 's/(\W(?:|pp|pr_l)|_)raw((?:constrs?|type|vars|_binder| _context|decl|_decompose|_compose|_make)(?:\W|_))/\1glob_\2/g;s/glo b__/glob_/g;s/prraw/prglob/g;s/(\W)R((?:Ref|Var|Evar|PatVar|App|Lam bda|Prod|LetIn|Cases|LetTuple|If|Rec|Sort|Hole|Cast|Dynamic)\W)/\1G \2/g' `git ls-files|grep -v dev/doc/changes.txt` git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13743 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-19Fixing bug #2454: inversion predicate strategy for inferring the typeherbelin
of "match" is not general enough; if there is a non dependent type constraint, we also try w/o inversion predicate in the return clause. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13727 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-18Univ.constraints made fully abstract instead of being a Set of abstract stuffletouzey
No need to tell the world about the fact that constraints are implemented via caml's Set. Other modules just need to know about the empty and union functions (and addition functions "enforce_geq" and "enforce_eq" that were already there). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13725 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-15Misc improvements about evar_mapletouzey
- A Evd.defined_evars to keep only this part of the evar_map - One Evd.fold less in Typeclasses.mark_unresolvables - We check that only undefined evar_map could be set unresolvable - A duplicated function in himsg.ml TODO: some calls to Evd.fold(_undefined) would be faster if written as Map.map or Map.mapi. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13716 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-08Refresh universes in params when generating schemes (Closes: #2429)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13631 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-07Delayed the evar normalization in error messages to the last minuteherbelin
before the message is delivered to the user. Should avoid useless computation in heavily backtracking tactics (auto, try, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13628 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-31An experimental support for open constrs in hints and in "using"herbelin
option of "auto". Works for not too complicated hints (e.g. "@pair _ _ 0"). Would be simpler if make_apply_entry supported lemmas containing evars. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13598 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-31Cleaning the use of parentheses around evd and evdref (cosmetic commit).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13597 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-31Slight cosmetic cleaning of tacred.ml.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13593 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-06Fixing the Not_found error in bug #2404 + dead code removal in cases.mlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13511 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-30Improve handling of metas as evars in unification (patch by Hugo)letouzey
Pratical situation: simple eapply foo on a goal ?123, while foo is a (forall f, exists ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13479 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-30Speed-up refine by avoiding some calls to Evd.foldletouzey
Instead of the full Evd.fold, Evd.fold_undefined seems enough in - Evarutil.push_dependent_evars - the nf_evars call in Evarutil.evars_to_metas (we hence create a function nf_evars_undefined and use it there) This should bring back Compcert into reasonable compilation time git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13478 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-28Fix bug #2321, allowing "_" named projections in classes. Not realizingmsozeau
the wish to allow named projections to not be put in the canonical structures databases for Structures. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13474 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-28Remove some occurrences of "open Termops"glondu
Functions from Termops were sometimes fully qualified, sometimes not in the same module. This commit makes their usage more uniform. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13470 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-28Remove "init" label from Termops.it_mk* specialized functionsglondu
These functions are applied much more often without labels than with them (the alternate of adding the label wherever relevant changes 124 lines instead of 41). Moreover, this is more consistent with the Term module and there is no ambiguity in argument types. This commit goes towards elimination of occurrences of OCaml warning 6. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13468 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
In particular, the unused lib/tlm.ml and lib/gset.ml are removed In addition, to simplify code, Libobject.record_object returning only the ('a->obj) function, which is enough almost all the time. Use Libobject.record_object_full if you really need also the (obj->'a). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13460 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-20Added eta-expansion in kernel, type inference and tactic unification,herbelin
governed in the latter case by a flag since (useful e.g. for setoid rewriting which otherwise loops as it is implemented). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13443 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-11Improving a few error messages in Ltac interpretationherbelin
- improving error message when a reference to unfold is not found - repairing anomaly when an evaluable reference exists at internalisation-time but not at run time, and similarly for an arbitrary term (but the latter is new from 8.3 because of the new use of retyping instead of understand for typing Ltac values) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13408 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-08-02Fix [clenv_missing] to compute a better approximation of missingmsozeau
dependent arguments. It breaks compatibility as some [apply with] clauses are not necessary anymore. Typically when applying [f_equal], the domain type of the function can be infered even if it does not appear directly in the conclusion of the goal. Fixes bug #2154. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13367 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-29kernel conversion and reduction do not raise assert failure on ill-typed ↵barras
terms, but an anomaly instead. It is caught in pretyping git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13353 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-29fixed bug #2105 (compilation of free de Bruijn) and missing lift of ↵barras
predicate in branch read-back (2) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13350 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-27Minor fixes:msozeau
- Document and fix [autounfold] - Fix warning about default Firstorder tactic object not being defined - Fix treatment of implicits in Program Lemma. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13334 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-24Updated all headers for 8.3 and trunkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-23Some fine-tuning after removal of automatic imports of coercions in r13310herbelin
- Moved Global Set from Keep to Substitute to ensure it is activated in real time and not only after the main parts of the module - Renamed Importation into Import in option name - Made "Print Libraries" prints the modules in the importation order (which is the most relevant order for non-commutative declarations) instead of load order git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13318 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-22Extension of the recursive notations mechanismherbelin
- Added support for recursive notations with binders - Added support for arbitrary large iterators in recursive notations - More checks on the use of variables and improved error messages - Do side-effects in metasyntax only when sure that everything is ok - Documentation Note: it seems there were a small bug in match_alist (instances obtained from matching the first copy of iterator were not propagated). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13316 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-22Made coercions active only when modules are imported.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13310 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-18Reverted 13293 commited mistakenly. Sorry for the noise.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13294 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-18Tentative de suppression de l'import automatique des hints et coercions.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13293 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-30Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13225 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-29Made tclABSTRACT normalize evars before saying it does not supportherbelin
them. This was the cause of the failure of compilation of CyclicAxioms after "replace" starting supporting open constrs (r13206). Seized the opportunity to clean a little bit things around nf_evar, whd_evar, check_evars, etc. Removed obsolete printer mod_self_id from dev/db. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13214 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-28Fixed a bug introduced in a combination in r12807 and revealed inherbelin
r13080 via a failure in CoRN (pattern_of_constr needs correct sigma). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13205 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-26Applying François' patches about Canonical Projections (see #2302 and #2334).herbelin
Printer pr_cs_pattern is kept in recordops only. Also updated CHANGES. Fixed spelling of "uniform inheritance condition" in doc too (see git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13204 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-25Restored a "feature" of unification in pre-8.3 (it was used e.g. in aherbelin
proof of Chung-Kil's Hur Heq package): conversion in "trivial_unify" accepted evars as ordinary variables. I hope I did not invalidate some features that would have needed restricting conversion on evar-free terms, but since failure of conversion in presence of evars is redirected to the main unification algorithm, I guess it is OK. For better readibility, I also inlined and cleaned a bit trivial_unify. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13193 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-22Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13179 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
Applied it to fix mli file headers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-18Hack for fixing bug #2172 (see explanations in file rewrite-2172.v).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13167 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-13Addressed bug #2310 and replaced anomaly "unknown meta" raised by "refine"herbelin
by a regular error in v8.3. Example behaves better in trunk thanks to new proof engine. In fact, there are two distinct solutions to a unification problem: should "refine" commit to one of them or leave the problem open? For trunk, improved the unification error message by enforcing nf_evar (but at some time, nf_evar in error messages should move to himsg because it is costly when errors are used for backtracking). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13127 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-12Fixed bug #2135 (second-order unification was raising cryptic message)herbelin
- made the example work (a call to whd_meta was missing) - replaced the internal error messages of w_unify_to_subterm_list into user-understandable messages - incidentally fixed the meaning of whd_meta (which now takes an evd) and meta_name (which now does what it means and do not treat differently the instantiated metas) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13122 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-12Improved the inference of the return predicate in dependent pattern-matching.herbelin
More precisely, the mecanism used to automatically infer return predicates of the form "as x in I y1..yn match y1..yn x with u1(z1)..un(zn) => P(z1..zn) | _ => ID end" now computes the dependencies in the types of y1..yn and x. This allows it to benefit of the generalisation mechanism of the pattern-matching compilation algorithm ("Abstract") and to infer more sophisticated return predicates (e.g. when working with "vector"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13118 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-12Added rudimentary support for using constructors from the explicitherbelin
substitution of evars when solving equation "?n[subst] = t": this is a quite common useful heuristic for inferring the return predicate of "match". Made incidentally a minor simplification of expand_full_opt. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13117 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-12Fixed a bug in evarutil.ml (wrong env of a postponed conversion problem).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13116 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-11Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).herbelin
Use two ways to solve it: - added a whd_betaiota in solve_simple_eqn (since evarconv itself refuses beta to preserve the opportunities of first-order-matching expressions of the form "(fun x => P) t"; an advantage of this whd_betaiota is also that it may simplify K-redexes. - also added a last-chance test in case of failing occur-check by trying to fully head-normalize (with delta) the right-hand-side (allows to solve for instance "?n = id ?n" where id is a constant (a bridled form of solve_refl that use fconv instead of evar_conv_x). Incidentally improved a bit the rendering of the type of generalized terms in pattern-matching by using whd_betaiota. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13113 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-11 17:30:10 +0000