diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-26 14:24:54 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-26 14:24:54 +0100 |
| commit | 36c6e9508a42d00686e90441999481354152aaa3 (patch) | |
| tree | 882909be1c393764f13923e059448f3808fa0966 /tactics/eqschemes.ml | |
| parent | b58e8aa6525d45473f88fbea71bab88a2b46c825 (diff) | |
| parent | b1a5fe3686ecd5b03e5c7c2efd95716a8e5270ea (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'tactics/eqschemes.ml')
| -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 76bf13a57..64a68ba6b 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -177,7 +177,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 @@ -396,7 +396,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) @@ -486,7 +486,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, @@ -784,5 +784,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) |