Implementing the non-strict mode.

5 files changed, 46 insertions, 10 deletions

diff --git a/doc/ltac2.md b/doc/ltac2.md
index c1216d8f89..d7c8719a14 100644
--- a/doc/ltac2.md
+++ b/doc/ltac2.md
@@ -440,6 +440,8 @@ TERM ::=
 QUOTNAME := IDENT
 ```
 
+### Built-in quotations
+
 The current implementation recognizes the following built-in quotations:
 - "ident", which parses identifiers (type `Init.ident`).
 - "constr", which parses Coq terms and produces an-evar free term at runtime
@@ -457,6 +459,28 @@ The following syntactic sugar is provided for two common cases.
 - `@id` is the same as ident:(id)
 - `'t` is the same as open_constr:(t)
 
+### Strict vs. non-strict mode
+
+Depending on the context, quotations producing terms (i.e. `constr` or
+`open_constr`) are not internalized in the same way. There are two possible
+modes, respectively called the *strict* and the *non-strict* mode.
+
+- In strict mode, all simple identifiers appearing in a term quotation are
+required to be resolvable statically. That is, they must be the short name of
+a declaration which is defined globally, excluding section variables and
+hypotheses. If this doesn't hold, internalization will fail. To work around
+this error, one has to specifically use the `&` notation.
+- In non-strict mode, any simple identifier appearing in a term quotation which
+is not bound in the global context is turned into a dynamic reference to a
+hypothesis. That is to say, internalization will succeed, but the evaluation
+of the term at runtime will fail if there is no such variable in the dynamic
+context.
+
+Strict mode is enforced by default, e.g. for all Ltac2 definitions. Non-strict
+mode is only set when evaluating Ltac2 snippets in interactive proof mode. The
+rationale is that it is cumbersome to explicitly add `&` interactively, while it
+is expected that global tactics enforce more invariants on their code.
+
 ## Term Antiquotations
 
 ### Syntax
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 197ec19b3a..7a900e8bf0 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -325,7 +325,7 @@ let register_ltac ?(local = false) ?(mut = false) isrec tactics =
     if isrec then inline_rec_tactic tactics else tactics
   in
   let map ((loc, id), e) =
-    let (e, t) = intern e in
+    let (e, t) = intern ~strict:true e in
     let () =
       if not (is_value e) then
         user_err ?loc (str "Tactic definition must be a syntactical value")
@@ -717,7 +717,7 @@ let register_redefinition ?(local = false) (loc, qid) e =
     if not (data.Tac2env.gdata_mutable) then
       user_err ?loc (str "The tactic " ++ pr_qualid qid ++ str " is not declared as mutable")
   in
-  let (e, t) = intern e in
+  let (e, t) = intern ~strict:true e in
   let () =
     if not (is_value e) then
       user_err ?loc (str "Tactic definition must be a syntactical value")
@@ -826,7 +826,7 @@ let solve default tac =
 
 let call ~default e =
   let loc = loc_of_tacexpr e in
-  let (e, t) = intern e in
+  let (e, t) = intern ~strict:false e in
   let () = check_unit ?loc t in
   let tac = Tac2interp.interp Tac2interp.empty_environment e in
   solve default (Proofview.tclIGNORE tac)
diff --git a/src/tac2intern.ml b/src/tac2intern.ml
index 1dba57c4c1..d1a3e13cdb 100644
--- a/src/tac2intern.ml
+++ b/src/tac2intern.ml
@@ -131,6 +131,8 @@ type environment = {
   (** Accept unbound type variables *)
   env_rec : (KerName.t * int) Id.Map.t;
   (** Recursive type definitions *)
+  env_str : bool;
+  (** True iff in strict mode *)
 }
 
 let empty_env () = {
@@ -139,6 +141,7 @@ let empty_env () = {
   env_als = ref Id.Map.empty;
   env_opn = true;
   env_rec = Id.Map.empty;
+  env_str = true;
 }
 
 let env_name env =
@@ -780,7 +783,13 @@ let rec intern_rec env (loc, e) = match e with
   let genv = Global.env_of_context Environ.empty_named_context_val in
   let ist = empty_glob_sign genv in
   let ist = { ist with extra = Store.set ist.extra ltac2_env env } in
-  let arg, tpe = Flags.with_option Ltac_plugin.Tacintern.strict_check (fun () -> obj.ml_intern self ist arg) () in
+  let arg, tpe =
+    if env.env_str then
+      let arg () = obj.ml_intern self ist arg in
+      Flags.with_option Ltac_plugin.Tacintern.strict_check arg ()
+    else
+      obj.ml_intern self ist arg
+  in
   let e = match arg with
   | GlbVal arg -> GTacExt (tag, arg)
   | GlbTacexpr e -> e
@@ -1121,8 +1130,9 @@ let normalize env (count, vars) (t : UF.elt glb_typexpr) =
   in
   subst_type subst t
 
-let intern e =
+let intern ~strict e =
   let env = empty_env () in
+  let env = if strict then env else { env with env_str = false } in
   let (e, t) = intern_rec env e in
   let count = ref 0 in
   let vars = ref UF.Map.empty in
@@ -1487,7 +1497,11 @@ let () =
   let open Genintern in
   let intern ist tac =
     let env = match Genintern.Store.get ist.extra ltac2_env with
-    | None -> empty_env ()
+    | None ->
+      (** Only happens when Ltac2 is called from a constr or ltac1 quotation *)
+      let env = empty_env () in
+      if !Ltac_plugin.Tacintern.strict_check then env
+      else { env with env_str = false }
     | Some env -> env
     in
     let loc = loc_of_tacexpr tac in
diff --git a/src/tac2intern.mli b/src/tac2intern.mli
index 045e657460..4b02f91caa 100644
--- a/src/tac2intern.mli
+++ b/src/tac2intern.mli
@@ -13,7 +13,7 @@ open Tac2expr
 val loc_of_tacexpr : raw_tacexpr -> Loc.t option
 val loc_of_patexpr : raw_patexpr -> Loc.t option
 
-val intern : raw_tacexpr -> glb_tacexpr * type_scheme
+val intern : strict:bool -> raw_tacexpr -> glb_tacexpr * type_scheme
 val intern_typedef : (KerName.t * int) Id.Map.t -> raw_quant_typedef -> glb_quant_typedef
 val intern_open_type : raw_typexpr -> type_scheme
 
diff --git a/tests/compat.v b/tests/compat.v
index f4e849c5de..489fa638e4 100644
--- a/tests/compat.v
+++ b/tests/compat.v
@@ -18,8 +18,7 @@ Qed.
 
 Goal true = false -> false = true.
 Proof.
-(** FIXME when the non-strict mode is implemented. *)
-Fail intros H; ltac1:(rewrite H); reflexivity.
+intros H; ltac1:(rewrite H); reflexivity.
 Abort.
 
 (** Variables do not cross the compatibility layer boundary. *)
@@ -57,4 +56,3 @@ Fail mytac ltac2:(fail).
 let t := idtac; ltac2:(fail) in mytac t.
 constructor.
 Qed.
-