patch by Brian committed, cut&paste should not crash matita any longer

Setoid-Rewriting under Ex works for an arbitrary depth of Ex. Patches needed:

Index: ../components/ng_refiner/nCicUnification.ml
===================================================================
--- ../components/ng_refiner/nCicUnification.ml (revision 10941)
+++ ../components/ng_refiner/nCicUnification.ml (working copy)
@@ -97,7 +97,7 @@
    let time2 = Unix.gettimeofday () in
    let time1 =
     match !times with time1::tl -> times := tl; time1 | [] -> assert false in
-   prerr_endline ("}}} " ^ string_of_float (time2 -. time1));
+   prerr_endline ("}}} " ^ !indent ^ " " ^ string_of_float (time2 -. time1));
    (match exc_opt with
    | Some e ->  prerr_endline ("exception raised: " ^ Printexc.to_string e)
    | None -> ());
@@ -730,6 +730,32 @@
               | Uncertain _ as exn -> raise exn
               | _ -> assert false
     in
+    let fo_unif_heads_and_cont_or_unwind_and_hints
+      test_eq_only metasenv subst m1 m2 cont hm1 hm2
+     =
+      let ms, continuation =
+        (* calling the continuation inside the outermost try is an option
+           and makes unification stronger, but looks not frequent to me
+           that heads unify but not the arguments and that an hints can fix
+           that *)
+        try fo_unif test_eq_only metasenv subst m1 m2, cont
+        with
+        | UnificationFailure _
+        | KeepReducing _ | Uncertain _ as exn ->
+           let (t1,norm1),(t2,norm2) = hm1, hm2 in
+           match
+             try_hints metasenv subst
+              (norm1,NCicReduction.unwind t1) (norm2,NCicReduction.unwind t2)
+           with
+            | Some x -> x, fun x -> x
+            | None ->
+                match exn with
+                | KeepReducing msg -> raise (KeepReducingThis (msg,hm1,hm2))
+                | UnificationFailure _ | Uncertain _ as exn -> raise exn
+                | _ -> assert false
+      in
+        continuation ms
+    in
     let height_of = function
      | NCic.Const (Ref.Ref (_,Ref.Def h))
      | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
@@ -767,7 +793,7 @@
             match t1 with
             | C.Const r -> NCicEnvironment.get_relevance r
             | _ -> [] *) in
-          let unif_from_stack t1 t2 b metasenv subst =
+          let unif_from_stack (metasenv, subst) (t1, t2, b) =
               try
                 let t1 = NCicReduction.from_stack ~delta:max_int t1 in
                 let t2 = NCicReduction.from_stack ~delta:max_int t2 in
@@ -784,14 +810,19 @@
                 NCicReduction.unwind (k2,e2,t2,List.rev l2),
                 todo
           in
-        let hh1,hh2,todo=check_stack (List.rev s1) (List.rev s2) relevance [] in
+          let check_stack l1 l2 r =
+            match t1, t2 with
+            | NCic.Meta _, _ | _, NCic.Meta _ ->
+                (NCicReduction.unwind (k1,e1,t1,s1)),
+                (NCicReduction.unwind (k2,e2,t2,s2)),[]
+            | _ -> check_stack l1 l2 r []
+          in
+        let hh1,hh2,todo = check_stack (List.rev s1) (List.rev s2) relevance in
         try
-         let metasenv,subst =
-          fo_unif_w_hints test_eq_only metasenv subst (norm1,hh1) (norm2,hh2) in
-         List.fold_left
-          (fun (metasenv,subst) (x1,x2,r) ->
-            unif_from_stack x1 x2 r metasenv subst
-          ) (metasenv,subst) todo
+          fo_unif_heads_and_cont_or_unwind_and_hints
+            test_eq_only metasenv subst (norm1,hh1) (norm2,hh2)
+            (fun ms -> List.fold_left unif_from_stack ms todo)
+            m1 m2
         with
          | KeepReducing _ -> assert false
          | KeepReducingThis _ ->

fixed notation

some more work

Change (or better define) the order of hints premises.

They are now processed top to bottom, and not viceversa as before. This seems
to be right thing, since rules like:

  X := carr T
  ....
  R := mk_foo ... (P X) ... T ...
 --------------------------------- |-
  carr R = (P X)

can't be written putting X := carr T last, but you really want to be sure that
the needed assumptions to obtain a foo (in that case, that X is the carrier of
a setoid T) are available _before_ you even try to typecheck the bigger
unification problem (that may not be well typed if X and carr T are not
_convertible_, since in the fix function called in instantiate we call the
typechecker and not the refiner).

non uniform coercions landed in hints_declaration.ma, setoids and sets library
updated accordingly

Some refactoring in set*.ma, some new notations and new hints for \cup.
non uniform coercions still to be pushed from re-setoids.ma to a place
before sets.ma, maybe in hints_declaration.ma since they are complementary.

