Hopefully the last word on having "simpl f" complying with the

semantics described in the reference manual (i.e. if "f" is a qualid,
do not add implicit arguments and, a fortiori, do not try to solve
these implicit arguments - in particular, changing DbLib which
expected this rule not to be followed).

2 files changed, 14 insertions, 14 deletions

diff --git a/CHANGES b/CHANGES
index e5b9987263..bf322f6895 100644
--- a/CHANGES
+++ b/CHANGES
@@ -156,8 +156,11 @@ Tactics
 - "change ... in ..." and "simpl ... in ..." now properly consider nested
   occurrences (possible source of incompatibilities since this alters
   the numbering of occurrences), but do not support nested occurrences.
-- simpl, vm_compute and native_compute can be given a notation string to a
-  constant as argument.
+- Tactics simpl, vm_compute and native_compute can be given a notation string
+  to a constant as argument.
+- When given a reference as argument, simpl, vm_compute and
+  native_compute now strictly interpret it as the head of a pattern
+  starting with this reference.
 - The "change p with c" tactic semantics changed, now type-checking 
   "c" at each matching occurrence "t" of the pattern "p", and 
   converting "t" with "c".
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 0a9182e0b9..5e40241487 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -346,18 +346,15 @@ let intern_typed_pattern ist p =
 
 let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
   match p with
-  | Inl r -> l,
-      (try Inl (intern_evaluable ist r)
-       with e when Logic.catchable_exception e ->
-         (* Compatibility. In practice, this means that the code above
-            is useless. Still the idea of having either an evaluable
-            ref or a pattern seems interesting, with "head" reduction
-            in case of an evaluable ref, and "strong" reduction in the
-            subterm matched when a pattern) *)
-         let r = match r with
-         | AN r -> r
-         | _ -> Qualid (loc_of_smart_reference r,qualid_of_path (path_of_global (smart_global r))) in
-         Inr (intern_typed_pattern ist (CRef(r,None))))
+  | Inl r ->
+      let loc = loc_of_smart_reference r in
+      let r = match r with
+      | AN r -> r
+      | _ -> Qualid (loc,qualid_of_path (path_of_global (smart_global r))) in
+      (* Ensure that no implicit arguments are added so that a qualid
+         is interpreted as the head of subterm starting with the
+         corresponding reference *)
+      l, Inr (intern_typed_pattern ist (CAppExpl(loc,(None,r,None),[])))
   | Inr c -> l, Inr (intern_typed_pattern ist c)
 
 (* This seems fairly hacky, but it's the first way I've found to get proper