diff options
| -rw-r--r-- | tactics/decl_interp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml index 0a984cceb9..f341580eb1 100644 --- a/tactics/decl_interp.ml +++ b/tactics/decl_interp.ml @@ -204,7 +204,7 @@ let rawconstr_of_hyps inject hyps head = let raw_prop = RSort (dummy_loc,RProp Null) let rec match_hyps blend names constr = function - [] -> [],constr + [] -> [],substl names constr | hyp::q -> let (name,typ,body)=destProd constr in let st= {st_label=name;st_it=substl names typ} in |