th 16.2 proved in the setoids setting

...

better not allowed sort elimination error messsage

...

...

...

some fixes to cope with the new mowgli server architecture

we can now generate static html pages about crg terms

some inprovements on the generated html pages

ld.dtd: updated to comply with crg
Makefiles: updated to comply with new HELM server configuration
top: some traces of old command line option "-m" removed

we removed old HAL exportation (replaced by XML exportation)

we renamed the module abbreviations according to src/modules.ml
ld.dtd: now is more strict
Makefiles: some refactoring
crg: bug fix in name/indexes translation
xmlLibrary: bug fix in the rendering of the "name" attribute: ^ is
forbidden in a NMTOKEN
brgOutput: new xml exportation via xmlCrg

the refactoring continues ...

new module "xml" devoted to xml I/O

the refactoring continues ....

now we take the NUri module from the helm-ng_kernel packeage

the refactoring continues

refactoring: helena sources are now in a dedicated directory

txtLexer: bug fix in parsing the string tokens
library: we now export the "meta" attribute
crgXml: crg exportation factorized and alpha conversion now works
crgBrg: we now mark the abstraction and the reverse translation works
ld.dtd: updated to export crg contents

- we simplified the parser return values
- now the display of parser and lexer debug information is controlled
from the command line (with the options -P and -L)
complete_rg: now the empty binders are not treated especially
top: we isolated a fragment of slow code (process_streaming) to be
investigated. It can be enabled with the -1 command line option)
Makefile: we now create the etc directory when it is missing

Bug fixed: nodes were copied.

interpret non ambiguous symbols ASAP

...

allows auto before eq is defined

...

Fixes unexpected behaviour of ncut when multiple goals are selected.

Experimental enhancements to the ndestruct tactic. By using the syntax

ndestruct (e1 ... em) skip (H1 ... Hn)

the user can tell the tactic that
- only equations e1 ... em should be considered
- rewriting should happen only in hypotheses H1 ... Hn and in the goal

both "(e1 ... em)" and "skip (H1 ... Hn)" are optional parameters.

Some experiments on a co-inductive Heityng algebra.

...

some work on \exists

eq -> eq0 renaming

useless box removed

fixed precedence so that no () are needed around variable assignement

do not apply hints if metaclosed

avoid assert false, just fail generating the coercion

...

...

...

...

new icons for the lambda-delta web site

completed lemma 17

...

re 16.4 almost done

big mess of notation

more notation

moved formal_topology into library"

some notation for map_arrows2

...

Some important proofs/definitions were (and are still) commented out and
do not compile.

Added the notion of functor1 to state the main theorem.

Proof simplified.

Proof simplified (??).

...

...

...

...

....

...

notation made half decent

better notation for oalgebra

....

off by one fixed

Fix for inversion principles of types with a single constructor.

Fixed a bug in the undebruijnate function which caused the refiner to produce
a wrong object when refining mutually recursive functions (the references to
recursive calls would contain the wrong index to the recursive argument).

some stuff on re

unify left args of inductive types with left argus of constructors. this allows
to put ? in every left arg of every constructor of an inductive type.

Library support files for John Major equality and Russell.

Experimental support for Russell (coercions moving inside lambda & pattern
matching etc.) added to the refiner.

minimization.ma

little workaround for multiple screens, gdk support not bound by lablgtk2

new intro:
- #; -- introduces into the context every possible assumption giving
        to it an unusable name
- #h1 .. h2; -- multi intros
- intros; -- macro che espande a #h1...hn.

trace generation with "// by _;"

notation

remarks and applyS

Bug fixed: nstatus => status (to undo the changes).

Worring warnings commented out.

...

Fixing naming scheme for composite coercions.

assert false could happen

Bug fixed:

 During unification of E1 with E2, E1 and E2 where not always reduced.
 In particular, reduction was not performed in the cases:
   LetIn vs LetIn, Match vs Match
 and maybe also in some cases Appl Meta vs Appl Meta (who knows?)

coinduction is between us

First tests.

* Fixed a couple of glitches in ndestruct
  - blob equations were not always handled properly
  - tactic used to fail due to not optimal behaviour of the refiner
* Added (experimental) support for JM equality to ndestruct

Regular expressions.

new dependences

From: fguidi <fguidi@c2b2084f-9a08-0410-b176-e24b037a169a>

Elimination of recursive inductive types leads to looping.
ELimnation of singleton types gives problems with negation.

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

alpha_eq instead of pervasives.compare

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

bool_ext on 'o' not on 'Prop' (they are convertible, but discrimination
trees do not compare up to conversion)

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

...

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

...

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

Formal points.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

Some dualization clean-up.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

fixed makefile

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

auto destructs while introducing in the context

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

print nobjects (hack with Obj.magic)

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>