diff options
Diffstat (limited to 'proofs/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 1b329dbc4..22262036e 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -36,8 +36,8 @@ let start_proof (id : Id.t) str hyps c ?init_tac terminator = let cook_this_proof p = match p with - | { Proof_global.id;entries=[constr];persistence;constraints } -> - (id,(constr,constraints,persistence)) + | { Proof_global.id;entries=[constr];persistence;universes } -> + (id,(constr,universes,persistence)) | _ -> Errors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.") let cook_proof () = |