diff options
Diffstat (limited to 'tactics/eqschemes.ml')
| -rw-r--r-- | tactics/eqschemes.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index b2603315..c9764af1 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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) |