diff options
| author | Pierre-Marie Pédrot | 2016-11-20 20:09:26 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:30:34 +0100 |
| commit | d4b344acb23f19b089098b7788f37ea22bc07b81 (patch) | |
| tree | 6dd26d747b259793ef6a24befd27e13234b19875 /plugins/decl_mode | |
| parent | 2cd0648e003308a000f9f89c898bce4d15fc94a1 (diff) | |
Eliminating parts of the right-hand side compatibility layer
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 5de2c41517..e73166be28 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -786,7 +786,7 @@ let rec consider_match may_intro introduced available expected gls = let consider_tac c hyps gls = let c = EConstr.of_constr c in - match kind_of_term (strip_outer_cast (project gls) c) with + match EConstr.kind (project gls) (strip_outer_cast (project gls) c) with Var id -> consider_match false [] [id] hyps gls | _ -> @@ -811,6 +811,9 @@ let rec take_tac wits gls = (* tactics for define *) +let subst_term sigma c t = + EConstr.Unsafe.to_constr (subst_term sigma c t) + let rec build_function sigma args body = match args with st::rest -> |