aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Collapse)AuthorAge
* Esubst: make types of substitutions & lifts privateGravatar puech2011-08-08
| | | | | | | 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
* Fix unification: detect invalid evar instantiations due to scoping earlier.Gravatar msozeau2011-08-04
| | | | | | 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
* Fix nf_evars_undefinedGravatar msozeau2011-08-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14382 85f007b7-540e-0410-9357-904b9bb8a0f7
* Patch to simplify is_open_canonical_projectionGravatar herbelin2011-08-02
| | | | | | (courtesy from François Garillot) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14381 85f007b7-540e-0410-9357-904b9bb8a0f7
* More robust evar_map debugging printerGravatar herbelin2011-08-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14380 85f007b7-540e-0410-9357-904b9bb8a0f7
* Evarutil: replace generic list_distinct on constr by constr_list_distinctGravatar puech2011-07-29
| | | | | | 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
* Evarutil: replaced some generic = on constr by destructorsGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14352 85f007b7-540e-0410-9357-904b9bb8a0f7
* Evarutil: generic equality on constr replaced by destructorsGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14332 85f007b7-540e-0410-9357-904b9bb8a0f7
* Evarconv: generic equality on constr replaced by eq_constrGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14329 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cases: generic equality on constr replaced by destructorsGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14327 85f007b7-540e-0410-9357-904b9bb8a0f7
* Classops: generic equality on constr replaced by eq_constrGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14325 85f007b7-540e-0410-9357-904b9bb8a0f7
* Evarutil: generic equality on constr replaced by eq_constr (x2)Gravatar puech2011-07-29
| | | | | | added array_equal in Util git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Evarutil: generic equality on constr replaced by eq_constrGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14318 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tacred: generic equality on constr replaced by eq_constrGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14317 85f007b7-540e-0410-9357-904b9bb8a0f7
* This is exactly the structure needed to handle controlling printingGravatar herbelin2011-07-16
| | | | | | | | of terms of record type with record or constructor syntax. Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14285 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: forbid Prop-polymorphism of inductives when extracting to OcamlGravatar letouzey2011-07-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | A particular case in sort-polymorphism of inductive types allows an informative type (such as prod) to have instances in Prop: (I,I) : True * True : Prop This is due to the fact that prod is a singleton type: indeed (I,I) has no informative content. But this invalidates an important invariant for the correctness of the extraction: inductive constructors stop having always the same sort as their inductive type. Consider for instance: Definition f (X:Type)(x:X*X)(g:X->nat) := g (fst x). Definition test := f _ (I,I) (fun _ => 0). Then the inductive element (I,I) is extracted as a logical part __, but during a strict evaluation (i.e. in Ocaml, not Haskell), this __ will be given to fst, and hence to a match, leading to a nasty result (potentially segfault). Haskell is not affected, since fst is never evaluated. This patch adds a check for this situation during any Ocaml extraction, leading for the moment to a fatal error. Some functions in inductive.ml and retyping.ml now have an extra optional argument ?(polyprop=true) that should stay untouched in regular Coq usage, while type-checking done during extraction will disable this prop-polymorphism. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14256 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning debugging printer relative to new proof engine. InGravatar herbelin2011-06-21
| | | | | | | | | particular, new printer for evar_map which displays undefined evars + defined evars that were instantiated by these undefined evars and recursively, up to some arbitrary level n chosen to be in practice n=2 (thanks to Arnaud). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14231 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing two typos introduced in r14217 and r14223Gravatar herbelin2011-06-20
| | | | | | | | (due to unreverted debugging stuff): - wrong revert of betaiota flag to false in r14223 - wrong exception raised in r14217 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14224 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ensured that the transparency state is used when flag betaiota is on for apply.Gravatar herbelin2011-06-19
| | | | | | | + small typo fix in r14217 + added compatibility of betaiota flag with 8.3 when "-compat 8.3" is given git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14223 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generalizing flag use_evars_pattern_unification into a flagGravatar herbelin2011-06-18
| | | | | | | | | | use_pattern_unification common for evars and metas. As a compensation, add a flag use_meta_bound_pattern_unification to restore the old mechanism of pattern unification for metas applied to rels only (this is used e.g. by auto). Not sure yet, what could be the most appropriate set of flags. Added documentation of the flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14221 85f007b7-540e-0410-9357-904b9bb8a0f7
* Activating flags betaiota by default for applyGravatar herbelin2011-06-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14220 85f007b7-540e-0410-9357-904b9bb8a0f7
* The ad hoc version for first-order unification at toplevel of "?n argsGravatar herbelin2011-06-18
| | | | | | | | | | | = t" introduced in r14199 (w_typed_unify_list) tried to check types of metas more than what w_typed_unify used to before (and these types need delta to be convertible). Don't know if it is a weakness of the test for checking types but since checking types should not be necessary here, w_typed_unify_list now follows what w_unify_core_0 does more closely. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14217 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added full pattern-unification on Meta for tactic unification.Gravatar herbelin2011-06-13
| | | | | | | No way to control it yet; maybe flag use_evars_pattern_unification should be generalized for that purpose. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14199 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a flag to restrict conversion in tactic unification on theGravatar herbelin2011-06-13
| | | | | | | | | strict subterms of the initial unification problem (inspired from ssreflect rewriting strategy). Not activated however (a few applications of setoid rewrite use this possibility on closed terms in the stdlib, e.g. "flip le p (min n m)" identified with "le (min n m) p"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14198 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oups, typo in previous commitGravatar herbelin2011-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14192 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed what looks like a (very old) useless f.o. unification passGravatar herbelin2011-06-12
| | | | | | made after s.o. unification succeeds. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14191 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a new flag for freezing evars in tactic unification. Used thisGravatar herbelin2011-06-12
| | | | | | | | | | | | | | | | flag to forbid rewriting tactics to instantiate an evar of the goal while looking for subterms (this is not clear that we always want that for rewrite but we certainly want it for autorewrite; see comments by Charguéraud on coqdev Oct 2010). In a few cases in the theories, a pre-existing evar of an hyp used for rewriting is instantiated by the rewriting step. Let's accept this at the current time. We have to make progress towards documenting and stabilizing the strategy for matching/unifying subterms in rewrite/induction/set... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14190 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved allow_K to a unification flagGravatar herbelin2011-06-10
| | | | | | | | - seized the opportunity to align unification flags for functional induction to the ones of induction - also tried to add delta in the elim_flags used in tactics.ml - also tried to unify the rewrite flags in concl or in hyp (removed allow_K in hyps) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14186 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes in pruning, do not fail if pruning is impossible due to typing ↵Gravatar msozeau2011-06-10
| | | | | | constraints but postpone evar-evar problems git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14176 85f007b7-540e-0410-9357-904b9bb8a0f7
* More fixes in pruning/restriction of evars during unification.Gravatar msozeau2011-06-09
| | | | | | | | - Do not allow to filter variables that appear in the conclusion of an evar. - Do not attempt to restrict evars based on a substitution that does not contain only evars (fall back to the pattern fragment and do not lose solutions). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14174 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes in pruning in unification.Gravatar msozeau2011-06-08
| | | | | | | | | Properly normalize evars to reflect the already pruned evars in the type of dependent evars to allow more precise restriction of hyps. Directly check the type of an evar instance, allowing backtracking on ill-typed instanciations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14169 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fix restrict_hyps to not allow filtering on a variable required to ↵Gravatar msozeau2011-06-07
| | | | | | | | | typecheck the evar's conclusion - Prevent extend_evar from creating ill-formed evars with de Bruijn-open conclusions. - Minor fix of define_evars_as_lambda, another mixup of named and de Bruijn indices. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14163 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applying Enrico Tassi's patch for giving priority to delta over eta inGravatar herbelin2011-05-24
| | | | | | | unification (evarconv.ml). Works better for compiling math. comp. library while seems ok on other examples. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14153 85f007b7-540e-0410-9357-904b9bb8a0f7
* Failing instead of switching to the coercion mechanism when VMcastGravatar herbelin2011-05-15
| | | | | | involves evars (seem cleaner) at type-inference time. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14123 85f007b7-540e-0410-9357-904b9bb8a0f7
* A better procedure for checking presence of undefined evars.Gravatar aspiwack2011-05-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14121 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix merge, Cumul moved to CUMULGravatar msozeau2011-05-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14093 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge branch 'subclasses' into coq-trunkGravatar msozeau2011-05-05
| | | | | | | | | Stop using hnf_constr in unify_type, which might unfold constants that are marked opaque for unification. Conflicts: pretyping/unification.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14092 85f007b7-540e-0410-9357-904b9bb8a0f7
* First phase removing obsolete support for eta up to conversion inGravatar herbelin2011-05-04
| | | | | | | | | | "apply" unification. Assuming w_unify_0 is not eventually abandoned, it remains to merge unify_with_eta into unify_0 (what unify_with_eta does and that unify_0 does not do is to select of two instances of the same meta the one with less lambda's; it is unclear whether this is useful heuristic). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14091 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug in printing let-in binders in fix/cofixGravatar herbelin2011-04-24
| | | | | | (backport from branch v8.3) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14055 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allow betaiota when checking unification of the types of metas (fixes ATBR ↵Gravatar msozeau2011-04-20
| | | | | | contrib). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14032 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a flag to control betaiota reduction during unification to maintain ↵Gravatar msozeau2011-04-18
| | | | | | backward compatibility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14022 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix unification of types of metavariables and error message for sort ↵Gravatar msozeau2011-04-16
| | | | | | unification. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14020 85f007b7-540e-0410-9357-904b9bb8a0f7
* Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".Gravatar herbelin2011-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14018 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Make typeclass transparency information directly availableGravatar msozeau2011-04-13
| | | | | | | - Fix pretyping to consider remaining unif problems with the right transparency information. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13996 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Remove create_evar_defsGravatar msozeau2011-04-13
| | | | | | - Be careful with consider_remaining_unif_problems: it might instantiate an evar, including the current goal! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13995 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Improve unification (beta-reduction, and same heuristic as evarconv for ↵Gravatar msozeau2011-04-13
| | | | | | reducing matches). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13993 85f007b7-540e-0410-9357-904b9bb8a0f7
* Unify meta types with the right flags, add betaiotazeta reduction to ↵Gravatar msozeau2011-04-13
| | | | | | unification (potentially harmful) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13991 85f007b7-540e-0410-9357-904b9bb8a0f7
* Proper typing of metavariables, type errors were completely ignored ↵Gravatar msozeau2011-04-13
| | | | | | before... Use sort constraint checking as in evarconv as well git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13990 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Do not make constants with an assigned type polymorphic (wrong unfoldings).Gravatar msozeau2011-04-13
| | | | | | - Add Set Typeclasses Debug/Depth n options for typeclasses eauto. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13989 85f007b7-540e-0410-9357-904b9bb8a0f7
* Catch NotArity exception and transform it into an anomaly in retyping.Gravatar msozeau2011-04-11
| | | | | | | | | | Add a temporary fix in solve_simple_eqn to catch anomalies coming from retyping because the unification algorithm with metas doesn't respect the precondition that evar instances should be well-typed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13985 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 22:08:47 +0000