Revision - 1aab7a8 - Quotient: use std def. of eqv relation

Revision 1aab7a846991d939e3a6f6b64f3f201333f08ecd authored by Pierre-Yves Strub on 05 April 2021, 06:42:55 UTC, committed by Pierre-Yves Strub on 05 April 2021, 06:42:55 UTC

Quotient: use std def. of eqv relation

1 parent 2a8554f

Files
Changes

Permalinks

ecCallbyValue.mli

(* -------------------------------------------------------------------- *)
open EcFol
open EcEnv
open EcReduction

(* -------------------------------------------------------------------- *)
val norm_cbv : reduction_info -> LDecl.hyps -> form -> form

Showing with 0 additions and 0 deletions (0 / 0 diffs computed)

Computing file changes ...