diff options
| author | Hugo Herbelin | 2014-10-26 14:23:00 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-26 15:26:22 +0100 |
| commit | 29a5127dac6d4fbc317e38452cf0fe05916adc56 (patch) | |
| tree | adabfae9b7e860ef3e6aacb4b9f9f3871c6a71dc /pretyping | |
| parent | 1be28ac589a6affa81b905bbf223bdf520511a44 (diff) | |
Fixing destruct/induction with a using clause on a non-inductive type,
that was broken by commit bf01856940 + use types from induction scheme
to restrict selection of pattern + accept matching from partially
applied term when using "using".
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/unification.ml | 16 | ||||
| -rw-r--r-- | pretyping/unification.mli | 4 |
2 files changed, 9 insertions, 11 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 65d08609fb..8b14feca04 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1410,7 +1410,7 @@ let default_matching_flags (sigma,_) = exception PatternNotFound -let make_pattern_test from_prefix_of_ind env sigma (pending,c) = +let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = let flags = default_matching_flags pending in let n = List.length (snd (decompose_app c)) in let matching_fun _ t = @@ -1427,12 +1427,8 @@ let make_pattern_test from_prefix_of_ind env sigma (pending,c) = applist (t,l1) else t in let sigma = w_typed_unify env sigma Reduction.CONV flags c t' in - let _ = - if from_prefix_of_ind then - (* We check that the subterm we found from prefix is applied *) - (* enough to be of inductive type *) - try ignore (Inductiveops.find_mrectype env sigma (Retyping.get_type_of env sigma t)) - with UserError _ -> raise (NotUnifiable None) in + let ty = Retyping.get_type_of env sigma t in + if not (is_correct_type ty) then raise (NotUnifiable None); Some(sigma, t) with | PretypeError (_,_,CannotUnify (c1,c2,Some e)) -> @@ -1526,7 +1522,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = type prefix_of_inductive_support_flag = bool type abstraction_request = -| AbstractPattern of prefix_of_inductive_support_flag * Name.t * pending_constr * clause or_like_first * bool +| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Name.t * pending_constr * clause or_like_first * bool | AbstractExact of Name.t * constr * types option * clause * bool type abstraction_result = @@ -1536,9 +1532,9 @@ type abstraction_result = let make_abstraction env evd ccl abs = match abs with - | AbstractPattern (from_prefix,name,c,occs,check_occs) -> + | AbstractPattern (from_prefix,check,name,c,occs,check_occs) -> make_abstraction_core name - (make_pattern_test from_prefix env evd c) + (make_pattern_test from_prefix check env evd c) env evd (snd c) None occs check_occs ccl | AbstractExact (name,c,ty,occs,check_occs) -> make_abstraction_core name diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 3b49981290..7f5cac2d23 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -65,8 +65,10 @@ val w_coerce_to_type : env -> evar_map -> constr -> types -> types -> exception PatternNotFound +type prefix_of_inductive_support_flag = bool + type abstraction_request = -| AbstractPattern of bool * Names.Name.t * pending_constr * Locus.clause Locus.or_like_first * bool +| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Names.Name.t * pending_constr * Locus.clause Locus.or_like_first * bool | AbstractExact of Names.Name.t * constr * types option * Locus.clause * bool val finish_evar_resolution : ?flags:Pretyping.inference_flags -> |