diff options
| author | Pierre-Marie Pédrot | 2015-05-16 12:33:32 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-05-16 12:33:32 +0200 |
| commit | b14d88c8cd17ad524898b31c1772a0e8f70f19f8 (patch) | |
| tree | 64cf2c55d16871504b30fc8969ea1a0eda9f6fa7 /tactics | |
| parent | cd6e8689abff88f03872840d12f177d06fccda05 (diff) | |
Fixing bug #2814: "Anomaly: Uncaught exception Option.IsNone".
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2791d7c484..402a9e88a1 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3597,8 +3597,11 @@ let find_induction_type isrec elim hyp0 gl = if Option.is_empty scheme.indarg then error "Cannot find induction type"; let indsign = compute_scheme_signature scheme hyp0 ind_guess in let elim = ({elimindex = Some(-1); elimbody = elimc; elimrename = None},elimt) in - scheme, ElimUsing (elim,indsign) in - (Option.get scheme.indref,scheme.nparams, elim) + scheme, ElimUsing (elim,indsign) + in + match scheme.indref with + | None -> error_ind_scheme "" + | Some ref -> ref, scheme.nparams, elim let get_elim_signature elim hyp0 gl = compute_elim_signature (given_elim hyp0 elim gl) hyp0 |