diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-06 19:01:45 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-06 19:18:45 +0200 |
| commit | cc7456862743e67d72f0875bc1511070e1658b7a (patch) | |
| tree | e01021b8cdb4084f49275b41e07cae91af369329 /plugins | |
| parent | 7afc8ec714a449c7ebef571f9846fccd3f97249b (diff) | |
Dead code.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 8647ca676..97989e268 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -832,7 +832,7 @@ let build_per_info etype casee gls = let ctyp=pf_type_of gls casee in let is_dep = dependent casee concl in let hd,args = decompose_app (special_whd gls ctyp) in - let (ind,u as indu) = + let (ind,u) = try destInd hd with DestKO -> |