aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2015-11-23 15:57:54 +0100
committerGravatar Matthieu Sozeau <mattam@mattam.org>2015-11-23 15:57:54 +0100
commit3e4a4fbb1e0f00aff08664321d916167166dbab3 (patch)
treee2a900c4136fb194bc088bcdc4ce563993e3e46f /tactics
parent6b3112d3b6e401a4c177447dd3651820897f711f (diff)
Fix generation of equality schemes on polymorphic equality types.
Diffstat (limited to 'tactics')
-rw-r--r--tactics/eqschemes.ml11
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)