From 364decf59c14ec8a672d3c4d46fa1939ea0e52d3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 16 Nov 2014 12:52:13 +0100
Subject: Enforcing a stronger difference between the two syntaxes "simpl
 reference" and "simpl pattern" in the code (maybe we should have merged them
 instead, but I finally decided to enforce their difference, even if some
 compatibility is to be preversed - the idea is that at some time "simpl
 reference" would only call a weak-head simpl (or eventually cbn), leading
 e.g. to reduce 2+n into S(1+n) rather than S(S(n)) which could be useful for
 better using induction hypotheses.

In the process we also implement the following:
- 'simpl "+"' is accepted to reduce all applicative subterms whose
  head symbol is written "+" (in the toplevel scope); idem for
  vm_compute and native_compute
- 'simpl reference' works even if reference has maximally inserted
  implicit arguments (this solves the "simpl fst" incompatibility)
- compatibility of ltac expressions referring to vm_compute and
  native_compute with functor application should now work (i.e.
  vm_compute and native_compute are now taken into account in
  tacsubst.ml)
- for compatibility, "simpl eq" (assuming no maximal implicit args in
  eq) or "simpl @eq" to mean "simpl (eq _ _)" are still allowed.

By the way, is "mul" on nat defined optimally? "3*n" simplifies to
"n+(n+(n+0))". Are there some advantages of this compared to have it
simplified to "n+n+n" (i.e. to "(n+n)+n").
---
 intf/genredexpr.mli | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'intf/genredexpr.mli')

diff --git a/intf/genredexpr.mli b/intf/genredexpr.mli
index 1096ecb1f8..a59278bb0e 100644
--- a/intf/genredexpr.mli
+++ b/intf/genredexpr.mli
@@ -32,7 +32,7 @@ type 'a glob_red_flag = {
 type ('a,'b,'c) red_expr_gen =
   | Red of bool
   | Hnf
-  | Simpl of 'c Locus.with_occurrences option
+  | Simpl of ('b,'c) Util.union Locus.with_occurrences option
   | Cbv of 'b glob_red_flag
   | Cbn of 'b glob_red_flag
   | Lazy of 'b glob_red_flag
@@ -40,8 +40,8 @@ type ('a,'b,'c) red_expr_gen =
   | Fold of 'a list
   | Pattern of 'a Locus.with_occurrences list
   | ExtraRedExpr of string
-  | CbvVm of 'c Locus.with_occurrences option
-  | CbvNative of 'c Locus.with_occurrences option
+  | CbvVm of ('b,'c) Util.union Locus.with_occurrences option
+  | CbvNative of ('b,'c) Util.union Locus.with_occurrences option
 
 type ('a,'b,'c) may_eval =
   | ConstrTerm of 'a
-- 
cgit v1.2.3