evarconv: MaybeFlex/MaybeFlex case infers more Canonical Structures

Canonical Structure inference works on named terms only: i.e.
the projection and the value must be named (with few exceptions).

The set of named (head) terms is:
  (Var _|Construct _|Ind _|Const _|Prod _|Sort _)

The set of unnamed is thus:
  (Case _|Fix _|CoFix _|Evar _|Meta _|Rel _)

The MaybeFlex/MaybeFlex case, when no CS inference takes place,
unfolds the rhs only if it exposes a named term. If it exposes
an unnamed term, it tries to unfold on the lhs first. Note that
unnamed terms are whd normal terms, since iota and zeta are
performed by evar_apprec. So the algorithm behaves as before,
but stops unfolding the rhs 1 delta step before it exposes an
unnamed term. Then it starts unfolding the lhs. If the lhs
exposes a rigid term the rhs is naturally unfolded, going back
to same situation in which the algorithm was ending before.
But while it unfolds on the left, the rhs is still named, and
canonical structure inference can succeed.

Ex failing before, the "canon_" prefix marks projections/values
declared as canonical.

  Record test := K { canon_proj : nat }
  (* canon_proj x := math x with K y => y end *)
  canon_val x := match x with 0 => 0 | S m => m end
  Canonical Structure canon_struct x := K (canon_val x)
  (* aliases *)
  proj := canon_proj
  val := canon_val

Old alg:

  proj ?       ===?===       val x
  proj ?       ===?=== canon_val x
  proj ?       ===?=== match x with ... end
  canon_proj ? ===?=== match x with ... end   (* no inference *)
  match ? with K x...end ===?=== match x with 0 ...end (* FAIL *)

New alg:

  proj ?       ===?===       val x
  proj ?       ===?=== canon_val x
  canon_proj ? ===?=== canon_val x (* inference works: ? := canon_struct *)

In case canon_struct is not declared for canon_proj and canon_val
it continues like that:

  canon_proj ? ===?=== canon_val x
  match ? with K x...end ===?=== canon_val x
  match ? with K x...end ===?=== match x with 0 ...end (* FAIL *)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15078 85f007b7-540e-0410-9357-904b9bb8a0f7
