diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 6 | ||||
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 1 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 6 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 26 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 3 |
5 files changed, 22 insertions, 20 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 5bf772fc5a..a3bb2eee96 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -397,9 +397,9 @@ let isLetIn t = let h_reduce_with_zeta = h_reduce - (Glob_term.Cbv - {Glob_term.all_flags - with Glob_term.rDelta = false; + (Genredexpr.Cbv + {Redops.all_flags + with Genredexpr.rDelta = false; }) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index f18309d049..ccf2caaf56 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -3,6 +3,7 @@ open Pp open Names open Term open Glob_term +open Glob_ops open Libnames open Indfun_common open Errors diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 96bde6f1ba..1c2509f6e2 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -104,9 +104,9 @@ let functional_induction with_clean c princl pat = (Tacmach.pf_ids_of_hyps g) in let flag = - Glob_term.Cbv - {Glob_term.all_flags - with Glob_term.rDelta = false; + Genredexpr.Cbv + {Redops.all_flags + with Genredexpr.rDelta = false; } in Tacticals.tclTHEN diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 667be89d09..4d072eca56 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -415,10 +415,10 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem (* observe_tac "unfolding" pre_tac; *) (* $zeta$ normalizing of the conclusion *) h_reduce - (Glob_term.Cbv - { Glob_term.all_flags with - Glob_term.rDelta = false ; - Glob_term.rConst = [] + (Genredexpr.Cbv + { Redops.all_flags with + Genredexpr.rDelta = false ; + Genredexpr.rConst = [] } ) Locusops.onConcl; @@ -804,9 +804,9 @@ and intros_with_rewrite_aux : tactic = | LetIn _ -> tclTHENSEQ[ h_reduce - (Glob_term.Cbv - {Glob_term.all_flags - with Glob_term.rDelta = false; + (Genredexpr.Cbv + {Redops.all_flags + with Genredexpr.rDelta = false; }) Locusops.onConcl ; @@ -819,9 +819,9 @@ and intros_with_rewrite_aux : tactic = | LetIn _ -> tclTHENSEQ[ h_reduce - (Glob_term.Cbv - {Glob_term.all_flags - with Glob_term.rDelta = false; + (Genredexpr.Cbv + {Redops.all_flags + with Genredexpr.rDelta = false; }) Locusops.onConcl ; @@ -958,9 +958,9 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = Equality.rewriteLR (mkConst eq_lemma); (* Don't forget to $\zeta$ normlize the term since the principles have been $\zeta$-normalized *) h_reduce - (Glob_term.Cbv - {Glob_term.all_flags - with Glob_term.rDelta = false; + (Genredexpr.Cbv + {Redops.all_flags + with Genredexpr.rDelta = false; }) Locusops.onConcl ; diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index d11909043f..0b61c5f858 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -39,12 +39,13 @@ open Pretyping open Safe_typing open Constrintern open Hiddentac +open Misctypes +open Genredexpr open Equality open Auto open Eauto -open Misctypes open Indfun_common |