diff options
Diffstat (limited to 'plugins/decl_mode/decl_interp.ml')
| -rw-r--r-- | plugins/decl_mode/decl_interp.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 5b1f15480..e387b31a5 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -138,7 +138,7 @@ let rec intern_bare_proof_instr globs = function | Pcast (id,typ) -> Pcast (id,intern_constr globs typ) -let rec intern_proof_instr globs instr= +let intern_proof_instr globs instr= {emph = instr.emph; instr = intern_bare_proof_instr globs instr.instr} @@ -467,7 +467,7 @@ let rec interp_bare_proof_instr info (sigma:Evd.evar_map) (env:Environ.env) = fu | Pcast (id,typ) -> Pcast(id,interp_constr true sigma env typ) -let rec interp_proof_instr info sigma env instr= +let interp_proof_instr info sigma env instr= {emph = instr.emph; instr = interp_bare_proof_instr info sigma env instr.instr} |