Merge bug fixes: r14892, 14922, 14923, 14940-14943, 14948, 14964, 14978-14985, 14988, 14991.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15091 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Fixing deactivation of scope at printing time in the body of a
lam or prod to be consistent with what is done at parsing time
(see coq-club on 25/3/2012).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15094 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Fixing printing level of Utf8 equivalent for ->.
Parsing with rhs at level 200 was already working thanks to I don't
which unexpected magic from camlp4/5.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15097 85f007b7-540e-0410-9357-904b9bb8a0f7
Removed a superfluous function in proof.mli. Preparing for incoming
changes of the handling of unfocusing errors.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15106 85f007b7-540e-0410-9357-904b9bb8a0f7
Corrects the erroneous error message when trying to unfocus a fully
unfocused proof (part of bug #2671).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15107 85f007b7-540e-0410-9357-904b9bb8a0f7
Arranged for the desirable behaviour that bullets do not see beyond braces.
i.e.: after a brace is open, one can use the bullets again without clashing with
bullets outside the brace. In particular, one can nest bullets with  arbitrary
depth (by interleaving them with occasional braces).

Also fixed a typo introduced in my previous commit which caused bullets
and braces to behave just like regular focuses.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15108 85f007b7-540e-0410-9357-904b9bb8a0f7
Added a command "Unfocused" which returns an error when the proof is
not fully unfocused (in the style of the Guarded command).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15109 85f007b7-540e-0410-9357-904b9bb8a0f7
Typo in a message.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15110 85f007b7-540e-0410-9357-904b9bb8a0f7
Backport fixes on typeclasses and interface of pretyping:
- Deal with unresolvable/resolvable cleanly at calls to resolution.
- Consider all holes of typeclasses to be resolvable except for GoalEvars
which have special status.
- understand_ltac is parameterized by a resolve_classes flag. Used
to launch typeclass resolution when interpreting _casted_ open constrs
exclusively.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15111 85f007b7-540e-0410-9357-904b9bb8a0f7
Introduce notations to ensure compatibility for 8.3 symbols ZOdiv and ZOmod,
which have been replaced by Zquot and Zrem in 8.4. This makes it possible for
the user to write Coq scripts in a way that works with both 8.3 and 8.4.
(Tested on the Flocq library r448.)

Note that this patch should not be ported to trunk, as the goal is to ease the
transition from 8.3 to 8.4, not from 8.3 to 8.5. In other words, ZOdiv and ZOmod
are definitions in 8.3, backward-compatible notations in 8.4, and removed in
8.5, since users will have switched to the new names by the time 8.5 is
released.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15112 85f007b7-540e-0410-9357-904b9bb8a0f7
Speedup free_vars_and_rels_up_alias_expansion (evarconv)

Small cache to avoid checking the same Rel or Var twice.
Consider an unification problem like the following one:

a := huge
b := F1 a + F2 a
c := G1 b + G2 b
===============
 ?i[c,b,a] == ?g[c,c,c]

The old code, as the "not optimal" comment was suggesting,
did process every item in the explicit substitution, even
duplicated ones, unfolding the letins over and over.

This was the cause of the huge slowdown in the definition
of cormen_lup in Ssreflect/theories/matrix.v, that
follows:

Fixpoint cormen_lup {n} :=
  match n return let M := 'M[F]_n.+1 in M -> M * M * M with
  | 0 => fun A => (1, 1, A)
  | _.+1 => fun A =>
    let k := odflt 0 [pick k | A k 0 != 0] in
    let A1 : 'M_(1 + _) := xrow 0 k A in
    let P1 : 'M_(1 + _) := tperm_mx 0 k in
    let Schur := ((A k 0)^-1 *: dlsubmx A1) *m ursubmx A1 in
    let: (P2, L2, U2) := cormen_lup (drsubmx A1 - Schur) in
    let P := block_mx 1 0 0 P2 *m P1 in
    let L := block_mx 1 0 ((A k 0)^-1 *: (P2 *m dlsubmx A1)) L2 in
    let U := block_mx (ulsubmx A1) (ursubmx A1) 0 U2 in
    (P, L, U)
  end.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15114 85f007b7-540e-0410-9357-904b9bb8a0f7
Relax uniform inheritance condition

Uniform inheritance is not always needed for the coercion mechanism
to work. We turn it into a warning.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15115 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Fixing a few bugs (see #2571) related to the interpretation of
multiple binders:
- fixing missing spaces in the format of the exists' notations (Logic.v);
- fixing wrong variable name in check_is_hole error message (topconstr.ml);
- interpret expressions with open binders such as "forall x y, t" as
  "forall (x:_) (y:_),t" instead of "forall (x y:_),t" to avoid
  the "implicit type" of a variable being propagated to the type of
  another variable of different base name.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15124 85f007b7-540e-0410-9357-904b9bb8a0f7
Backporting color picker in CoqIDE.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15126 85f007b7-540e-0410-9357-904b9bb8a0f7
Pfedit: avoid Undoing too much

 It seems that we can currently do a successful Undo (but not two!)
 on a freshly started Lemma. Let's add a depth check on Pfedit.undo
 to avoid that. This way, we cannot Undo to depth < 1 (with 1 being
 the initial depth of a lemma).

 Simplier implementation of Pfedit.restart : it is Pfedit.undo_todepth 1.

 This extra initial step in the Undo Stack has probably something
 to see with the Lemma argument introduction. For instance, before this
 patch we had:

 Lemma test n : n+0=n.
 Restart. (* now the goal is universally quantified ! *)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15132 85f007b7-540e-0410-9357-904b9bb8a0f7
Ppvernac: nicer printing of proof delimiters { ... }

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15133 85f007b7-540e-0410-9357-904b9bb8a0f7
Remove old proof-managment commands Suspend/Resume

There're not compatible with the current Backtrack mecanism used
both by ProofGeneral and CoqIDE.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15134 85f007b7-540e-0410-9357-904b9bb8a0f7
Remove undocumented command "Delete foo"

 This command isn't trivial to port to the forthcoming evolution of
 backtracking in coqtop. Moreover, it isn't clear whether this
 "Delete" works well in advanced situation (was not updating
 frozen states).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15135 85f007b7-540e-0410-9357-904b9bb8a0f7
A unified backtrack mechanism, with a basic "Show Script" as side-effect

 Migrate the backtracking code from ide_slave.ml into a new backtrack.ml.
 In particular the history stack of commands that used to be there is now
 non-coqide-specific.

 ** Adapted commands **

 - "Show Script": a basic functional version is restored (and the printing
 of scripts at Qed in coqtop). No indentation, one Coq command per line,
 based on the vernac_expr asts recorded in the history stack, printed via
 Ppvernac.

 - "Back n" : now mimics the backtrack of coqide: it goes n steps back
 (both commands and proofs), and maybe more if needed to avoid re-entering
 a proof (it outputs a warning in this case).

 - "BackTo n" : still try to go back to state n, but it also handles the
 proof state, and it may end on some state n' <= n if needed to avoid
 re-entering a proof. Ideally, it could someday be used by ProofGeneral
 instead of the complex Backtrack command.

 ** Compatible commands **

 - "Backtrack" is left intact from compatibility with current ProofGeneral.
 We simply re-synchronize the command history stack after each Backtrack.

 - "Undo" is kept as a standard command, not a backtracking one, a bit like
 "Focus". Same for "Restart" and "Abort". All of these are now accepted
 in coqide (Undo simply triggers a warning).

 - Undocumented command "Undo To n" (counting from start of proof instead of
 from end) also keep its semantics, it is simply made compatible with
 the new stack mechanism.

 ** New restrictions **

 We now forbid backtracking commands (Reset* / Back*) inside files
 when Load'ing or compiling, or inside VernacList/VernacTime/VernacFail.
 Too much work dealing with these situation that nobody uses.

 ** Internal details **

 Internally, the command stack differs a bit from what was in Ide_slave
 earlier (which was inspired by lisp code in ProofGeneral). We now tag
 commands that are unreachable by a backtrack, due to some proof being
 finished, aborted, restarted, or partly Undo'ed. This induce a bit of
 bookkeeping during Qed/Abort/Restart/Undo, but then the backtracking code
 is straightforward: we simply search backward the first reachable state
 starting from the desired place. We don't depend anymore on the proof
 names (apart in the last proof block), It's more robust this way
 (think of re-entering a M.foo from an outside proof foo).

 Many internal clarifications in Lib, Vernac, etc. For instance
 "Reset Initial" is now just a BackTo 1, while "Reset foo" now calls
 (Lib.label_before_name "foo"), and performs a BackTo to the corresponding
 label.

 Concerning Coqide, we directly suppress the regular printing of goals
 via a flag in Vernacentries. This avoid relying on a classification
 of commands in Ide_slave as earlier.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15136 85f007b7-540e-0410-9357-904b9bb8a0f7