diff options
| author | Matthieu Sozeau | 2014-08-14 13:01:30 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-08-14 13:01:30 +0200 |
| commit | 37a58edffeff7b6a7f03ec781e1e2ca73de4b3af (patch) | |
| tree | e7c73845d8ccc700662875c5455d9a797225da87 | |
| parent | 9c1e76422c63ab845d72893ca85dd38ce5ce9bec (diff) | |
Restrict eta-conversion to inductive records, fixing bug #3310.
| -rw-r--r-- | kernel/closure.ml | 3 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 22 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3310.v (renamed from test-suite/bugs/opened/3310.v) | 0 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3482.v | 11 |
4 files changed, 24 insertions, 12 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 62ee5db5d5..6dacb7818c 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -866,7 +866,8 @@ let rec get_parameters depth n argstk = let eta_expand_ind_stacks env ind m s (f, s') = let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with - | Some (exp,projs) when Array.length projs > 0 -> + | Some (exp,projs) when Array.length projs > 0 + && mib.Declarations.mind_finite -> let primitive = Environ.is_projection projs.(0) env in if primitive then (* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') -> diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index ed04c71503..68dfb1a1bd 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -745,21 +745,21 @@ and conv_record trs env evd (ctx,(h,h'),c,bs,(params,params1),(us,us2),(ts,ts1), and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with - | Some (exp,projs) when Array.length projs > 0 -> + | Some (exp,projs) when Array.length projs > 0 + && mib.Declarations.mind_finite -> let pars = mib.Declarations.mind_nparams in (try let l1' = Stack.tail pars sk1 in - if Environ.is_projection projs.(0) env then - let l2' = - let term = Stack.zip (term2,sk2) in - List.map (fun p -> mkProj (p, term)) (Array.to_list projs) - in - exact_ise_stack2 env evd (evar_conv_x ts) l1' - (Stack.append_app_list l2' Stack.empty) - else raise (Failure "") + let l2' = + let term = Stack.zip (term2,sk2) in + List.map (fun p -> mkProj (p, term)) (Array.to_list projs) + in + exact_ise_stack2 env evd (evar_conv_x ts) l1' + (Stack.append_app_list l2' Stack.empty) with - | Invalid_argument _ (* Stack.tail: partially applied constructor *) - | Failure _ -> UnifFailure(evd,NotSameHead)) + | Invalid_argument _ -> + (* Stack.tail: partially applied constructor *) + UnifFailure(evd,NotSameHead)) | _ -> UnifFailure (evd,NotSameHead) (* Profiling *) diff --git a/test-suite/bugs/opened/3310.v b/test-suite/bugs/closed/3310.v index ee9f8edfd3..ee9f8edfd3 100644 --- a/test-suite/bugs/opened/3310.v +++ b/test-suite/bugs/closed/3310.v diff --git a/test-suite/bugs/closed/3482.v b/test-suite/bugs/closed/3482.v new file mode 100644 index 0000000000..34a5e73da7 --- /dev/null +++ b/test-suite/bugs/closed/3482.v @@ -0,0 +1,11 @@ +Set Primitive Projections. +Class Foo (F : False) := { foo : True }. +Arguments foo F {Foo}. +Print Implicit foo. (* foo : forall F : False, Foo F -> True + +Argument Foo is implicit and maximally inserted *) +Check foo _. (* Toplevel input, characters 6-11: +Error: Illegal application (Non-functional construction): +The expression "foo" of type "True" +cannot be applied to the term + "?36" : "?35" *)
\ No newline at end of file |