diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/dune | 6 | ||||
| -rw-r--r-- | proofs/refine.ml | 18 |
2 files changed, 12 insertions, 12 deletions
diff --git a/proofs/dune b/proofs/dune new file mode 100644 index 0000000000..679c45f6bf --- /dev/null +++ b/proofs/dune @@ -0,0 +1,6 @@ +(library + (name proofs) + (synopsis "Coq's Higher-level Refinement Proof Engine and Top-level Proof Structure") + (public_name coq.proofs) + (wrapped false) + (libraries interp)) diff --git a/proofs/refine.ml b/proofs/refine.ml index b64e7a2e5e..198e057ebc 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -49,20 +49,14 @@ let (pr_constrv,pr_constr) = (* Get the side-effect's constant declarations to update the monad's * environmnent *) -let add_if_undefined kn cb env = - try ignore(Environ.lookup_constant kn env); env - with Not_found -> Environ.add_constant kn cb env +let add_if_undefined env eff = + let open Entries in + try ignore(Environ.lookup_constant eff.seff_constant env); env + with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env (* Add the side effects to the monad's environment, if not already done. *) -let add_side_effect env = function - | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } -> - add_if_undefined kn cb env - | { Entries.eff = Entries.SEscheme (l,_) } -> - List.fold_left (fun env (_,kn,cb,eff_env) -> - add_if_undefined kn cb env) env l - -let add_side_effects env effects = - List.fold_left (fun env eff -> add_side_effect env eff) env effects +let add_side_effects env eff = + List.fold_left add_if_undefined env eff let generic_refine ~typecheck f gl = let sigma = Proofview.Goal.sigma gl in |