diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2015-11-23 15:57:54 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2015-11-23 15:57:54 +0100 |
| commit | 3e4a4fbb1e0f00aff08664321d916167166dbab3 (patch) | |
| tree | e2a900c4136fb194bc088bcdc4ce563993e3e46f /tactics | |
| parent | 6b3112d3b6e401a4c177447dd3651820897f711f (diff) | |
Fix generation of equality schemes on polymorphic equality types.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/eqschemes.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index b2603315d..d08c7615a 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -176,7 +176,7 @@ let build_sym_scheme env ind = name_context env ((Name varH,None,applied_ind)::realsign) in let ci = make_case_info (Global.env()) ind RegularStyle in let c = - (my_it_mkLambda_or_LetIn mib.mind_params_ctxt + (my_it_mkLambda_or_LetIn paramsctxt (my_it_mkLambda_or_LetIn_name realsign_ind (mkCase (ci, my_it_mkLambda_or_LetIn_name @@ -395,7 +395,7 @@ let build_l2r_rew_scheme dep env ind kind = applied_sym_C 3, [|mkVar varHC|]) in let c = - (my_it_mkLambda_or_LetIn mib.mind_params_ctxt + (my_it_mkLambda_or_LetIn paramsctxt (my_it_mkLambda_or_LetIn_name realsign (mkNamedLambda varP (my_it_mkProd_or_LetIn (if dep then realsign_ind_P else realsign_P) s) @@ -485,7 +485,7 @@ let build_l2r_forward_rew_scheme dep env ind kind = mkApp (mkVar varP,Array.append (rel_vect 3 nrealargs) (if dep then [|cstr (3*nrealargs+4) 3|] else [||])) in let c = - (my_it_mkLambda_or_LetIn mib.mind_params_ctxt + (my_it_mkLambda_or_LetIn paramsctxt (my_it_mkLambda_or_LetIn_name realsign (mkNamedLambda varH applied_ind (mkCase (ci, @@ -782,5 +782,6 @@ let build_congr env (eq,refl,ctx) ind = let congr_scheme_kind = declare_individual_scheme_object "_congr" (fun _ ind -> - (* May fail if equality is not defined *) - build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, Safe_typing.empty_private_constants) + (* May fail if equality is not defined *) + build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, + Safe_typing.empty_private_constants) |