Implementing the non-strict mode.

3 files changed, 21 insertions, 7 deletions

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