diff options
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/decl_interp.ml | 4 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 6 |
2 files changed, 5 insertions, 5 deletions
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 5b1f154808..e387b31a58 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} diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index b7c5174562..4fc5862c14 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1140,10 +1140,10 @@ let case_tac params pat_info hyps gls0 = (* end cases *) -type instance_stack = - (constr option*(constr list) list) list +type ('a, 'b) instance_stack = + ('b * (('a option * constr list) list)) list -let initial_instance_stack ids = +let initial_instance_stack ids : (_, _) instance_stack = List.map (fun id -> id,[None,[]]) ids let push_one_arg arg = function |